Benchmarking the Capabilities and Limitations of SAT Solvers in Defeating Obfuscation Schemes

TL;DR

This paper benchmarks six SAT solvers to evaluate their effectiveness and limitations in attacking various obfuscation schemes, highlighting their performance differences based on circuit size and complexity.

Contribution

It provides a comprehensive comparison of SAT solver performance on obfuscated circuits, revealing their strengths, limitations, and the impact of solver choice on assessing obfuscation hardness.

Findings

Glucose and Lingeling excel on small-to-midsize circuits

MapleGlucose performs well on mid-to-difficult obfuscation if memory is sufficient

Solver execution times vary significantly, affecting hardness assessment

Abstract

In this paper, we investigate the strength of six different SAT solvers in attacking various obfuscation schemes. Our investigation revealed that Glucose and Lingeling SAT solvers are generally suited for attacking small-to-midsize obfuscated circuits, while the MapleGlucose, if the system is not memory bound, is best suited for attacking mid-to-difficult obfuscation methods. Our experimental result indicates that when dealing with extremely large circuits and very difficult obfuscation problems, the SAT solver may be memory bound, and Lingeling, for having the most memory efficient implementation, is the best-suited solver for such problems. Additionally, our investigation revealed that SAT solver execution times may vary widely across different SAT solvers. Hence, when testing the hardness of an obfuscation method, although the increase in difficulty could be verified by one SAT solver, the pace of increase in difficulty is dependent on the choice of a SAT solver.