Mining Secure Behavior of Hardware Designs

TL;DR

This paper applies specification mining techniques to hardware security, demonstrating how to discover security properties in CPU designs that can prevent vulnerabilities and attacks, using control signals, temporal logic, and information flow analysis.

Contribution

It introduces hardware-specific specification mining methods for security, including control signal partitioning, security-temporal logic templates, and information flow tracking, addressing hardware design challenges.

Findings

Discovered security specifications in x86 CPU designs preventing privilege escalation.

Identified security properties related to system initialization and historical vulnerabilities.

Demonstrated the use of information flow tracking to verify absence of certain weaknesses.

Abstract

Specification mining offers a solution by automating security specification for hardware. Specification miners use a form of machine learning to specify behaviors of a system by studying a system in execution. However, specification mining was first developed for use with software. Complex hardware designs offer unique challenges for this technique. Further, specification miners traditionally capture functional specifications without a notion of security, and may not use the specification logics necessary to describe some security requirements. This work demonstrates specification mining for hardware security. On CISC architectures such as x86, I demonstrate that a miner partitioning the design state space along control signals discovers a specification that includes manually defined properties and, if followed, would secure CPU designs against Memory Sinkhole and SYSRET privilege escalation. For temporal properties, I demonstrate that a miner using security specific linear temporal logic (LTL) templates for specification detection may find properties that, if followed, would secure designs against historical documented security vulnerabilities and against potential future attacks targeting system initialization. For information--flow hyperproperties, I demonstrate that a miner may use Information Flow Tracking (IFT) to develop output properties containing designer specified information--flow security properties as well as properties that demonstrate a design does not contain certain Common Weakness Enumerations (CWEs).