Property Driven Hardware Security

Synopsis: Materials related to the 2020 IEEE International Symposium on Hardware Oriented Security and Trust (HOST) Tutorial on “Property Driven Hardware Security” presented on December 7, 2020 by Nicole Fern (Tortuga Logic) and Ryan Kastner (UC San Diego).


Overview: There are a large and growing number of hardware specific security vulnerabilities. Meltdown, Spectre, Foreshadow, TLBleed, and countless other attacks expose architectural flaws with implications on the security of computing devices ranging from cloud services to embedded devices. With the dramatic increase in hardware security flaws reported, it is clear that we have reached a time where hardware has become an attractive attack surface that can be exploited with potentially large consequences. To mitigate these attacks we must make security a first class citizen in the hardware design process.

Property driven hardware security is a design methodology to assess the safety and security of hardware designs. It enables security experts to describe how the hardware should (or should not) function. These security properties are formally specified using languages that map to models that are easy to verify using existing design tools. There are three fundamental elements for any hardware security design flow. First, security experts need expressive languages to specify these security properties. Second, these properties should map to models to describe the security related behavior of a hardware design. Finally, hardware security design tools verify that the hardware design meets these properties using formal solvers, simulation, and emulation.

This tutorial looks at the elements of a property driven hardware security design methodology. A property driven hardware security design methodology starts with expressive security models that enable one to specify safety and security properties related to confidentiality, integrity, availability, separation, isolation, side channels, real-time operation, and Trojans. These models provide a formal way to specify the desired security of the hardware. Hardware security verification tools evaluate that the hardware design meets these security properties. These tools help the hardware designer find the source of security flaws and provide an assessment of their potential risks. Information flow and statistical models provide the necessary expressive power for specifying these properties, while also leveraging existing hardware verification tools for formal analysis, simulation, and emulation.