Security Analysis of a System-on-Chip Using Assertion-Based Verification

Current systems-on-chip designs contain multiple cores which perform a variety of processing, storage, and communication functions. Complexity of interactions among the cores and of the cores themselves introduce potential security vulnerabilities which can be exploited by malicious actors to mount a variety of attacks. Hence, it is essential to develop appropriate security policies to mitigate the vulnerabilities. In addition, these security policies should be formally specified and the design should be statically verified for security assurance prior to fabrication. In this paper, we show how a catalog of vulnerabilities can be used to develop mitigating security policies for a set of cores in a system-on-chip. We show how temporal logic assertions can be used to formally specify the security policies, parameterized using formal signal names. Given a specific target architecture, these parameterized assertions can be instantiated with actual signal names and verified using a formal verification tool. We demonstrate the application of this process to an OpenRISC-1200 based system-on-chip design written in Verilog. Security policies are specified as SystemVerilog Assertions and verified using Cadence JasperGold™. Three design errors ad-versely effecting the security policies are uncovered in the design.