dipanjanroy/SMT-Attack

# SMT-Attack 一个基于可满足性模理论（SMT）的工具，通过恢复混淆密钥来评估在高级综合（HLS）阶段被混淆的硬件设计的安全性。 ## 仓库结构 ``` SMT Attack Code/ │── Obfuscated/ # Obfuscated Verilog designs _obfuscated_hls.v │── Oracle/ # Original (oracle) Verilog designs _hls.v │── Smt_Attack_Verilog.py # Main script for performing the SMT-based attack ``` ### Obfuscated/ 包含待分析的 HLS 混淆 Verilog 设计。 ### Oracle/ 包含在攻击过程中用作 oracle 的相应原始（未混淆）Verilog 设计。 ### Smt_Attack_Verilog.py 主要的 Python 脚本，通过生成 SMT 约束、查询 oracle 并恢复正确的混淆密钥，来执行基于 SMT 的密钥恢复攻击。 # 针对 High-Level-Synthesis 混淆的 SMT Attack 一个基于 SMT 的框架，用于通过密钥恢复分析在高级综合阶段应用的硬件混淆的安全性。给定一个锁定（混淆）的设计及其功能性 oracle，该框架能够恢复解锁该设计的密钥。它是 oracle 引导的，适用于在高级综合阶段混淆的任何设计，与具体的混淆技术无关。 ## 环境要求 - Python 3.8+ - [Z3](https://github.com/Z3Prover/z3)：`pip install z3-solver` ## 用法 ``` python SMT_Attack_Verilog.py ``` 该脚本会列出 `Obfuscated Files/` 中的所有混淆设计，并询问要破解哪一个。然后，它会在 `Oracle/` 中查找匹配的 oracle（名称相同但去掉 `_obfuscated`，例如 `iirb_obfuscated_hls.v` → `iirb_hls.v`）。由于该攻击是 oracle 引导的，如果找不到 oracle，它将停止运行并输出提示信息。成功后，它会打印出恢复的密钥、使用的区分性输入数量以及运行时间。 可选的自检功能 —— 将恢复的密钥重新代入设计中，并在随机输入下根据 oracle 对其进行验证： ``` python SMT_Attack_Verilog.py --selfcheck ``` ## 工作原理 该攻击保留两个独立的符号化密钥副本，并搜索一个使它们产生分歧的输入（即区分性输入）。它向 oracle 查询该输入，并约束每一个候选密钥使其匹配。每一个这样的输入都会排除至少一个错误的密钥类别；当不再有区分性输入时，密钥即被唯一确定并输出。 ## 许可证 基于 MIT 许可证发布 —— 详见 [LICENSE](LICENSE)。 ## 免责声明 仅用于学术和研究目的：评估 HLS 阶段的硬件混淆安全性。

标签：SMT求解器, Z3, 密码分析, 形式化验证, 硬件安全, 逆向工具, 逻辑加密