Design of complex semiconductor circuits and systems requires many steps, involves hundreds of engineers, and is typically distributed across multiple locations and organizations worldwide. The conventional processes and tools for design of semiconductors can ensure the correctness, that is, the resulting product does what it is supposed to do. However, these processes do not provide confidence about whether the chip is altered such that it provides unauthorized access or control. Such undesirable behavior may due to a weakness in the design that results in an unintentional side channel or due to maliciously inserted Trojan hardware. This project develops techniques for improving the reliability and trustworthiness of hardware systems. The Invariant-Carrying Machine (ICM) approach developed in this project is based on light-weight formal methods, and requires only minor additions over the conventional design process. In this approach, each design carries with it an inductive invariant that is used to guarantee the security. When receiving a design from the third party or after a complex design process, the user can check whether the circuit inductively satisfies the invariant and whether the invariant satisfies the security rules. Any violation will raise a red flag for deploying the design. The project develops principles and tools for checking inductive invariants, investigates suitable security properties, and validates the approach by testing on hardware Trojan benchmarks.
SaTC: STARSS: ICM: Invariant Carrying Machine for Hardware Assurance