Symbolic assertion mining for security validation
Symbolic assertion mining for security validation
复制标题
用于安全验证的符号断言挖掘
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
G. Pravadelli
中科院分区：
文献类型：
--
作者：
Alessandro Danese;V. Bertacco;G. Pravadelli
本文介绍了DOVE，这是一个用于识别IP固件内部漏洞点的验证框架。该框架依赖于固件的符号模拟来搜索其计算路径中可能隐藏漏洞的角落情况。然后，DOVE自动挖掘出一组紧凑的形式化断言来代表这些不可能的路径，以指导验证工程师的分析。两个案例的实验结果表明，生成的断言在查明实际漏洞和执行时间方面的效率的有效性。
This paper presents DOVE, a validation framework to identify points of vulnerability inside IP firmwares. The framework relies on the symbolic simulation of the firmware to search for corner cases in its computational paths that may hide vulnerabilities. Then, DOVE automatically mine a compact set of formal assertions representing these unlikely paths to guide the analysis of the verification engineers. Experimental results on two case studies show the effectiveness of the generated assertions in pinpointing actual vulnerabilities and its efficiency in terms of execution time.