Post-SAT 2: Insertion of SAT-Unresolvable Structures

This chapter presents cyclic logic locking and one-way function-based logic locking. The underlying idea of both schemes is to embed structures in a netlist that are hard to resolve for a SAT solver. Cyclic logic locking introduces cycles into a netlist with the expectation that it will render the SAT attack effort exponential in the number of cycles introduced. However, cyclic logic locking is vulnerable to the CycSAT attack, which can encode the presence of cycles in the CNF representation. One-way function-based logic locking integrates one-way functions into the locked netlist to render the SAT attack computationally infeasible. The SAT attack resilient techniques discussed so far achieve high SAT attack resilience by compromising on the output corruptibility. This chapter introduces two logic locking techniques that need not make such compromise. Section 8.1 introduces cyclic logic locking that inserts cycles/loops in a netlist to thwart the SAT attack. Section 8.2 highlights the security vulnerabilities of cyclic logic locking and presents CycSAT, an attack that can break cyclic logic locking. Section 8.3 presents one-way function-based logic locking that integrates one-way functions into the locked netlist.