GALOIS, INC. — Department of Defense SBIR Phase II: A17-006

Description

Due to exponential growth in complexity, current hardware designs cannot be thoroughly tested, which leads to significant hardware vulnerabilities reaching the field. Recent innovations in Model-Based Engineering (MBE) provide information flow analysis results that can be used to drive design state space partitioning – separating the design into multiple, individually verifiable portions – based on existing mission requirements. Advances in formal methods and symbolic execution allow us to formally analyze the resulting partitions to guarantee that mission requirements, such as security classification boundaries, are satisfied. This partitioning will reduce the complexity of what must be formally analyzed, allowing the techniques to scale from small microcontrollers to complete System on Chips (SoCs) with multiple heterogeneous processor cores, accelerators, and uncore components. The techniques also include a new quantitative measure of the complexity of achieving the partitioning, providing developers with guidance on where the design can be optimized for performance while preserving security. In this Phase II project, we will show that our partitioning approach makes it possible to reduce the state-space explosion problem of mission-critical digital design verification. We will show that it is possible to partition key areas of microarchitecture designs based on application requirements captured in architecture-level models.  To accomplish this, we will derive information flow constraints based on mission-system architectural models and supporting software implementations, drive these constraints into the hardware microarchitecture, and formally verify that those constraints are satisfied. We will demonstrate the feasibility of applying these mission-driven constraints to help scale verification techniques to multi-core systems with heterogeneous accelerators.  The results will show that it is feasible to scale formal methods to hardware designs of 10M gates, which is a 50x improvement of the state of the art.