| Title | Towards the formal verification of security properties of a Network-on-Chip router |
| Publication Type | Conference Paper |
| Year of Publication | 2018 |
| Authors | Sepulveda, Johanna, Aboul-Hassan, Damian, Sigl, Georg, Becker, Bernd, Sauer, Matthias |
| Conference Name | 2018 IEEE 23rd European Test Symposium (ETS) |
| Keywords | cryptography, 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 |
| Abstract | pubcrawl, 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. |
| DOI | 10.1109/ETS.2018.8400692 |
| Citation Key | sepulveda_towards_2018 |
Towards the formal verification of security properties of a Network-on-Chip router