Explosive Overflow: Lessons From Rocket Science

The talk revisits the 1996 maiden flight of the Ariane 5 rocket, which self-destructed about 39 seconds after liftoff. The speaker traces the failure to an inertial reference module carried over unchanged from the earlier Ariane 4. A velocity value that the faster new rocket produced overflowed a narrower integer type. The error handler shut the unit down, the identical backup failed the same way, and the flight computer read the diagnostic data as real velocity, forcing the vehicle off course.

The speaker lists the contributing causes: reused legacy code, untested design assumptions, an alignment routine that kept running after liftoff although it was no longer needed, and exception handling that treated software errors as random hardware faults. The talk then turns to what it means to prove software correct. It covers formal verification, including its cost and limits, the halting problem, and Gödel's incompleteness results. It also compares memory-safe languages, noting Ada's earlier mandate for critical weapons systems and the practical difficulty of rewriting large C and C++ codebases.

For practitioners, the main takeaways are to triage static analysis output instead of handing developers thousands of raw findings, to enable compiler sanitizers even in legacy projects, and to make secure defaults and vetted libraries the easy path. The Q&A also touched on seL4 and fuzzing tools. The overall message is to treat reused code and undocumented assumptions as risks that need testing against realistic inputs.