Visible to the public Towards the formal verification of security properties of a Network-on-Chip router

TitleTowards the formal verification of security properties of a Network-on-Chip router
Publication TypeConference Paper
Year of Publication2018
AuthorsSepulveda, Johanna, Aboul-Hassan, Damian, Sigl, Georg, Becker, Bernd, Sauer, Matthias
Conference Name2018 IEEE 23rd European Test Symposium (ETS)
Keywordscryptography, formal verification, Hardware, integrated circuit design, IP networks, Metrics, model checking, multiprocessing systems, MultiProcessors Systems-on-Chip, network on chip security, network routing, network-on-chip, Network-on-Chip router, NoC routing architectures, pubcrawl, resilience, Resiliency, Routing, Scalability, security, Timing
Abstractpubcrawl, Network on Chip Security, Scalability, resiliency, resilience, metrics, 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.
Citation Keysepulveda_towards_2018