硬件设计中信息流的增强符号执行
摘要：静态分析与符号执行相结合的SEIF方法用于验证和诠释硬件设计中的信息流路径。SEIF通过静态构建设计的信息流模型，并使用引导式符号执行来识别和消除高精度的非流动或找到真实流动的相应路径。我们在两个开源CPU、一个AES核心和AKER访问控制模块上评估了SEIF。SEIF平均可以耗时4-6秒，在10-12个时钟周期内进行全面的探索，并可以自动处理静态构建模型中86-90％的路径。此外，SEIF还可用于查找违反安全性属性的多个路径，为安全验证提供新的角度。
作者：Kaki Ryan, Matthew Gregoire and Cynthia Sturton
论文ID：2307.11884
分类：Cryptography and Security
分类简称：cs.CR
提交时间：2023-08-03