QUIIP

Challenge

As Cyber Physical Systems (CPS) have grown exponentially more complex over time, the industry and government’s ability to thoroughly understand, test, and verify the correctness of these systems has failed to keep pace. Standard CPS design practices cannot catch defects during the early stages of system design, often resulting in significant system vulnerabilities that are not discovered until a system is already in the field. Fixing a problem this late in the game is significantly more time consuming and expensive than if addressed early in the design lifecycle. As a result, DoD acquisition programs have gone billions over budget and years past deadline time and time again.

At each level in hardware, software, and system design processes, CPS designers specify desired behaviors, including intended information flows. Unfortunately, due to the exponentially-growing complexity of modern CPS, these specifications are nearly always incomplete and inadequate – rough approximations rather than faithful, detailed models. Unbeknownst to the designers, incomplete specifications may permit information flows that support undesirable behaviors, leading to loss of confidentiality and integrity, and, ultimately, impact mission success.

For example, over the past several years, adversaries have been able to use side channel attacks to exploit unintended information flows in cryptographic operations, accessing both cryptographic keys and sensitive information. In the world of imagery and signal analysis, attackers can exploit logic bugs in hardware to inject information into the processing stream to, for example, hide illicit activities or military forces. Adversaries might also cause deadlock or delays, resulting in the mission-level collection decision missing its window of opportunity.

These sorts of flaws are deeply intertwined in today’s hardware designs and have proven difficult or impossible to fix after the fact with software and firmware patches. To meet today’s global challenges, the DoD needs to be able to develop and field resilient systems faster and cheaper.

Solution

With the QUantified Information flow for Intelligent Partitioning (QUIIP) program, Galois aims to solve this problem. Based on mission-critical safety and security properties that are specified in existing architectural models and supporting software implementations, this program drives these constraints into the hardware microarchitecture to formally verify that those constraints are satisfied during runtime execution. We 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 real CPS designs.

We will publish and deploy tools resulting from this effort on Galois’s Curated Access to Model-based Engineering Tools (CAMET) Library, an existing subscription service for model-based systems engineering tools. Current subscribers, including multiple Department of Defense (DoD) organizations as well as Defense Industrial Base (DIB) performers working programs such as the Future Vertical Lift (FVL), will have immediate access to these tools.

How Does it Work?

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 integrity guarantees and 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 (supporting logic and components within or to a processor). 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 integrity and confidentiality.

Value Add

• High Assurance Security and Correctness
• Faster Timelines and Lower Costs
• Scalable Formal Verification Solutions
• Knowledge Capture and Retention