More Like this

1. SRCLock: SAT-Resistant Cyclic Logic Locking for Protecting the Hardware

   Roshanisefat, Shervin ; Mardani Kmali, Hadi ; Sasan, Avesta ( May 2018 , Proceedings of the 2018 on Great Lakes Symposium on VLSI)

   In this paper, we claim that cyclic obfuscation, when properly implemented, poses exponential complexity on SAT or CycSAT attack. The CycSAT, in order to generate the necessary cycle avoidance clauses, uses a pre-processing step. We show that this pre-processing step has to compose its cycle avoidance condition on all cycles in a netlist, otherwise, a missing cycle could trap the SAT solver in an infinite loop or force it to return an incorrect key. Then, we propose several techniques by which the number of cycles is exponentially increased with respect to the number of inserted feedbacks. We further illustrate that when the number of feedbacks is increased, the pre-processing step of CycSAT faces an exponential increase in complexity and runtime, preventing the correct composition of loop avoidance clauses in a reasonable time before invoking the SAT solver. On the other hand, if the pre-processing is not completed properly, the SAT solver will get stuck or return incorrect key. Hence, when the cyclic obfuscation in accordance to the conditions proposed in this paper is implemented, it would impose an exponential complexity with respect to the number of inserted feedback, even when the CycSAT solution is used.
2. InterLock: An Intercorrelated Logic and Routing Locking

   Hadi Mardani Kamali, Kimia Zamiri ( November 2020 , 2020 IEEE/ACM International Conference On Computer Aided Design (ICCAD))

   In this paper, we propose a canonical prune-and-SAT (CP&SAT) attack for breaking state-of-the-art routing-based obfuscation techniques. In the CP&SAT attack, we first encode the key-programmable routing blocks (keyRBs) based on an efficient SAT encoding mechanism suited for detailed routing constraints, and then efficiently re-encode and reduce the CNF corresponded to the keyRB using a bounded variable addition (BVA) algorithm. In the CP&SAT attack, this is done before subjecting the circuit to the SAT attack. We illustrate that this encoding and BVA-based pre-processing significantly reduces the size of the CNF corresponded to the routing-based obfuscated circuit, in the result of which we observe 100% success rate for breaking prior art routing-based obfuscation techniques. Further, we propose a new intercorrelated logic and routing locking technique, or in short InterLock, as a countermeasure to mitigate the CP&SAT attack. In Interlock, in addition to hiding the connectivity, a part of the logic (gates) in the selected timing paths are also implemented in the keyRB(s). We illustrate that when the logic gates are twisted with keyRBs, the BVA could not provide any advantage as a pre-processing step. Our experimental results show that, by using InterLock, with only three 8×8 or only two 16×16 keyRBs (twistedmore »with actual logic gates), the resilience against existing attacks as well as our new proposed CP&SAT attack would be guaranteed while, on average, the delay/area overhead is less than 10% for even medium-size benchmark circuits.« less
3. LUT-Lock: A Novel LUT-Based Logic Obfuscation for FPGA-Bitstream and ASIC-Hardware Protection

   https://doi.org/10.1109/ISVLSI.2018.00080  

   Mardani Kamali, Hadi ; Zamiri Azar, Kimia ; Gaj, Kris ; Homayoun, Houman ; Sasan, Avesta ( July 2018 , 2018 IEEE Computer Society Annual Symposium on VLSI (ISVLSI))

   In this work, we propose LUT-Lock, a novel Look-Up-Table-based netlist obfuscation algorithm, for protecting the intellectual property that is mapped to an FPGA bitstream or an ASIC netlist. We, first, illustrate the effectiveness of several key features that make the LUT-based obfuscation more resilient against SAT attacks and then we embed the proposed key features into our proposed LUT-Lock algorithm. We illustrate that LUT-Lock maximizes the resiliency of the LUT-based obfuscation against SAT attacks by forcing a near exponential increase in the execution time of a SAT solver with respect to the number of obfuscated gates. Hence, by adopting LUT-Lock algorithm, SAT attack execution time could be made unreasonably long by increasing the number of utilized LUTs.
4. On Efficiently Solvable Cases of Quantum k-SAT

   https://doi.org/10.4230/LIPIcs.MFCS.2018.38  

   Aldi, Marco ; De Beaudrap, Marco ; Gharibian, Sevag ; Saeedi, Seyran ( January 2018 , International Symposium on Mathematical Foundations of Computer Science)

   The constraint satisfaction problems k-SAT and Quantum k-SAT (k-QSAT) are canonical NP-complete and QMA_1-complete problems (for k >= 3), respectively, where QMA_1 is a quantum generalization of NP with one-sided error. Whereas k-SAT has been well-studied for special tractable cases, as well as from a parameterized complexity perspective, much less is known in similar settings for k-QSAT. Here, we study the open problem of computing satisfying assignments to k-QSAT instances which have a "matching" or "dimer covering"; this is an NP problem whose decision variant is trivial, but whose search complexity remains open. Our results fall into three directions, all of which relate to the "matching" setting: (1) We give a polynomial-time classical algorithm for k-QSAT when all qubits occur in at most two clauses. (2) We give a parameterized algorithm for k-QSAT instances from a certain non-trivial class, which allows us to obtain exponential speedups over brute force methods in some cases by reducing the problem to solving for a single root of a single univariate polynomial. (3) We conduct a structural graph theoretic study of 3-QSAT interaction graphs which have a "matching". We remark that the results of (2), in particular, introduce a number of new tools tomore »the study of Quantum SAT, including graph theoretic concepts such as transfer filtrations and blow-ups from algebraic geometry; we hope these prove useful elsewhere.« less
5. BeSAT: behavioral SAT-based attack on cyclic logic encryption

   https://doi.org/10.1145/3287624.3287670  

   Shen, Yuanqi ; Li, You ; Rezaei, Amin ; Kong, Shuyu ; Dlott, David ; Zhou, Hai ( January 2019 , Asia and South Pacific Design Automation Conference)

   Cyclic logic encryption is newly proposed in the area of hardware security. It introduces feedback cycles into the circuit to defeat existing logic decryption techniques. To ensure that the circuit is acyclic under the correct key, CycSAT is developed to add the acyclic condition as a CNF formula to the SAT-based attack. However, we found that it is impossible to capture all cycles in any graph with any set of feedback signals as done in the CycSAT algorithm. In this paper, we propose a behavioral SAT-based attack called BeSAT. Be-SAT observes the behavior of the encrypted circuit on top of the structural analysis, so the stateful and oscillatory keys missed by CycSAT can still be blocked. The experimental results show that BeSAT successfully overcomes the drawback of CycSAT.