yannickmoy

you can ask Alire to install the latest GNAT it built, or to use another version installed on your machine, see https://alire.ada.dev/transition_from_gnat_community.html

It also explains how to install GNATprove: ``alr with gnatprove``

and there are actually multiple ways to prove that the result is a permutation of the entry, either by computing a model multiset (a.k.a. bag) of the value on entry and exit and showing they are equal, or by exhibiting the permutation to apply to the entry value to get the exit value (typically by building this permutation as the algorithm swaps value, in ghost code), etc.

but none of this makes a good read for people not already familiar with program proof tools.

For a related eye-opening result, with both practical application and interesting research backing it, see this talk on "Quicksorts of the 21st century" at Newton Institute on Verified Software last year: https://www.newton.ac.uk/seminar/30504/

TLDR; practical complexity computation needs to take into account things like memory access latency on different architectures.

You can get automatic resource handling with controlled types, but this is not part of the baremetal minimal runtime you can use for a driver.

You can get ownership tracking with SPARK, but you need to use proof techniques.

There are pointers in Ada, but it's not at all the same as in C. First, C pointers are really addresses, references and pointers in Ada. And pointers come in various flavors named/anonymous access-to-variable/constant/subprogram, pointing only to the heap or also to the stack, with accessibility levels depending on where the type is defined... which lead to fine-grain distinction of the various use cases with SPARK so that only correct use is provable.

Here, we are targeting full functional specification, which is hard. So there is a lot of ghost code to support the proof (the loop invariants, assertions and ghost entities). That's what's driving the verification time up. I don't find this enormous at all, given the guarantees provided.

Most code in SPARK is proved to a much more modest level, where the proof is much easier, and that's where you get scaling.

And yes, we're using the best available provers for the task under the hood (currently Alt-Ergo, CVC4, Z3 and COLIBRI), and on some of the checks in that proof of the light runtime, a call to a single prover on a single check may take minutes.

I confirm that we're following closely what Xavier is doing for Rust, and even copied his work on "prophecy variables" to take the effects of borrowing into account in loop invariants in SPARK!

Your plans for having Rust analyzers collaborate look very cool! Like you said, the first challenge is to agree on a base specification language. I hope this gets discussed at the next Rust Verification Workshop.

As someone said, the best solution here is to use the dimensionality analysis in GNAT: https://docs.adacore.com/gnat_ugn-docs/html/gnat_ugn/gnat_ug...

as in:

  with Ada.Text_IO; use Ada.Text_IO;
  with System.Dim.Float_Mks; use System.Dim.Float_Mks;
  with System.Dim.Float_Mks_IO; use System.Dim.Float_Mks_IO;

    procedure Main is
       subtype Distance is System.Dim.Float_Mks.Length;
       subtype Area is System.Dim.Float_Mks.Area;

       D1 : constant Distance := 10.0*m;

       D2 : constant Distance := 20.0*m;

       -- D3 : constant Distance := D1 * D2;
       -- Does not compile. GNAT returns the following error:
       --   main.adb:13:08: dimensions mismatch in object declaration
       --   main.adb:13:37: expected dimension [L], found [L**2]

       A : constant Area := D1 * D2;
    begin
       -- print: Area A is  2.00000E+02 m**2
       Put ("Area A is ");
       Put (Item => A);
       Put_Line ("");
    end Main;

It has changed: https://blog.adacore.com/pointer-based-data-structures-in-sp...

You can look at this blog post where I used a ghost global variable to hold the current state of the game (see section "Proving Functional Properties of Tetris Code"): https://blog.adacore.com/tetris-in-spark-on-arm-cortex-m4

You can similarly express ghost properties of your types, even though we don't have ghost fields in SPARK. For more on ghost code in SPARK, you can look at this presentation last year from my colleague Claire Dross: https://www.adacore.com/uploads/products/SSAS-Presentations/...

As a more extensive example of a useful library with this kind of contracts for proof, Joffrey Huguet added rich contracts of this kind to the Ada.Text_IO standard library just two weeks ago, as part of his current internship with us. This should be in the FSF trunk in the coming weeks. For example, here are some contracts he added:

   procedure Open
     (File : in out File_Type;
      Mode : File_Mode;
      Name : String;
      Form : String := "")
   with
     Pre    => not Is_Open (File),
     Post   =>
      Is_Open (File)
      and then Ada.Text_IO.Mode (File) = Mode
      and then (if Mode /= In_File
                  then (Line_Length (File) = 0
                        and then Page_Length (File) = 0)),
     Global => (In_Out => File_System);

   procedure Put (File : File_Type; Item : Character) with
     Pre    => Is_Open (File) and then Mode (File) /= In_File,
     Post   =>
       Line_Length (File)'Old = Line_Length (File)
       and Page_Length (File)'Old = Page_Length (File),
     Global => (In_Out => File_System);

   procedure Close  (File : in out File_Type) with
     Pre    => Is_Open (File),
     Post   => not Is_Open (File),
     Global => (In_Out => File_System);

