Accelerating New Capability Through Rapid Certifiable Trust

2021 Year in Review

Accelerating New Capability Through Rapid Certifiable Trust

In today’s military, as in most sectors, the line between computer and mechanical device has blurred. For such cyber-physical systems (CPS), new and critical capabilities come mostly by way of software rather than hardware. Rapid delivery of new capabilities to CPS helps maintain our nation’s strategic advantage. This demand for more rapid deployment, however, requires system verification techniques that can adapt to a faster deployment cadence.

CPS that are complex, involve unpredictable components such as machine learning, or are part of mission- and safety-critical systems can slow or stymie traditional verification techniques. Existing formal methods for verification do not scale to the level of assurance required, and existing testing methods are not reliable. “Department of Defense systems that interact with the physical world, like vehicles and weapons, need to be certified for safety-critical properties before they are deployed, and this certification process is complex and error prone,” said Dio de Niz, the SEI’s technical director of assuring CPS and lead of the project Rapid Certifiable Trust (RCT).

Our solutions make formal methods scalable by ensuring that infrequent but catastrophic erroneous CPS behaviors are monitored and guarded against without compromising capability.

Dio de Niz
Technical Director, Assuring Cyber-Physical Systems, SEI Software Solutions Division

De Niz and his team are developing techniques to automatically verify critical properties of CPS using scalable formal verification. The team comprises world-class researchers in timing, logic, security, and control verification and includes experts from Carnegie Mellon University, University of California Riverside, and Washington University in St. Louis. With help from these collaborators, the SEI developed an approach that leaves most of the software unverified and adds small pieces of verified code that enforce the safety-critical properties of interest. The system no longer needs to verify all the software code, only the enforcers.

“We created a new way to monitor and enforce the output of a system to evaluate whether the output is safe and, if not, replace it with a safe one,” said de Niz. “Our solutions make formal methods scalable by ensuring that infrequent but catastrophic, erroneous CPS behaviors are monitored and guarded against without compromising capability.”

Part of this effort is developing compositional verification techniques to allow operation of multiple enforced components, minimizing and automatically removing conflicting enforcer assumptions—for instance, reducing a plane’s airspeed to avoid a crash while increasing airspeed to prevent stalling. These techniques will allow the Department of Defense (DoD) to assure full-scale systems, even if most of their functionality is implemented by unverified components.

The SEI team has presented this work in 17 academic and industrial publications and conferences. It has also produced two open source projects: a real-time mixed-trust computing framework and a verified hypervisor.

The goal of RCT is to reduce the deployment time of CPS by reducing the overall development and assurance times. The technique enables the use of unverified commodity software components, such as open source drone piloting software, guarded by verified enforcers that guarantee the containment of unsafe component behavior. The DoD has long relied on bespoke components, but RCT opens the door to commodity components as a way to improve the rapid deployment of critical capabilities.