Programming Languages for High-Assurance Vehicles

### Overview The talk addresses the persistent security weaknesses in embedded and cyber-physical systems, noting that despite exponential increases in system complexity and networking (such as modern vehicles with dozens or up to 100 ECUs networked over CAN buses and wireless interfaces), developers remain reliant on 1970s-era tools like C, C++, and basic debugging. Highlighting landmark automotive hacks (such as research from University of Washington, UC San Diego, and work by Charlie Miller and Chris Valasek), the speaker emphasizes that attackers routinely gain full vehicle control through remote interfaces using classic vulnerabilities like buffer overflows. Standard solutions such as sandboxing, traditional hypervisors, and full functional languages like Haskell or OCaml fall short due to resource constraints on microcontrollers, real-time concurrency demands, and the lack of runtime predictability.

### Key Topics - **DARPA HACMS Program**: The High Assurance Cyber Military Systems program, initiated under Kathleen Fisher, aimed to build high-assurance software from scratch, starting on small airframes (quadrotors) and transitioning to military platforms like Boeing's Unmanned Little Bird helicopter. - **Embedded Domain-Specific Languages (eDSLs)**: Rather than writing a new language compiler from scratch (impractical at the time, given Rust was pre-1.0) or shrinking massive language runtime systems, the team created Haskell-embedded DSLs to generate safe C code. - **The Ivory Language**: A sub-Turing complete embedded DSL designed for low-level embedded systems that enforces memory and type safety, prevents null pointer dereferencing, and uses Haskell as a compile-time, type-safe macro language. - **Concurrency and System Architecture with Tower**: A companion DSL developed to generate communication glue code, inter-process communication (IPC), monitor-style concurrency, and Architecture Analysis & Design Language (AADL) architectural models targeting verified operating systems such as seL4 and eChronos.

### Technical Details - **Ivory Design and Syntax**: Ivory provides compile-time guarantees, such as tracking allocation scopes (local vs. global) with type variables, non-null references, and safe array iteration (`arrayMap`) that eliminates buffer overruns. To facilitate adoption by C++ systems engineers at Boeing, the team designed a concrete C-like syntax over Ivory, allowing them to rewrite flight controllers and mission computers with minimal assistance. - **Type-Safe Macros and Automatic Differentiation**: Ivory leverages Haskell's type system to define higher-level abstractions without expanding the core language. For example, custom conditional syntax (`cond`) can be implemented in a few lines. By taking advantage of Haskell's numeric type classes (`num`), developers used forward automatic differentiation libraries directly on Ivory ASTs to automatically generate Jacobian matrix computation in C for Kalman filters in an inertial navigation system. - **Target Platforms and Red Team Testing**: The software pipeline targeted multiple RTOS environments (POSIX, FreeRTOS) and compiled via AADL "trusted builds" to the seL4 formally verified microkernel and eChronos. During DARPA evaluation, red teams were provided full source code, specifications, and hardware for two months. They were unable to penetrate the vehicle's network, finding only minor physical attack surface flaws (an open debug port) and unverified assertions. The resulting platform was demonstrated at the Pentagon and featured on 60 Minutes.

### Takeaways - **Comprehensive Engineering Beyond Formal Proofs**: Formal verification must be paired with standard software hygiene, including fuzzing, regression testing, continuous integration, code reviews, and defensive practices like network message filtering and eliminating insecure remote flashing conveniences. - **Co-evolving Architecture and Code**: Generating AADL architectural models directly from the Tower DSL ensured models stayed strictly synchronized with compiled implementations, preventing model-code drift. - **Open Cyber-Physical Challenges**: Hard problems remain in global toolchain integration and cyber-physical failover—such as safely handling real-time failures or attacks on physical vehicles with spinning blades that cannot simply be powered down like traditional IT servers.