The goal of the research is to develop technology for the construction of embedded computer systems that are “functionally correct and satisfy appropriate safety and security properties”, explained Kathleen Fisher, DARPA’s program manager for the project, known as the High-Assurance Cyber Military Systems (HACMS) program.
HACMS will adopt a clean-slate, formal methods-based approach to enable semi-automated code synthesis from executable, formal specifications, DARPA explained. In addition to generating code, HACMS seeks a synthesizer capable of producing a machine-checkable proof that the generated code satisfies functional specifications as well as security and safety policies.
The agency said a key technical challenge will be the development of techniques to ensure that such proofs are composable, allowing the construction of high-assurance systems.
Technologies that will be developed include interactive software synthesis systems, verification tools such as theorem provers and model checkers, and specification languages.
If successful, HACMS will produce a set of publicly available tools integrated into a high-assurance software workbench, which will be distributed for use in both the commercial and defense software sectors. HACMS intends to use these tools to generate open-source, high-assurance, and operating system and control system components and use these components to construct military vehicles.