Formal Verification

On this site

External links

Formal verification in Ironclad

Formal verification in Ironclad is done with the goals of ensuring abscence of runtime errors (AoRTE) and program correctness.

Ironclad is not 100% verified code. A majority of it lies somewhere within SPARK's spectrum, and a big chunk of it is verified to very high SPARK verification levels, but at the end of the day, Ironclad is basically a hobbyist 1-man effort, and the project is really constrained on the manpower needed to verify components.

Because of this manpower shortage, currently development leans more heavily on implementing new features than verifying said features. But verification is still done, just playing catch-up.

So how much is formally verified anyways?

Ironclad is divided on different subsystems, which can be seen in the source code as subdirectories and Ada packages. The statistics for all subsystems as of Fri Jan 19 are as follows:

Subsystem SPARKification process Verification process Verification quality
arch Done Peding on arch ports Peding on arch ports
arch/aarch64-stivale2 Not started Peding on SPARKification Peding on SPARKification
arch/arm-raspi2b Not started Peding on SPARKification Peding on SPARKification
arch/sparc-leon3 Not started Peding on SPARKification Peding on SPARKification
arch/x86_64-multiboot2 Not started Peding on SPARKification Peding on SPARKification
cryptography Done Done Full AoRTE
devices Done Partial Full AoRTE on registry and virtual devices
ipc Done Mostly done Full AoRTE when applicable
lib Done Done Full AoRTE
memory Done Not started Peding on verification
networking Done Done Full AoRTE
userland Done Partial Full AoRTE on MAC, syscall bodies unverified
vfs Done Partial Full AoRTE on registry, drivers unverified

How it is done

Ironclad uses SPARK for formal verification. SPARK works with contracts specified in Ada code itself. Which take the form of preconditions, postconditions, and relationships between types and variables. When not specified, SPARK infers them.

These verification mechanisms may appear in the source as:

procedure Substract
   (Seconds1, Nanoseconds1 : in out Unsigned_64;
    Seconds2, Nanoseconds2 : Unsigned_64)
   with Pre =>
      Is_Normalized (Nanoseconds1) and then
      Is_Normalized (Nanoseconds2)
         Post => Is_Normalized (Nanoseconds1);

Often times, these mechanisms can be infered by SPARK itself. That is the approach taken for arithmetic functions, which are designed to take all data given, with no pickyness, and always present AoRTE.

By checking these constructs across the whole codebase, SPARK checkers, like GNATProve, by using a process called deductive verification, are able to establish checkable mathematical proof obligations that the code must comply to.