Mutation Analysis and Model Checking Guided Test Generation for SoC Run-Time Monitors

Security verification and validation both before and after fabrication emerged as an important concern in the design of systems-on-chip (SoC) architectures. Assertion-based formal methods are widely for pre-fabrication verification of SoC designs. Assertions denoting the SoC's security policies are formally verified to check if the design satisfies these specifications. In addition, several researchers have proposed to migrate these assertions into silicon as run-time monitors to facilitate continuous run-time security monitoring. However, due to limited observability, post-silicon validation of these run-time monitors requires input sequences that are specifically targeted to testing these monitors. In this paper, we present a methodology to produce a variety of tests for assertion-based run-time monitors. Given temporal logic assertions which denote security properties of an SoC design, the methodology consists of the following steps: (1) introduce mutations into the SoC design model to cause assertion failures, (2) use model checking to produce counterexample traces, (3) generate alternative and longer counterexamples for a mutant, with the help of novel algorithms to enhance the test suite, (4) extract test programs from the counterexamples and winnow repetitive test cases, (5) investigate the code coverage of the design with the help of these multiple tests. This methodology can be used to generate a large number of tests for each security monitor, enhancing the design's code coverage. We demonstrate the methodology for a large OpenRISC-1200 based SoC design. We show the effectiveness of the generated test programs via simulation and FPGA-based emulation.