Towards the formal verification of security properties of a Network-on-Chip router
Towards the formal verification of security properties of a Network-on-Chip router
复制标题
实现片上网络路由器安全属性的形式验证
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
M. Sauer
中科院分区：
文献类型：
--
作者：
Martha Johanna Sepúlveda;Damian Aboul;G. Sigl;B. Becker;M. Sauer
可以利用片上网络 (NoC) 路由器中的漏洞和设计缺陷来监视、修改和限制多处理器片上系统 (MPSoC) 内部的敏感通信。尽管之前的工作解决了 NoC 威胁，但寻找安全有效的解决方案来验证安全性仍然是一个挑战。在这项工作中，我们首次提出了一种正式验证 NoC 路由器的正确性和安全属性的方法，以便提供适当的通信功能并避免 NoC 攻击。我们提出了一个通用的验证流程，证明了一系列与实现无关的安全相关属性。我们采用无界模型检查技术来解释 NoC 系统的高度顺序行为。评估结果通过展示六种不同 NoC 路由架构的验证结果证明了我们的方法的可行性，并展示了每种设计的漏洞。
Vulnerabilities and design flaws in Network-on-Chip (NoC) routers can be exploited in order to spy, modify and constraint the sensitive communication inside the Multi-Processors Systems-on-Chip (MPSoCs). Although previous works address the NoC threat, finding secure and efficient solutions to verify the security is still a challenge. In this work, we propose for the first time a method to formally verify the correctness and the security properties of a NoC router in order to provide the proper communication functionality and to avoid NoC attacks. We present a generalized verification flow that proves a wide set of implementation-independent security-related properties to hold. We employ unbounded model checking techniques to account for the highly-sequential behaviour of the NoC systems. The evaluation results demonstrate the feasibility of our approach by presenting verification results of six different NoC routing architectures demonstrating the vulnerabilities of each design.