This webinar provides a comprehensive overview of SPARK, an Ada-derived language and verification toolset designed to formally prove the safety and security of embedded and systems software. The presentation details the core principles of SPARK, including its use of deductive formal verification, where program correctness is proven against functional specifications (contracts) using automated theorem provers. Key features are highlighted, such as its modular and practical nature allowing for incremental adoption, its target-aware analysis that proves the absence of runtime exceptions, and its rich support for advanced Ada constructs and low-level hardware interaction.
A significant portion of the webinar is dedicated to a practical demonstration using a "Mars Rover" platform. It shows how to formalize a critical safety requirement—collision avoidance—and tie it to the software implementation. The demonstration walks through the process of modeling hardware state using ghost code and uninterpreted functions, and illustrates the necessity of loop invariants to help the SPARK prover successfully verify the property within the rover's remote-control logic. The session concludes by discussing the potential role of SPARK in verifying code generated by AI and a Q&A segment.
Using SPARK to Prove Safety and Security in Embedded Systems
00:01:29 - What is SPARK?: SPARK is a technology for deductive program verification. It consists of two main parts: an Ada-derived programming language that includes a functional specification language (contracts), and a tool that uses automatic theorem provers (SMT solvers) to prove that the code is correct with respect to its contracts.
00:03:36 - Deductive Formal Verification: The core concept is to prove that given a set of preconditions (constraints on inputs) and an implementation, a subprogram will always satisfy its postconditions (constraints on outputs).
00:05:56 - Modular and Practical by Design: SPARK verifies code one subprogram at a time, which makes the analysis scalable. This modularity allows for incremental adoption, meaning you can apply SPARK to critical parts of an existing Ada codebase without rewriting everything. It also allows for safe interfacing with code in other languages like C or Rust.
00:11:14 - Ideal for Embedded Systems: SPARK is essentially Ada and supports critical embedded features like precise memory layout definitions (representation clauses) and interaction with hardware through volatile memory, making it highly suitable for low-level programming.
00:12:41 - Modeling with Ghost Code: SPARK allows the use of "ghost code," which is code used only for specification and proof that is not compiled into the final executable. This is useful for modeling system properties without adding runtime overhead.
00:14:52 - Automatic Proof of Critical Properties: Without writing any custom contracts, SPARK automatically proves the absence of many common bugs, including memory safety violations, integer overflows, array out-of-bounds access, and other runtime exceptions.
00:18:16 - Industrial Strength and Qualification: The commercial version, SPARK Pro, is professionally supported and has been qualified under safety standards like ISO 26262 for automotive systems (up to ASIL D).
00:22:53 - Demo: The Mars Rover Safety Property: The webinar demonstrates proving a safety requirement on a Mars Rover: "The rover shall not proceed straight forward when an obstacle is closer than a safety threshold."
00:25:16 - Modeling Hardware State: A key challenge is reasoning about hardware state (e.g., the direction the wheels are turned) when the hardware abstraction layer only provides setters, not getters. This is solved by creating a "model" of a getter using an uninterpreted function and ghost state, linking the setter's action to the proof without implementing an actual getter.
00:35:03 - The Importance of Loop Invariants: During the live coding demo, an initial proof fails because the prover "forgets" the state of the system from one loop iteration to the next.
00:38:26 - Solving the Proof with a Loop Invariant: To successfully complete the proof, a loop invariant is added. This is a property that is true at the beginning of every loop iteration, providing the prover with the necessary context to confirm that the safety property is maintained throughout the loop's execution.
00:41:20 - The Future with Generative AI: SPARK is positioned as an ideal language for a future with generative AI. AI can generate the implementation, but SPARK's formal specifications can be used to rigorously verify that the generated code is correct and safe.