SoC interconnection protection through formal verification

The wide adoption of third-party hardware Intellectual Property (IP) cores including those from untrusted vendors have raised security concerns for system designers and end-users. Existing approaches to ensure the trustworthiness of individual IPs rarely consider the entire SoC design, especially the IP interactions through SoC bus. These methods can hardly identify malicious logic (or design flaws) distributed in multiple IPs whereas individual IPs fulfill security properties and can pass the security testing/verification. One possible solution is to treat the SoC as one IP core and try to verify security properties of the entire design. This method, however, suffers from scalability issues due to the large size of SoC designs with multiple IP cores integrated. In this paper, we present a scalable SoC bus verification framework trying to verify the security properties of SoC bus implementation where the bus protocol plays the role of the golden reference. More specifically, finite state machine (FSM) models will be constructed from the bus implementation and the trustworthiness will be verified based on the property set derived from the bus protocol and potential security threats. Along with IP level formal verification solutions, the proposed framework can help ensure the security of large-scale SoCs. Experimental results on ARM AMBA Bus demonstrate that our approach is applicable and scalable to prevent information leakage and denial-of-service (DoS) attack by verifying security properties.