International Defense Security & Technology Your trusted Source for News, Research and Analysis
The Department of Defense (DOD) relies heavily on software systems for its critical missions, including national security and defense operations. However, software systems are inherently prone to defects and vulnerabilities that can compromise their integrity, security, and reliability. To address this challenge, DARPA is investing in a nascent discipline known as proof engineering. Proof engineering aims to create higher levels of assurance that will help critical DOD software systems remain free of certain classes of defects and vulnerabilities.
Engineering practices for software-reliant systems have evolved steadily over many decades, and so too have the assurance techniques that confirm systems’ correctness and security.
Proof engineering employs formal methods, which are mathematically rigorous techniques that use logic and mathematics to reason about software systems. Formal methods can help identify and eliminate certain types of defects and vulnerabilities that are difficult to detect through other methods, such as testing and static analysis. Proof engineering focuses on the development and management of mathematical proofs that demonstrate the correctness and security of software systems with respect to certain properties and requirements.
Formal methods, a set of mathematical techniques for specifying and verifying software and hardware systems, have been gaining traction in recent years as a way to improve the reliability and security of critical systems. By providing rigorous and systematic methods for reasoning about the behavior of complex systems, formal methods can help ensure that systems meet their intended specifications and are free from bugs, errors, and vulnerabilities.
Formal methods for system assurance have a long and rich history spanning over half a century. Even in the early days of computing, there were efforts directed at mathematical specifications and proof of properties of programs. These efforts were motivated by the emerging uses of computing software and hardware in critical systems, such as space or aircraft flight control, communication security, or medical devices. To this end, several US agencies invested in research in formal methods.
For deeper understanding of Formal methods and applications please visit: Comprehensive Guide to Formal Methods for Software Assurance: Theory, Practice, and Case Studies
One notable example of the successful application of formal methods is the seL4 microkernel, which is used in a range of critical systems, including defense systems, medical devices, and autonomous vehicles. The seL4 kernel was formally verified using the Isabelle/HOL theorem prover, which allowed for the detection and elimination of subtle bugs and security vulnerabilities that would have been difficult or impossible to detect through traditional testing methods. The seL4 project demonstrated that formal methods can be applied at scale to verify complex systems, and provided a model for the use of formal methods in the development of safety-critical systems.
Another example of the successful use of formal methods is in the design and verification of cryptographic protocols. Cryptographic protocols are used to secure communications over networks, and errors or vulnerabilities in these protocols can have serious consequences. Formal methods have been used to verify the correctness and security of widely used protocols, such as SSL/TLS, SSH, and DNSSEC. For example, the ProVerif tool has been used to verify the security of the TLS 1.3 protocol, detecting and eliminating several subtle security flaws.
Formal methods have also been applied in the field of autonomous vehicles, where the safety and reliability of these systems are critical. The HACMS (High-Assurance Cyber Military Systems) project, a joint effort between DARPA and Galois, used formal methods to verify the correctness of the software running on a quadcopter drone. The project demonstrated that formal methods can be applied to autonomous systems to ensure their safety and reliability, and provided a framework for the use of formal methods in the development of autonomous vehicles.
However, for decades, formal methods tools and ecosystems could only operate on problems and systems of modest scale. But recently, there have been revolutionary advances in tools, practices, training, and ecosystems that have facilitated the application of formal methods at larger scales. This has pointed to the existence of a tipping point for the scalability and usability of formal methods in a manner that is affordable and accessible to traditional software developers and engineers.
DARPA launched in April 2023 Pipelined Reasoning of Verifiers Enabling Robust Systems (PROVERS) program, with the goal to develop formal methods tools that are fully integrated into pipelined software development and maintenance processes. This will enable higher levels of assurance that software systems are free of certain defects or security issues. These formal methods tools will be designed for software engineers who are not formal methods experts in verifying a system’s properties. Tooling will be integrated into a development pipeline, enabling a continuous flow of capabilities over time while maintaining high assurance.
PROVERS is organized to advance proof engineering technologies and integrate these technologies into software development pipelines where they become more accessible to traditional developers without formal method backgrounds. Well-specified use cases, proposed by PROVERS performers, will provide the context for experts to advance program verification and proof repair technologies.
PROVERS builds off the Proof Engineering, Adaptation, Repair, and Learning for Software (PEARLS) AI Exploration project, which demonstrated how AI and machine learning could support and automate the generation and maintenance of proofs used in the formal verification of software at large scale.
The ultimate goal of proof engineering is to provide a level of assurance that critical software systems are free of certain classes of defects and vulnerabilities, such as those that can be exploited by malicious actors. By leveraging formal methods and mathematical proofs, proof engineering can help ensure that software systems behave as intended and that they meet their intended requirements and specifications. This can enhance the reliability, security, and trustworthiness of critical DOD software systems, ultimately helping to protect national security and defense interests.
Technical Areas
PROVERS has three technical areas (TAs): Proof Engineering (TA1), Platform Use Cases (TA2), and Cybersecurity Vulnerabilities (TA3). TA1 focuses on advancing proof engineering technologies and integrating these technologies into modern software development processes. TA2 provides platform use cases for assessing TA1 capabilities, and TA3 focuses on assessing the cybersecurity vulnerabilities of the TA2 platform use cases.
TA1 has three sub-areas: Scalable Automation (TA1.1), Workflow Integration (TA1.2), and Continuous Feedback (TA1.3). TA1 performers will leverage their developed capabilities in concert with TA2 performers and associated use cases.
Scalable Automation should develop proof engineering tools to guide software engineers through designing proof-friendly software systems and to reduce the proof development and repair burden. Developed capabilities should address challenges of scalability and usability, as well as increasing the range of properties that can be proven using formal methods tools.
Workflow Integration should enable proof engineering to fit within existing software development and maintenance workflows, providing a seamless experience for engineers without formal methods backgrounds. The continuous feedback sub-area should provide feedback mechanisms to software developers and engineers on the results of formal methods analyses.
The PROVERS program recognizes the importance of integrating formal methods into existing software engineering workflows. To achieve this, TA1.2 aims to integrate new and existing TA1.1 tools with widely-used tool chains consistent with common defense industrial base workflows.
One important aspect of this integration is to ensure that changes made to code are automatically reflected in associated proofs. The PROVERS program is working towards this by developing Proof repair tools that can automatically update proofs when changes are made to the code. These tools can break down large changes into smaller pieces, encouraging scalable automation. Recent work in this area includes the secure implementation of the Transport Layer Security protocol using continuous verification and tooling for analyzing cryptography. Other research has focused on identifying changes and factoring them into smaller parts to support proof repair automation.
TA1.2 aims to provide a continuous flow of enhanced capabilities, with tools engineered to ensure that (re)assessment effort is comparable to the effort of maintaining the software. The goal is to enable developers to seamlessly integrate formal methods into their workflows. Recent developments in the domains of cryptography and static analysis, which have transitioned from research into commercial practice, serve as a guide for PROVERS efforts.
By taking a developer/analyst-oriented approach, formal reasoning methods can be adapted to help developers and analysts. This will allow PROVERS to provide the seamless integration of formal methods into modern engineering workflows, including the (semi) automated repair and long-term proof maintenance in both models and code. Ultimately, the goal is to make proof engineering tools accessible to DIB-developers by designing and developing user interfaces and tools that match their intuitions and expectations.
In conclusion, the PROVERS program is working towards integrating formal methods into existing software engineering workflows. The development of Proof repair tools that can automatically update proofs when changes are made to the code is an important step towards achieving this goal. By taking a developer/analyst-oriented approach, the PROVERS program aims to seamlessly integrate formal methods into modern engineering workflows and make proof engineering tools accessible to DIB-developers. The development of such tools is an important step towards improving software security and resilience.
PROVERS aims to enable traditional software developers and engineers to use formal methods tools to increase the assurance of software systems. With the advances in tools, practices, training, and ecosystems, formal methods are becoming more accessible and affordable to traditional software developers and engineers. By integrating formal methods tools into software development and maintenance processes, PROVERS aims to provide higher levels of assurance that software systems are free of certain defects or security issues. This will enable the development of more robust and secure software systems that are vital to critical systems such as space or aircraft flight control, communication security, or medical devices.
Proof engineering will help developers construct software safely and ensure the software meets specified assurance requirements. DARPA’s Pipelined Reasoning of Verifiers Enabling Robust Systems (PROVERS) program will develop formal methods tools to guide software engineers through designing proof-friendly software systems and reduce the proof repair workload.
The goal of PROVERS is to make formal methods accessible to non-experts (e.g., traditional software developers and systems engineers) while minimizing the impact on their existing processes and performance. Furthermore, the tooling would integrate into a development pipeline enabling a continuous flow of capabilities over time while maintaining high levels of assurance.
PROVERS is a 42-month program spanning three phases that encompasses proof engineering, platform development, a red team to emulate potential adversaries’ attacks, and a separate federally funded research and development center to provide quantitative evaluation and evidence curation.
