In Praise of Exact-Functional-Secrecy in Circuit Locking

Many logic locking schemes have been proposed and subsequently broken in recent years most notably by oracle-guided SAT-solver-based attacks. This has in part been due to a lack of formal definitions of security. Recent work has however taken the first steps towards this by defining some notions of security. One such notion, exact-functional-secrecy (EFS) is satisfied as soon as the attacker is not able to learn the precise functionality of the original circuit. This is less stringent than the approximate-functional-secrecy (AFS) notion of security which captures approximation-resiliency. This paper focuses on EFS. We present first a novel SAT-based attack that can automatically divide the deobfuscation of a locked circuit into two different processes: a) deobfuscating high-activity/entropy nets which contribute to AFS and are best handled by a few queries and heavy SAT-solving, and b) deobfuscating low-activity nets which require many useless queries in search of a few rare informative queries. The attack, called the rare-fast-querying (RFQ) SAT attack, guarantees key-correctness for logic outside of low-activity cones, and is not exclusive to a specific low-activity locking scheme. We show how the RFQ attack can under some conditions, avoid exponential querying altogether. Given the insight from this attack, we then present a deeper look into EFS and discuss simple techniques to achieve always-exponential EFS with bearable overhead. We show how one can take advantage of the abundance of comparator logic at the RT-level of control-oriented designs to achieve EFS with even less overhead via absorbing existing structures.

Automated summary

Many logic locking schemes have been proposed and defeated, particularly by oracle-guided SAT-solver-based attacks. Recent work has begun to define security terms, including exact-functional-secrecy (EFS) and approximate-functional-secrecy (AFS). This paper focuses on EFS and introduces a novel SAT attack called the rare-fast-querying (RFQ) attack, which can automatically deobfuscate high-activity/entropy nets for key-correctness while also discussing techniques to achieve EFS with manageable overhead.