Abstract
A drone autopilot is a complex software artifact that includes operating systems, networking, and sensor systems. With support from DARPA, Galois is addressing the challenge of building an open-source high-assurance autopilot that is resistant to security attacks and software faults. We are tackling the problem by borrowing from a suite of formal-methods-inspired technologies such as strongly-typed domain-specific languages for embedded control systems, software model-checking, and runtime-verification.
Just over one year in, we have designed two new languages and compilers and have a provisional autopilot developed. I will describe how we have achieved low-cost high-assurance software, the challenges ahead, and the open problems we do not yet know how to address.
The autopilot and more information is available at smaccmpilot.org.