Security policies for ASIC/SoC designs can be stated using two different styles of assertions: (1) Information Flow Assertions (IFA), and (2) Temporal Logic Assertions (TLA). Both types assertions are found to be useful in practice and are supported by commercial verification tools. However, commercial formal verification is exclusively focused on pre-fabrication verification with no clear path provided to ensure that the security guarantees hold during run-time.

Accordingly, our research aims to develop methodologies and tools for migrating both IFA and TLA assertions used in prefabrication verification to run-time monitors usable for post fabrication security validation and for continuous security monitoring during the operation of the ASIC/SoC.

Specifically, we will develop and evaluate a security assurance methodology supported by two sets of tools: (1) Automated synthesis of run-time security monitors from security policy specifications in the form of IFA and TLA assertions. Information flow assertions will be specified in a notation similar to Tortuga Logic’s Sentinel language. Temporal logic assertions will be specified in the System Verilog Assertions (SVA) notation. (2) Automated security test generation for validating the synthesized run-time security monitors. A security policy driven design mutation generator will be developed to inject various types of security violations in the ASIC/SoC design. The tests generated can test for these security flaws in the fabricated ASIC/SoC chips.

In addition, the methodology and tools will be thoroughly evaluated using a set of ASIC and SoC designs selected from the opencores.org web site. These will include but not limited to an OpenRISC-1200 based SoC and a RISC-V based processor.