CORRECT BY CONSTRUCTION FOR LSCOA
a program run by the Defense Advanced Research Projects Agency (DARPA) and transitioned to the Program Executive Office for Aviation in December 2024. When the flight ended, she approached the Army’s own autonomous UH-60L test vehicle (MX) outfitted with the latest launched effects capabilities. Her first question was how to protect the autonomous systems from being hacked and used against us. Te DARPA director at that time, Stefanie Tompkins, told Wormuth about a DARPA program called High-Assurance Cyber Military Systems (HACMS). HACMS proved unequivocally that a Boeing unmanned little bird (H-6U) and a commercial off-the-shelf (COTS) quadcop- ter circa 2017 could be protected from attacks even when the hackers had full access to the system for months using formal mathematical methods, also called formal methods. Last year, the Army applied formal methods to secure a Polaris MRZR in another DARPA test under the program, Assured Micropatching. Tese examples of collaboration join several others over the past decade, but their successes are disparate, small-scale and largely unharnessed by the services.
WHY FORMAL METHODS, AND WHY NOW? For years, industry has used formal methods to verify soft- ware, but these capabilities are rarely scaled to DOD challenges. However, early DARPA-Army partnerships have pioneered how formal methods can secure cyber-physical systems: Tink military systems that are a complex integration of analog, soft- ware and hardware components working together to deliver a warfighting capability. Formal methods are mathematically rigorous techniques that ensure code is free from errors and, thus, cyber vulnerabilities. For those who don’t speak in terms of parsers and kernels, formal methods are the checklist and math- ematical proofs (i.e., guarantees) that ensure a system does what it is specified and verified to do.
When building a bridge, instead of hoping it will not collapse, the engineer uses strict mathematical calculations to prove it will not. Before DARPA’s advancements, such tools for existing software development pipelines were out of reach. Today, they’re within reach and when applied to an Army system like the MRZR, formal methods demonstrated that even if a red team hacked the system, the hacker could not make the MRZR do something the blue operator did not approve.
Recent advances in formal methods tools, practices, training and ecosystems, combined with dramatically increasing computing capabilities, make applying formal methods at larger scales more affordable than ever. Today, various U.S. government agencies and industry leaders invest in formal methods due to the growing
54 Army AL&T Magazine Summer 2025
reliance on software and hardware in critical systems, such as space and aircraft flight control, critical infrastructure, commu- nication security and medical devices.
The Army can leverage investments made by DARPA’s Resilient Software Systems portfolio to secure systems:
• Assured Micropatching (AMP) tools sustain binary-only embedded software and firmware for which source code is no longer available.
• Automated Rapid Certification of Software (ARCOS) automates the evaluation of soft- ware assurance evidence to enable certifiers to determine the risk of software deployment is acceptable.
• Cyber Assured Systems Engineering (CASE) tools provide necessary design, analysis and verification tools to allow system engineers to design in cyber resiliency.
• SafeDocs tools verify data coming in and out of systems and their components.
• Verified Security and Performance Enhance- ment of Large Legacy Software (V-SPELLS) tools enable modernization of large legacy soft- ware systems.
The Army can help guide the operational direction of DARPA’s new assurance programs:
• Assured Neuro Symbolic Learning and Reason- ing (ANSR) develops novel algorithms that integrate contextual understanding to build safety and trustworthy military systems.
• Pipelined Reasoning of Verifiers Enabling Robust Systems (PROVERS) makes formal methods accessible to the engineers and inte- grates tools into the design process.
• Safe and Assured Foundation Robots for Open Environments (SAFRON) seeks new approaches to ensure Foundation Model-controlled robots perform as directed by warfighters.
• Securing Artificial Intelligence for Battlefield Effective Robustness (SABER) seeks to oper- ationalize adversarial-AI techniques and red teams to assess emerging military systems.
Page 1 |
Page 2 |
Page 3 |
Page 4 |
Page 5 |
Page 6 |
Page 7 |
Page 8 |
Page 9 |
Page 10 |
Page 11 |
Page 12 |
Page 13 |
Page 14 |
Page 15 |
Page 16 |
Page 17 |
Page 18 |
Page 19 |
Page 20 |
Page 21 |
Page 22 |
Page 23 |
Page 24 |
Page 25 |
Page 26 |
Page 27 |
Page 28 |
Page 29 |
Page 30 |
Page 31 |
Page 32 |
Page 33 |
Page 34 |
Page 35 |
Page 36 |
Page 37 |
Page 38 |
Page 39 |
Page 40 |
Page 41 |
Page 42 |
Page 43 |
Page 44 |
Page 45 |
Page 46 |
Page 47 |
Page 48 |
Page 49 |
Page 50 |
Page 51 |
Page 52 |
Page 53 |
Page 54 |
Page 55 |
Page 56 |
Page 57 |
Page 58 |
Page 59 |
Page 60 |
Page 61 |
Page 62 |
Page 63 |
Page 64 |
Page 65 |
Page 66 |
Page 67 |
Page 68 |
Page 69 |
Page 70 |
Page 71 |
Page 72 |
Page 73 |
Page 74 |
Page 75 |
Page 76 |
Page 77 |
Page 78 |
Page 79 |
Page 80 |
Page 81 |
Page 82 |
Page 83 |
Page 84 |
Page 85 |
Page 86 |
Page 87 |
Page 88 |
Page 89 |
Page 90 |
Page 91 |
Page 92 |
Page 93 |
Page 94 |
Page 95 |
Page 96 |
Page 97 |
Page 98 |
Page 99 |
Page 100
