Correct by Construction for LSCOA

A New Take on an Old Technique Is Neutralizing Cyber Threats Before They Materialize

Col. Trent Mills, Maj. Nikesh Kapadia and Robert Price, Lt. Col., USA (Ret.)

Article published on: July 1, 2025 in the Army AL&T Summer 2025 Issue

Read Time: < 7 mins

CLEAR TO FLY
The Army MX Autonomous Test Platform configured with Launched Effects options. (Photo by Sgt. David Resnick, Office of the Secretary of the Army)

Are we willing to accept the risk of adversaries adapting cyberattack tactics, techniques and procedures (TTPs) faster than we can push new software updates? Are we willing to expose the warfighter in comms-sensitive environments to the risk of unverified software updates that may break their system?

In today's dynamic digital environment, these questions demand foolproof solutions. Yet the DOD has been conditioned to accept vulnerable software. We have resigned ourselves to a learned helplessness that defaults to applying patches after discovering software vulnerabilities. In protracted, large-scale combat operations (LSCO), this resignation will translate into catastrophe on the battlefield. However, solutions exist now to secure Army systems. It's just a matter of knowing what they are and how to apply them.

Urgent Need for Software Fortification

The continued success of our Human-Machine Integrated Formation efforts, highlighted at the Project Convergence Capstone 5 demonstration in March 2025, will paradoxically invite our adversaries to strike where we are weakest: Our networked computers on wheels and ubiquitous uncrewed systems. Our creativity and willingness to integrate robots and advanced software into our formations will provide additional attack surfaces for our adversaries to exploit.

In July 2024, the former Army Secretary, Hon. Christine Wormuth, flew on a fully autonomous UH-60A called Aircrew Labor In-Cockpit Automation System (ALIAS), 54 Army AL&T Magazine Summer 2025 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. The 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) quadcopter 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. These 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 software, but these capabilities are rarely scaled to DOD challenges. However, early DARPA-Army partnerships have pioneered how formal methods can secure cyber-physical systems: Think military systems that are a complex integration of analog, software 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 mathematical 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 reliance on software and hardware in critical systems, such as space and aircraft flight control, critical infrastructure, communication security and medical devices.

PROCESS FOR SUCCESS
DARPA's Resilient Systems Portfolio consists of programs with a shared vision to increase the survivability of our military systems. This chart highlights examples of formal methods techniques based on maturity level (vertical axis) and ways to implement them (horizontal axis). (Graphic courtesy of Matthew Wilding, DARPA)

The Army Prepares for the Next Fight

In 2016, the HACMS "edge" case included a malign actor using a USB stick to hijack an Army system. At the beginning of the program, the HACMS red team could hack into the H-6U onboard flight-control computer and take control of the entire system. Then, the HACMS blue team modified the H-6U using formal methods and gave the same red team six weeks of unfettered access to the H-6U. They couldn't hack it. The red team was then given access to a non-essential partition of the helicopter as a way in, but the red team could not expand access or disrupt operations. In other words, the front door of the bank was open, but they did not have the combination to the vault. Perhaps more importantly, the safety pilots of the H-6U did not know the system was hacked as it maintained full functionality. To demonstrate durability of the solution, DARPA offered the same HACMS 2016 quadcopter to hackers at the premier defense hacking conference, DEF CON, for another go. They also failed. Formal methods can secure DOD systems now. If inclined, the Army could proactively apply formal methods to the Autonomous Resupply Vessel before it rolls off the production line, or the Navy could reinforce the 240-ton DARPA autonomous vessel called USX-1 Defiant (conducting sea trials in 2025). But the scope doesn't have to be limited to just future systems; rather, formal methods can be applied to legacy systems warfighters rely on today.

Formal methods can minimize software updates for networkconnected capabilities. Doing so would increase survivability by extending the time Army systems can operate in no-comms environments.

"Formal methods are the best route to shift security from a reactive practice to a proactive guarantee that we can build upon to gain advantages in the DOD," said Mark A. "Al" Mollenkopf, science advisor to the U.S. Army Cyber Commanding General.

The Army can make protracted LSCO possible—think secure and survivable weapons systems, transport platforms, critical infrastructure and lines of communication that are ready for the next fight.

Rapid action to implement formal methods tools in current and future systems can dramatically reduce the DOD's software vulnerabilities. In fact, DARPA estimates that broad application can eliminate 80 to 90% of our military's cyber vulnerabilities.

"Formal methods application should start at the outset of the formal requirements process to secure our weapons systems and other platforms," said Maj. Gen. Jake S. Kwon, director of Strategic Operations, Headquarters, Department of the Army G-3/5/7. "We can ill afford to retrofit our weapons systems after they're fielded. As formations continue to experiment with COTS solutions and coding at the edge, formal methods provide a clear advantage in securing our innovation efforts."

Assurances in the Future Operating Environment

Although formal methods offer many benefits, they are not a silver bullet. The adversary has a vote and is already enhancing their cyberattack TTPs.

Future Army systems increasingly rely on artificial intelligence (AI)-based technologies to propel the capabilities of robotics and decision support tools towards the complex military scenarios in the future. However, large neural network architectures and foundational models create new opportunities for adversaries to corrupt data feeds and exploit underlying algorithms. DARPA is exploring how we can secure these emerging AI technologies. Moreover, the Army can help them understand the future operational concepts and lean forward on new requirements to build assurances for our future military systems. These assurances will ensure that military AI-based systems perform as expected in complex and dynamic battlefields.

Conclusion

The Army and DARPA are collaborating on a capstone application of formal methods. Instead of a single platform, the Army is considering an entire acquisition line. The Air Force and Navy are also participating. In the aggregate, these capstone efforts will signal that the DOD Enterprise understands the software vulnerabilities underpinning the Interim National Defense Strategy and supporting warfighting concepts, and serves as a leap forward in creating learned resilience across the joint force.

For more information, go to https://www.darpa.mil/research/ research-topic-spotlights/formal-methods.