Researchers pick Galois for military trusted computing hardware and software design and development tools
ARLINGTON, Va. – U.S. military researchers needed hardware and software design and development tools to guarantee that software is running correctly by combining formal methods and side-channels. They found a solution from Galois Inc. in Portland, Ore.
Officials of the U.S. Defense Advanced Research Projects Agency (DARPA) in Arlington, Va., announced a $12.6 million contract to Galois earlier this month for the Continuous-correctness On Opaque Processors (COOP) program to develop new trusted computing approaches.
Galois will develop secure design and development tools and techniques to guarantee that software is running correctly if and only if the device physics is correct by combining formal methods and side-channels to unify computer science and physics.
COOP solutions will guarantee software correctness on any digital processor with low overhead. Analog and mixed-signal hardware are of interest, but only after achieving program goals for digital hardware.
Reliability physics is grounded in mathematics and can serve as the rigorous, stable, and tautological basis for formal analysis. Still, side-channels only can detect errors; they cannot correct the errors.
Today's safety-critical system design principles such as triple modular redundancy with majority voting or n-variant redundancy could detect, isolate, and correct errors continuously, but the performance penalties are prohibitive for mass deployments.
The solution lies in developing new techniques that can achieve revolutionary improvements in continuous-correctness guarantees and performance.
The COOP program uses these definitions:
-- availability, or the ability to guarantee that data, information, and processing can be accessed by authorized entities when needed;
--confidentiality, or the ability to guarantee that data, information, processing, etc., are not disclosed to unauthorized entities; --continuous-correctness, or the ability to identify and correct errors over time within program metrics;
-- control boundary, or the physical and logical boundaries between what the COOP solution can control, and what the solution has shared or no control;
-- correct, or computation is correct if the computation output as expected in time and value;
-- digital-side-channel, or manifestations of software running on hardware that is not physical;
-- error, or a condition that makes the computational output incorrect;
-- formal methods, or tools and techniques that provide rigorous mathematical proofs of specified properties;
-- informal methods, or tools and techniques that are logical and rigorous but that do not require mathematical proof;
-- integrity, or the ability to guarantee that data, information, and processing are not altered by unauthorized entities;
-- mission-critical software, or any software that requires continuous-correctness guarantees;
-- multi-modal-side-channel, or a combination of one or more distinct side-channels plus zero or more digital-side-channels;
-- oracle, or an abstraction in formal methods to represent the axiomatic source of correct answers;
-- opaque, or hardware or software with information about its behavior documented and known;
-- processor, or digital hardware that runs software; proof, or an independently verifiable argument using mathematics;
-- reference monitor, or a trusted entity that enforces control boundaries by completely mediating accesses; and
-- side-channel, or physical manifestations of software running on hardware.
Related: Trusted computing: application development, testing, and analysis for optimal security
Galois engineers will develop a threat model that is expected to change, as control boundaries depend on the proposed solutions. A COOP solution that completely mediates all accesses between a processor and the rest of the system can assume that only the processor and non-mission-critical software are untrusted.
The opaque processor and non-mission-critical software components are free to attempt to violate the computational integrity of mission-critical software as long as the goal is not a denial-of-service attack on the system, except when the denial-of-service vulnerability was newly introduced by the proposed approach. It is within the physical limitations of the components and behavior would not render the component commercially non-viable.
To ensure that COOP solutions can be integrated with processors that are manufactured separately, Galois will develop solutions between two system boundaries. COOP solutions could reside within a processor package, but not on the same die. COOP solutions also could reside within a computer case, but not outside where additional resources are available.
Potential embodiments of a COOP solution include integration within a processor’s package, co-located on a board, and independently located on a daughter card. Any proposed embodiment must be able to sense multi-modal side-channels within the computer case.
There are two program-identified technical challenges to COOP program goals: provable physics-based software error isolation; and continuous provable error correction. The COOP program is interested in tools and techniques that can provably isolate mission-critical software errors.
The first phase of the COOP program will demonstrate a solution on a general-purpose processor with multi-threaded cores in simulation. The second phase will demonstrate the COOP solution on real hardware.
On this contract Galois will do the work in Dayton and Columbus Ohio; Portland, Ore.; Tempe, Ariz.; Exton and Pittsburgh, Pa.; Irvine and San Francisco Calif.; Cambridge, Mass.; and Brooklyn, N.Y., and should be finished by April 2026.
For more information contact Galois online at https://galois.com, or DARPA at https://www.darpa.mil.
John Keller | Editor-in-Chief
John Keller is the Editor-in-Chief, Military & Aerospace Electronics Magazine--provides extensive coverage and analysis of enabling electronics and optoelectronic technologies in military, space and commercial aviation applications. John has been a member of the Military & Aerospace Electronics staff since 1989 and chief editor since 1995.
