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.
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 Oct 18 2024 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/riscv64-limine | Not started | Peding on SPARKification | Peding on SPARKification |
| arch/sparc-leon3 | Not started | Peding on SPARKification | Peding on SPARKification |
| arch/x86_64-limine | 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 |
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.