Directed Test Generation for Activation of Security Assertions in RTL Models
Directed Test Generation for Activation of Security Assertions in RTL Models
复制标题
DOI：
10.1145/3441297
复制
发表时间：
2021-01
期刊：
影响因子：
--
通讯作者：
Hasini Witharana;Yangdi Lyu;P. Mishra
中科院分区：
文献类型：
--
作者：
Hasini Witharana;Yangdi Lyu;P. Mishra
断言广泛用于软件和硬件设计的功能验证以及覆盖分析。断言支持运行时错误检测以及更快的错误定位。虽然有大量的文献都在软件和硬件断言监控功能的情况下，有有限的努力，利用断言监控系统芯片（SoC）的安全漏洞。我们已经确定了常见的SoC安全漏洞，并定义了几个类的断言，使运行时检查的安全漏洞。基于断言的验证中的一个主要挑战是如何激活安全断言以确保它们是有效的。虽然现有的测试生成使用模型检测是有前途的，它不能产生大型设计的直接测试，由于状态空间爆炸。我们提出了一个自动化和可扩展的机制来生成直接测试使用的RTL模型的符号执行和具体的模拟相结合。不同基准测试的实验结果表明，有向测试能够非空地激活安全断言。
Assertions are widely used for functional validation as well as coverage analysis for both software and hardware designs. Assertions enable runtime error detection as well as faster localization of errors. While there is a vast literature on both software and hardware assertions for monitoring functional scenarios, there is limited effort in utilizing assertions to monitor System-on-Chip (SoC) security vulnerabilities. We have identified common SoC security vulnerabilities and defined several classes of assertions to enable runtime checking of security vulnerabilities. A major challenge in assertion-based validation is how to activate the security assertions to ensure that they are valid. While existing test generation using model checking is promising, it cannot generate directed tests for large designs due to state space explosion. We propose an automated and scalable mechanism to generate directed tests using a combination of symbolic execution and concrete simulation of RTL models. Experimental results on diverse benchmarks demonstrate that the directed tests are able to activate security assertions non-vacuously.