Cool video of replacing C components with SPARK on an ST Micro board

General
1

I really enjoyed making this demo, let me know what you think and how you think I can make this a stronger message to advocate for SPARK.

One of my next steps is to analyze the C code with static analysis to see if I can find the same problems. Not sure if it would.

The full LinkedIn topic is here: AI Ports, Formal Methods Prove: Memory Safety on ST Micro Boards with SPARK | AdaCore

Like and subscribe!

2

Pardon my ignorance. I know very little about Spark, but I take it that it’s Ada with extra bells and whistles for formal verification. It would’ve been helpful if you demonstrated your code because it leaves me with few questions:

  1. Is this video intended for non-technical stakeholders, general developers, or Ada developers?
  2. How did you prove the variables were within their bounds? From my understanding, it’s typically done in Ada by specifying its type with a range, for example: type X is Integer range 1..1000, and checked at compile-time and runtime. Is this how you proved it, or did you use a Spark-only feature to achieve it? If so, what extra verification did it offer?
  3. How did you inject incorrect values? Did you pass it in by calling the code’s interface, or was it done by manipulating the stream?
  4. The verified code ran without issues after the injection, how did you achieve it? The code must have either discarded or corrected the invalid values

Finally, AdaCore often throws around “Ada” and “Spark” interchangeably and it creates confusion. When I hear “Spark”, I assume it’s in reference to its special features, but when I hear “Ada”, I assume it’s in reference to the standard Ada language. In this case, I’m unsure. My questions would be answered if I knew.

3

Hello @bweiram,

Thanks for your question! Allow me to answer them 1-by-1:

  1. It is meant for non-technical stakeholders. I wanted to try and highlight that a) it is easy to include Ada as a subcomponent in existing code; and b) that it helps fix unsafe C or C++ code. We use this on tradeshows as well.
  2. I used SPARK in combination with specifying types with ranges. Using SPARK allows me to statically prove the absence of runtime errors. In other words, with Ada I would have to run test-cases and then I would get exceptions when bad data is received. In SPARK gnatprove forces the developer to properly scope the values, or the proof does not pass.
  3. the board has ‘USER’ button that you can program. So the LLM wrote some code to inject bad data in the stream whenever that button is pressed.
  4. Correct, it ignores bad values. The benefit here is that the programmer has_to_ handle these, it cannot be ignored.

All SPARK code is Ada code, but not all Ada code is SPARK code is probably the best way to think about it. SPARK is a subset of Ada, certain constructs you cannot use. Then, once your code is SPARK, you can apply a qualifier to it, we typically use Stone, Bronze, Silver, Gold and Platinum as the progression.

Stone means you are using the SPARK subset. Bronze means you have proven initialization and certain flow properties. Silver is the absense of run-time errors (no undefined behavior). Gold means you have certain properties proven, Platinum means you have expressed all of your requirements in contracts and you have proven all of them. You can find a complete definition here: New Guidance for Adoption of SPARK | AdaCore

With the video, I was trying to demonstrate

  1. You can lift C to Ada, if the data model is not too much based on shared pointers, then this is very easy
  2. You can then lift Ada to SPARK Silver and prove the absence of runtime errors.

Hope this helps, if not, ask away!

Regards,

Mark