We have a compiler from a subset of Ada & SPARK to C: http://docs.adacore.com/live/wave/gnat_ccg/html/gnatccg_ug/g...

But that's not the same as having a full certified (in the sense of Coq) compiler. If we were to use a CompCert-like approach, we'd have to redo it in Coq. Not a small feat.

Regarding approaches that build safety/security by developing a language on top of C, that has been tried so many times that I don't think it can work. The use of the same syntax is deceptive, as you end up doing a lot of redesign/rewrite (as anyone who has done program proof would expect), so none of these sticked. Even those trying to enforce properties by design and runtime checking instead of proof (CCured, Cyclone). Better to stick with C then and use an appropriate toolset like Frama-C.

Funny that you pointed to the workshop at KAIST. My colleague Johannes Kanig presented SPARK there, he's on the front row with a SPARK t-shirt. :-)

Regarding your Brute-Force Assurance Concept, it connects to the concept we're pushing at AdaCore of System to Software Integrity, in which we're looking at ways to preserve assurance from higher level descriptions at system level down to code. I must admit we're still in the early stages, exploring with customers how to go from SysML or Simulink to code in SPARK while preserving properties.

Your concept of using the best available tools is certainly attractive, if indeed they can be made to collaborate, and if the translations can be made trustworthy. That's something we're quite familiar with, as this is the bread-and-butter for tool building really. :-) One of the challenges in connecting languages and tools is that all the pieces are constantly moving. This is also what makes C so attractive as an intermediate language: it does not move.

WhyML has some advantages as an intermediate language. But note that the way we use it in our SPARK toolchain would not allow compiling through WhyML. Our translation only preserves the axiomatic semantics of the program, not its operational semantics. So we try to get equi-provability, but not an executable WhyML code.

If you start with WhyML though, you can either extract it to OCaml (see http://why3.lri.fr/doc-0.83/manual009.html) or to C (see https://hal.inria.fr/hal-01519732v2/document). One of the authors of this last paper, Raphael Rieu-Helft, is currently doing his PhD on getting this extraction to C formally proved, so that it can be used for efficient security components in WhyML. So maybe what you're looking at could be done with formally verified translation from WhyML to C and then formally verified compilation to assembly. We've also looked at having a SPARK frontend to CompCert in the past, but so far we've seen no commercial interest in that approach.

Thanks for your thoughts on that topic!

Thanks for the links to interesting articles. Definitely interested in the interior point formalization and proof. As I expected, it's already quite hard even without taking floats into account. (In the conclusion they say "We worked with real variables to concentrate on runtime errors, termination and functionality and left floating points errors for a future work.") Our experience with industrial users using floats is that most are not interested if we don't deal with floats. Otherwise no guarantees can be given for the actual code.

Re learning SPARK, we'll have a brand new learning website during the year for Ada and SPARK, to replace the e-learning website u.adacore.com. This should make it far easier to learn Ada/SPARK, hopefully with online tweakable examples as on https://cloudchecker.r53.adacore.com/

With the SPARK Discovery GPL 2017 edition (from https://www.adacore.com/download), note that you'll get only Alt-Ergo installed by default. You need to follow these other instructions to add CVC4/Z3: http://docs.adacore.com/spark2014-docs/html/ug/en/appendix/a...

If you have any problems, let's discuss on spark2014-discuss@lists.adacore.com, or report it on spark@adacore.com

I'm curious about your Brute-Force Assurance concept, can you say more?

I would be interested in your repository of resources, is it something you plan to make public soon?

Something I find very useful as a developer is to see how tools work on concrete examples. For formal verification, this is well examplified by the document "ACSL by Example" about Frama-C:

https://github.com/fraunhoferfokus/acsl-by-example/blob/mast...

This has inspired other researchers to do the same for SPARK, but currently they have done only the code/proofs, not yet the doc around it:

https://github.com/yoogx/spark_examples/tree/master/spark-by...

As I like that approach a lot, that's something I have adopted for the static analysis tools we develop around Ada and SPARK:

http://docs.adacore.com/codepeer-docs/users_guide/_build/htm...

https://docs.adacore.com/spark2014-docs/html/ug/en/source/gn...

This shares with the O'Reilly Cookbook series (https://ssearch.oreilly.com/?q=cookbook) the goals to get very concrete immediately, on code that the reader might have to write or have already written.