Galois Awarded $12.6M by DARPA to support COOP Program

Galois was awarded $12.6 million by DARPA for HEIMDALLR (Hybrid Electromagnetic side-channel and Interactive-proof Methods to Detect and Amend LogicaL Rifts) to support the COOP (Continuous-correctness On Opaque Processors) program. Massachusetts Institute of Technology (MIT), New York University (NYU), Ohio State University (OSU), Carnegie Mellon University (CMU), Battelle, Niobium Microsystems, Riscure (a part of Keysight Technologies), and Ansys are all partnering with Galois on the project. 

Today, although mission critical software (MCS) in DoD equipment may be heavily tested or even formally proven correct, the correct execution of that software remains at risk due to interactions with the physical and software environment on which it runs. Currently, it is very difficult to assure trust about that external environment, which includes the processor and memory on which the software runs, because you only have control over the MCS. It is also difficult to assure trust about other portions of the software stack, such as the operating system and other programs that run in the same environment, which are likely commercial or otherwise “off-the-shelf”. 

With HEIMDALLR, Galois aims to solve this problem through an alternative approach that combines the power of formally-verifiable computation, rather than formally verified software, with the use of electromagnetic side-channel sensing to assure that errors in program flow or computation are provably identified, isolated, and corrected during execution.

To accomplish these goals, our process relies on trusted hardware called the HEIMDALLR InterProcessor (HIP), which performs several functions: First, HIP provides a physical control boundary between what is trusted (HIP memory, peripherals, power control) and what is not (the mission processor, system memory, and non-MCS code executing on the mission processor, such as the operating system), isolating errors from propagating to I/O devices or trusted computation results stored in HIP’s memory. Second, HIP measures and analyzes side-channel data (here, electromagnetic signals), comparing them to causal software mechanisms to isolate errors in program flow in MCS and verify flow control evidence. Third, HIP uses Verifiable Computation (VC) interactive proof (IP) methods to isolate errors in results of computations and verify that the target system executed MCS correctly. It then takes actions to either accept (allow propagation of) or reject (force re-execution of) MCS results. The HIP is a single piece of hardware that ensures commercial and off-the-shelf hardware and software cannot interfere with MCS. 

Together, each of these capabilities address the semantics of MCS execution – which instructions are executed, and whether each produces the expected result – with a high degree of mathematically provable soundness. Having detected and isolated errors, HEIMDALLR then enforces formally verified continuous correction of detected errors by preventing error propagation and forcing limited, low-latency MCS re-execution.

To learn more, check out the HEIMDALLR project page and stay tuned for more updates!

‍

Distribution Statement "A": Approved for Public Release, Distribution Unlimited