This paper introduces KRATT, a removal and structural analysis attack against state-of-the-art logic locking techniques, such as single and double flip locking techniques (SFLTs and DFLTs). KRATT utilizes powerful quantified Boolean formulas (QBFs), which have not found widespread use in hardware security, to find the secret key of SFLTs for the first time. It can handle locked circuits under both oracle-less (OL) and oracle-guided (OG) threat models. It modifies the locked circuit and uses a prominent OL attack to make a strong guess under the OL threat model. It uses a structural analysis technique to identify promising protected input patterns and explores them using the oracle under the OG model. Experimental results on ISCAS'85, ITC'99, and HeLLO: CTF'22 benchmarks show that KRATT can break SFLTs using a QBF formulation in less than a minute, can decipher a large number of key inputs of SFLTs and DFLTs with high accuracy under the OL threat model, and can easily find the secret key of DFLTs under the OG threat model. It is shown that KRATT outperforms publicly available OL and OG attacks in terms of solution quality and run-time.

翻译：本文提出KRATT方法，一种针对先进逻辑锁定技术的去除与结构分析攻击手段，主要针对单重翻转锁存技术（SFLTs）和双重翻转锁存技术（DFLTs）。KRATT首次利用在硬件安全领域尚未广泛应用的强大量化布尔公式（QBF），成功破解SFLTs的密钥。该方法可同时处理无预言机（OL）和预言机引导（OG）威胁模型下的锁定电路。在OL威胁模型下，KRATT通过修改锁定电路并借助一种主流OL攻击技术实现强推测；而在OG模型下，它采用结构分析技术识别有前景的保护输入模式，并利用预言机进行探索。在ISCAS'85、ITC'99及HeLLO: CTF'22基准测试上的实验结果表明：KRATT能在1分钟内基于QBF公式破解SFLTs；在OL威胁模型下，能以高精度解密SFLTs和DFLTs的大量关键输入；在OG威胁模型下，可轻易获取DFLTs的秘密密钥。结果证实，KRATT在求解质量与运行时间两方面均优于公开可用的OL及OG攻击方法。