Revolutionizing Cyber Resiliency for Military Systems
DOD's Aging Assets: A Critical Vulnerability
The Department of Defense’s (DOD) reliance on aging IT infrastructure, using security standards developed over the last 30 years, creates inherent vulnerabilities in its systems, from legacy architectures to advanced weapons.
Adversaries like Volt Typhoon are actively exploiting these vulnerabilities, gaining access to critical infrastructure. They are also stealing and re-engineering sensitive military system source code.
A Proven Solution: Formal Methods
Technology exists today to minimize exploitable software vulnerabilities.
- What it is: DARPA has developed scalable tools based on formal mathematical methods (formal methods) to secure and prove the absence of exploitable vulnerabilities.
- How it works: Rather than validate the security of software code solely by testing it after it’s already written, formal methods’ mathematically based software development approach designs software through rigorous mathematical analysis, verifying its performance before and as it’s being built. As a result, software does what it's supposed to and doesn't do what it's not supposed to, making it inherently more secure.
- Proof of concept: Our High-Assurance Cyber Military Systems (HACMS) program successfully applied formal methods to military systems like quadcopters, helicopters, and automobiles – making them inherently secure against cyber threats. | Read the case study.
- Transition: Many of these tools and techniques have transitioned to the services for further maturation and operational use but broad adoption is needed to dramatically improve overall DOD cybersecurity.
- Future plans: We want to create a sustainable ecosystem of formal methods tools that are ready to use, while continuing to advance the state of the art.
Why it Matters
- Formal methods tools and techniques are universally applicable and can drastically improve the security of the DOD's vast catalog of deployed legacy code and secure future systems.
- Rapid implementation of these tools in legacy and future systems can significantly reduce the DOD's cyber vulnerabilities.
- Cyber-hardened systems help the warfighter complete their missions successfully.
At DEF CON 32, I2O Office Director Kathleen Fisher presented, “Closing the Software Vulnerability Gap.”
Research Spotlight
Case Study
HACMS: High-Assurance Cyber Military Systems
Event
Resilient Software Systems Colloquium
June 17, 2025
Hyatt Regency Crystal City
Arlington, Va.
Registration deadline: May 26, 2025
Resources
Programs
Featured program: Safe Documents
- AMP: Assured Micropatching
- ARCOS: Automated Rapid Certification Of Software
- CASE: Cyber Assured Systems Engineering
- CPM: Compartmentalization and Privilege Management
- E-BOSS: Enhanced SBOM for Optimized Software Sustainment
- PROVERS: Pipelined Reasoning of Verifiers Enabling Robust Systems
- TRACTOR: Translating All C to Rust
- V-SPELLS: Verified Security and Performance Enhancement of Large Legacy Software
Videos
Watch the 12 demonstrations in this playlist. Try expanding videos to full window.
Formal Methods Examples
Parsers
Parsers are software components that serve as the "trusted gatekeepers" of high-assurance software; computer programs rely on them to consume input from untrusted sources.
seL4 microkernel
The secure embedded L4 (seL4) is compact and simple kernel-based software that runs multiple machines at once, providing the highest assurance of isolation between applications running in the system.
AADL
The Architecture Analysis and Design Language (AADL) is an example of model-based system engineering (MBSE) that uses formal language and automation, making the software development process efficient, rigorous, and repeatable.
Open-source Tools
The following tools were developed under DARPA programs and range in functionality and specificity for a variety of uses. We will add additional tools here as they become available.
Last updated on April 8, 2025.
Data formats, auto-generating parsing code
- DaeDaLus
Data description language for defining data formats and generating memory-safe parsers in a variety of languages.
- Hammer
Declarative secure parser/scanner construction kit in C.
- Parsley
Data description language to capture data formats.
Document collections, format rules
- File Observatory
System to enable visualization, search, discovery of complex file format patterns/data.
- Format Analysis Workbench
Runs/analyzes output from any number of parsers dealing with a single file or streaming format.
- Dowker tools
Tools for statistical inference of file format behaviors.
- PolyFile
Identifies/maps the semantic structure of files.
Behavior of existing parser code
- PolyTracker
Data/control-flow analysis for programs.
- GraphTage
Command-line utiility/underlying library for semantically comparing/merging tree-like structures.
- Fickling
Decompiler, static analyzer, bytecode rewriter for Phython pickle object serializations.
- Arlington PDF Model
Document object model for PDF to enhance security/drive new modalities in specifications.
- Digital Corpora Project Corpus
8 million real-world PDFs.
- SPARCLUR
Collection of various wrappers for extant PDF parsers/renderer & output comparison/analysis tools.