中文

HOLL:面向高阶逻辑锁定的程序合成

密码学与安全 2022-01-26 v1 形式语言与自动机理论 计算机科学中的逻辑

摘要

逻辑锁定“隐藏”数字电路的功能,以保护其免遭仿冒、盗版与恶意设计修改。原始设计被转换为“锁定”设计,使得电路仅当使用秘密比特序列——密钥比特串——“解锁”时才显现正确功能。然而,强力攻击尤其是使用SAT求解器恢复密钥比特串的SAT攻击,已极有效地破解锁定电路并恢复电路功能。我们将逻辑锁定提升为高阶逻辑锁定(HOLL),通过隐藏高阶关系而非独立值密钥,迫使攻击者发现该密钥关系以重建电路功能。我们的技术使用程序合成构建锁定设计并合成相应密钥关系。HOLL开销低,且现有逻辑锁定攻击均不适用,因为待恢复实体不再是值。为评估我们的方案,我们提出一种新攻击(SynthAttack),其使用归纳合成算法并以运行电路作为输入输出预言机来恢复隐藏功能。SynthAttack受SAT攻击启发,且类似SAT攻击,它是可验证正确的,即若正确功能被显现,验证检查可保证其结果相同。我们的实证分析表明,SynthAttack可破解小型电路与小规模密钥关系的HOLL,但对实际设计无效。

关键词

引用

@article{arxiv.2201.10531,
  title  = {HOLL: Program Synthesis for Higher OrderLogic Locking},
  author = {Gourav Takhar and Ramesh Karri and Christian Pilato and Subhajit Roy},
  journal= {arXiv preprint arXiv:2201.10531},
  year   = {2022}
}

备注

Accepted in TACAS-22 conference. 24 pages llncs format (without references), 11 figures, 5 tables