SaTC: STARSS: ICM: Invariant Carrying Machine for Hardware Assurance

Project: Research project

Description

PROJECT SUMMARY

Semiconductor-based hardware is the foundation of interconnected and intelligent systems--from personal computers and mobile phones to Internet, financial, energy, and other critical infrastructure systems. As we increasingly depend upon these systems in our everyday lives, their trustworthiness and security are more critical than ever. Since the software trustworthiness can only be built upon the trustworthiness of hardware, the assurance and security of hardware has become an important problem that cannot be avoided.

Design and manufacture of complex semiconductor circuits and systems requires many steps, and one design could involve hundreds of engineers,typically distributed across multiple locations and organizations worldwide. Moreover, the deployment of IP blocks from different sources has become a common practice. The conventional processes and tools for design and manufacture of semiconductors at most ensure the correctness, that is, the resulting product does what it is supposed to do. However, to date, these processes do not provide confidence about whether the chip is altered such that it provides unauthorized access or control. Such undesirable behavior can be due to a weakness in the design that results in an unintentional side channel or due to maliciously inserted Trojan hardware.

In this research, we propose one approach called Invariant-Carrying Machine (ICM) for hardware assurance. This approach is based on the concept of light-weight formal method and only requires minor additions over the conventional design process. In this approach, each design will carry with it an inductive invariant that is used to guarantee its 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 will investigate the principles for selecting security invariant and develop tools for creating and checking those invariants.

Intellectual Merit:
Compared with software design, hardware design is the area where formal verification has a stronger food hold and is broadly deployed. Our project will leverage such an advantage and develop a framework of Invariant-Carrying Machine (ICM) for hardware assurance. Based on the observation that the most expensive part of formal verification happens on the generation of inductive invariant from general invariant, our approach requests an inductive invariant as a proof in order to reduce the checking cost. Instead of correctness invariants, the project will investigate the invariants relevant to security properties, and testing their effectiveness on Trojan detection.

Broader Impacts:
Hardware is the foundation of modern information technology. One big obstacle for increasing the productivity of hardware design thus decreasing the cost and barrier for adoption of information technology for economic-societal disadvantaged groups is the complexity of the design process and the design control for security assurance. The project will help to increase the deployment of third party components and decrease the design control, thus decreasing the design cost of hardware. The increased hardware assurance level will also help to improve the security of critical infrastructures, such as the Internet and the power grid network, which ultimately increases the homeland security.
StatusFinished
Effective start/end date10/1/149/30/19

Funding

  • National Science Foundation (CNS-1441695)

Fingerprint

Hardware
Critical infrastructures
Semiconductor materials
Information technology
Internet
Costs
Formal methods
National security
Networks (circuits)
Intelligent systems
Software design
Mobile phones
Personal computers
Computer hardware
Large scale systems
Productivity
Engineers
Economics
Testing