HEIMDALLR

Challenge

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.” 

Solution

With HEIMDALLR (Hybrid Electromagnetic side-channel and Interactive-proof Methods to Detect and Amend LogicaL Rifts), our project supporting DARPA’s Continuous-correctness On Opaque Processors (COOP) program, we propose an alternative approach that combines the power of formally-verifiable computation, rather than formally verified software, along 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.

Value Add

• Continuous Detection of Errors and Assurance of Correctness
• Efficient Isolation and Correction of Errors During Software Execution
• Improved Efficiency of Verifiable Computation Proofs of MCS Execution
• New & Improved Electromagnetic Approach for Sensing and Providing Evidence of MCS Program Control Flow
• First-of-its-kind Hybrid Approach to Error Detection

‍

‍

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