This presentation by Neil White and Rod Chapman from Altran discusses the critical need for developing software with ultra-low defect rates, contrasting the software industry's defect tolerance with other engineering disciplines. They introduce the SPARK programming system, a methodology and set of tools designed to enable the development of highly reliable and safe software through static verification. SPARK achieves this by using a subset of a language that eliminates ambiguity and undefined behaviors, integrating formal methods, contracts, and automated theorem proving to mathematically prove the absence of common bugs like buffer overflows and certain types of arithmetic overflows. The speakers illustrate SPARK's effectiveness with real-world examples from critical domains such as aerospace (helicopter landing, jet engine control), rail (backup signaling), finance (credit card key generation), and defense (secure access systems, air traffic control), highlighting systems with decades of operation and minimal reported defects. They emphasize that while tools are crucial, a "fumble programming" approach (formal methods coupled with humility) is necessary, acknowledging that human programmers inevitably introduce defects, and the tools are there to catch them early and reliably. The technology, including the SPARK tools, is available under a permissive license, encouraging its adoption in safety and security-critical applications.
Building Ultra-Reliable Software: The SPARK Approach
0:00 - 1:12 Altran's Mission: Neil White and Rod Chapman from Altran introduce their company's core mission: writing software correctly with ultra-low defects, aiming to raise the industry standard for acceptable defect levels.
1:12 - 2:22 High Defect Tolerance in Software: They highlight the unique tolerance for defects in the software industry compared to other mature engineering fields (mechanical, electrical), where failure is often unacceptable and not easily dismissed.
2:55 - 4:42 Critical Infrastructure Failure: A real-world example recounts a software failure in UK critical national infrastructure caused by an array index/buffer overflow bug, leading to widespread system outage and a public inquiry. They emphasize that testing alone is insufficient for preventing such rare but critical errors, while their methods design out such possibilities.
5:50 - 8:05 Introduction to SPARK: SPARK is presented not just as a programming language (similar to Pascal/VHDL), but as a comprehensive system including static verification tools and engineering disciplines, designed for bare-metal/ring-nought programming in systems where operating systems are not trusted or available.
9:24 - 12:14 Static Verification: The core concept is analysis of code (and other artifacts) without running it (non-dynamic verification/testing). Desired tool properties include soundness (no false negatives), completeness (few false positives), depth (finding hard bugs), speed (fast feedback), and modularity (analyzing parts). This approach prevents entire classes of defects and can reduce or eliminate the need for certain testing activities (like unit testing).
15:39 - 17:31 Language Ambiguity is a Problem: Ambiguity and undefined behavior in widely used languages like C are major sources of bugs, making reliable static analysis difficult or impossible without significant false positives. An example i = i++ in C demonstrates undefined behavior.
17:34 - 19:58 Levels of Static Analysis: Static analysis can range from basic hygiene (coding style) to finding "dumb" bugs (uninitialized variables), to tackling deep, implicit problems (buffer overflows, arithmetic overflows), and finally to proving application-specific security or safety properties (fourth base). SPARK aims for this highest level.
20:01 - 21:01 How SPARK Achieves High Reliability: SPARK enables deep verification by subsetting the base language (eliminating ambiguous features), incorporating contracts (specifying expected behavior), and leveraging automated theorem provers to mathematically prove properties about the code.
21:08 - 26:30 Finding a Bug in Crypto Code: A technical example details how SPARK's verification process found an integer overflow bug in the official C reference implementation of the Skein cryptographic hash function, which could lead to incorrect or insecure output for certain inputs. This highlights the tool's ability to find subtle corner cases missed by experts and extensive testing.
26:44 - 32:40 Real-World Success Stories: SPARK has been used in numerous critical systems with impressive results:
26:53 Helicopter Landing System: 20+ years of operation with only one minor HMI bug, enabling safer landings in rough seas.
28:19 Rolls-Royce Jet Engines: Used in FADEC (engine control) and engine monitor software, improving safety, reliability, and maintenance costs through predictive monitoring.
29:43 Credit Card Key Generation: Used for generating public/private key pairs, achieving 0.04 defects per thousand lines of code over a decade.
30:29 Network Rail Signaling: Prototype backup system using low-integrity inputs (GPS, phone signal) to derive high-integrity train positioning.
31:21 NSA Tokeneer: A publicly released secure access system built as a demo, showcasing the methods and tools.
32:44 - 38:04 UK Air Traffic Control System: A system predicting future aircraft positions and conflicts using complex algorithms and diverse data sources. This quarter-million line logical code base is mathematically proven memory safe with no undefined behavior, gracefully handling bad data.
38:05 - 39:11 Verification Workflow Efficiency: While initial full proofs can take hours (~2 hours), caching results reduces reproof time significantly (~15 mins), and modularity allows changes to be verified in seconds, making static analysis a practical pre-commit activity for developers.
39:17 - 41:01 "Fumble Programming" & Future: The process using these tools is humbling, revealing that even experienced programmers introduce many defects. The recommended approach ("formal + humble") embraces tool assistance to catch these flaws early. The need for such high-integrity software is growing, especially in IoT, connected vehicles, and security-sensitive domains. The technology is freely available (GPLv3) and includes resources for learning.
49:05 - 50:24 Compiler Trust & Performance: SPARK programs often perform very well with standard optimizers (like GCC) because the absence of undefined behavior allows compilers to make stronger, correct optimization decisions, sometimes outperforming C code. While compiler trust is important, the well-defined nature of SPARK code enhances reliability.