Formal verification of security properties

Network-on-Chip (NoC) routers can be exploited in order to spy, modify and constrain 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 a method that allows the formal verification of the correctness and security properties of NoC routers. For limitation space in this article we show our technique to formally verify the security and correctness of several arbiters, one of the main router component. We show that our method is an effective and efficient solution towards secure routers.      «

Network-on-Chip (NoC) routers can be exploited in order to spy, modify and constrain 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 a method that allows the formal verification of the correctness and security properties of NoC routers. For limitation space in this article we show our technique to formally...     »