ARLINGTON, Va. – U.S. military researchers are asking industry to find new trusted computing approaches by developing hardware and software tools to guarantee that software is running correctly by combining formal methods and side-channels.
Officials of the U.S. Defense Advanced Research Projects Agency (DARPA) in Arlington, Va., issued a broad agency announcement this month for the Continuous-correctness On Opaque Processors (COOP) program.
COOP seeks to 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.
Related: Securing safety-critical software for avionics and other mission-critical systems
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.
Related: New frontiers in real-time software
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.
COOP 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, proposed COOP solutions must exist 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.
Related: Model-based design uses COTS tools for unmanned aerial systems development
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.
Companies interested should submit full proposals no later than 13 May 2024 to the DARPA Broad Agency Announcement Tool (BAAT) online at https://baa.darpa.mil/Public/SecurityAgreement. Email questions or concerns to [email protected]. More information is online at https://sam.gov/opp/bfee586f95dc4b47bcd56972bb71f234/view.
