Programming Languages for High-Assurance Vehicles

Explore a conference talk on developing secure autopilot systems using embedded domain-specific languages (EDSLs) in Haskell. Delve into the experiences of synthesizing a fully-featured autopilot for the DARPA High-Assurance Cyber-Military Systems (HACMS) program, which was deemed "the most secure UAV in the world" by a government official after independent red-team assessment. Learn about the process of transitioning these EDSLs to Boeing for use in large-scale platforms, and discover the open-source nature of both the EDSLs and the autopilot. Gain insights into debugging embedded systems, modern vehicles, full control, sandboxing, verification tools, and the diversity of properties in high-assurance vehicles. Explore topics such as embedded DSL, embedded Haskell, conditional expressions, automatic differentiation, algebra, type classes, safety cases, and lessons learned from red team analysis. Understand the importance of filtering and the benefits of open-source development in creating secure programming languages for high-assurance vehicles.