HACMS (High-Assurance Cyber Military Systems)
Galois has built two new domain-specific languages (DSLs) and used them to develop a "hack-proof", full-featured, unpiloted air system. The secret to our increased productivity and assurance was building embedded DSLs, in which the DSLs are libraries in Haskell. We generate embedded C code that is guaranteed to be memory-safe from a relatively small specification.
As part of DARPA’s High Assurance Cyber Military Systems (HACMS), Galois is building critical flight control software using new software methods for embedded systems programming. We demonstrated technology developed to-date under this program at DARPA I2O’s Demo Day on May 21, 2014, at the Pentagon. Read more about the program and what our team is doing in this article recently published on Signal Online.
The flagship application for the technologies we’ve developed under the HACMS program is called SMACCMPilot: a new flight controller for small quadcopter unmanned aerial vehicles (UAVs). SMACCMPilot is written in the Ivory language, a new domain-specific language for safe systems programming. We’ve built an ecosystem of libraries on top of the Ivory language, including a concurrency framework and drivers for microcontroller hardware. Ivory has a simple interface to external C code, which allows SMACCMPilot to re-use software components from the ArduCopter open source project.
We’ve also implemented communications protocol stacks and control primitives in Ivory. SMACCMPilot is currently alpha-quality software as we actively develop the flight control software itself and evolve the new technologies we’ve used to build it. We’ll be continuing work on the SMACCMPilot project for the next few years.
All of the software behind SMACCMPilot is open source and available on github, and documented on the project web site. We welcome collaboration with programming languages, formal methods, and flight control researchers!