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.

Intro
Debugging
Embedded Systems
Modern Vehicles
Full Control
Sandboxing
Verification Tools
Diversity of Properties
DARPA
Embedded DSL
Embedded Haskell
Embedded Concrete
Conditional Expressions
Automatic Differentiation
Algebra
Type Classes
Automatic Appreciation
safety case
road show
Red team analysis
Lessons learned
Filtering
Open Source