Researchers and hackers have shown that all kinds of networked embedded systems from your computer to medical devices to your car are vulnerable to remote attack, and such attacks can cause physical damage while hiding the effects from monitors.
To help counter this threat, DARPA has created the High-Assurance Cyber Military Systems (HACMS) program.
The goal of the HACMS program is to create technology for the construction of high-assurance cyber-physical systems, where high assurance is defined to mean functionally correct and satisfying appropriate safety and security properties. Achieving this goal requires a fundamentally different approach from what the software community has taken to date.
According to DARPA, HACMS will adopt a clean-slate, formal methods-based approach to enable semi-automated code synthesis from executable, formal specifications. 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.
In the video below, DARPA Program Manager Dr. Kathleen Fisher outlines the objectives of the High-Assurance Cyber Military Systems (HACMS) project.