How to Improve the Robustness of Auto-active Program Proof Through Redundancy

Presented as part of the 2021 HCSS conference. 

ABSTRACT:

SPARK is a program proof environment for Ada programs. It is typically used to guarantee simple properties of medium-size critical programs, from thousands to tens of thousands of lines of code. The typical properties of interest range from absence of run-time errors to data invariants and correct sequencing of calls. The scope of a proof in SPARK is an individual function, which is in general much smaller than the complete program, from tens to hundreds of lines of code. While this reduced analysis scope greatly facilitates the initial establishment of proofs and their maintenance over time, in particular because it avoids scalability problems, it does not completely solve the issue of proof maintenance. Restricting our investigation to changes that don’t impact specifications, there are two root causes for proof regressions: either the code has changed, or the tool has changed. Code changes that don’t impact the specification are typical of small code fixes or code optimizations. Tool changes are incurred when upgrading to a newer version of the tools that offers new functionality and/or fixes problems in the tools. As part of developing the SPARK tools, we are well familiar with the latter, as it is a recurring cost to maintain the proof baseline of our testsuites. In both cases, restoring the proof may require changing the tool settings and/or modifying the ghost code used to nudge automatic provers towards a proof. Our accumulated experience over the years is that the redundancy provided by using multiple automatic provers and careful use of ghost code increases the robustness of such auto-active proofs. We will present experiments that we conducted to question these impressions, which provide quantitative results on how each type of redundancy contributes to the overall proof robustness. In these experiments, we ran public versions of the SPARK tool released between 2018 and 2020 on algorithms from the SPARK-by-Example1 education project, the SPARKNaCl2 rewrite of the cryptographic library TweetNaCl in SPARK and a functionally proved library of imperative red-black-trees in SPARK3. We enabled different provers and/or ghost code, to see how each type of redundancy was contributing to the robustness of the proof as we’re changing the version of the tool. All results will be made public for others to reproduce our results or perform similar experiments.

1  https://github.com/tofgarion/spark-by-example
2  https://github.com/rod-chapman/SPARKNaCl
3  http://toccata.lri.fr/gallery/spark_red_black_trees.en.html

Yannick Moy is Static Analysis Lead at AdaCore. Yannick leads the development of SPARK, a software source code analyzer aiming at verifying safety/security properties of programs. He frequently talks about SPARK in articles, conferences, classes and blogs (in particular blog.adacore.com). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.