International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

SMT Attack: Next Generation Attack on Obfuscated Circuits with Capabilities and Performance Beyond the SAT Attacks

Authors:
Kimia Zamiri Azar , ECE Department, George Mason University, Fairfax
Hadi Mardani Kamali , ECE Department, George Mason University, Fairfax
Houman Homayoun , ECE Department, George Mason University, Fairfax
Avesta Sasan , ECE Department, George Mason University, Fairfax
Download:
DOI: 10.13154/tches.v2019.i1.97-122
URL: https://tches.iacr.org/index.php/TCHES/article/view/7335
Search ePrint
Search Google
Presentation: Slides
Abstract: In this paper, we introduce the Satisfiability Modulo Theory (SMT) attack on obfuscated circuits. The proposed attack is the superset of Satisfiability (SAT) attack, with many additional features. It uses one or more theory solvers in addition to its internal SAT solver. For this reason, it is capable of modeling far more complex behaviors and could formulate much stronger attacks. In this paper, we illustrate that the use of theory solvers enables the SMT to carry attacks that are not possible by SAT formulated attacks. As an example of its capabilities, we use the SMT attack to break a recent obfuscation scheme that uses key values to alter delay properties (setup and hold time) of a circuit to remain SAT hard. Considering that the logic delay is not a Boolean logical property, the targeted obfuscation mechanism is not breakable by a SAT attack. However, in this paper, we illustrate that the proposed SMT attack, by deploying a simple graph theory solver, can model and break this obfuscation scheme in few minutes. We describe how the SMT attack could be used in one of four different attack modes: (1) We explain how SMT attack could be reduced to a SAT attack, (2) how the SMT attack could be carried out in Eager, and (3) Lazy approach, and finally (4) we introduce the Accelerated SMT (AccSMT) attack that offers significant speed-up to SAT attack. Additionally, we explain how AccSMT attack could be used as an approximate attack when facing SMT-Hard obfuscation schemes.
Video from TCHES 2019
BibTeX
@article{tches-2019-29066,
  title={SMT Attack: Next Generation Attack on Obfuscated Circuits with Capabilities and Performance Beyond the SAT Attacks},
  journal={IACR Trans. Cryptogr. Hardw. Embed. Syst.},
  publisher={Ruhr-Universität Bochum},
  volume={2019, Issue 1},
  pages={97-122},
  url={https://tches.iacr.org/index.php/TCHES/article/view/7335},
  doi={10.13154/tches.v2019.i1.97-122},
  author={Kimia Zamiri Azar and Hadi Mardani Kamali and Houman Homayoun and Avesta Sasan},
  year=2019
}