## CryptoDB

### Paper: 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 DOI: 10.13154/tches.v2019.i1.97-122 URL: https://tches.iacr.org/index.php/TCHES/article/view/7335 Search ePrint Search Google Slides 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.
##### 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
}