Formal verification in Ironclad is done with the goals of ensuring Absence of Runtime Errors (AoRTE) and program correctness.
Ironclad is not 100% verified code. A majority of its architecture-independent code lies somewhere within SPARK’s spectrum, and a big chunk of it is verified to high SPARK verification levels, while architectural code is much less verified. Non-architectural code is prioritized due to easier and more rewarding verification.
Ironclad is divided on different subsystems, which can be seen in the source code as subdirectories and Ada packages. Here is an overview of the project:
| Subsystem | SPARK’s stone level progress | SPARK’s silver/gold level progress | Verification quality |
|---|---|---|---|
| arch | Done | Pending on arch ports | Pending on arch ports |
| arch/riscv64-limine | Not started | Pending on stone level | Pending on stone level |
| arch/x86_64-limine | Not started | Pending on stone level | Pending on stone level |
| cryptography | Done | Done | Full AoRTE |
| devices | Done | Mostly done | Sporadic small errors |
| ipc | Done | Mostly done | Full AoRTE selectively |
| lib | Done | Done | Full AoRTE |
| memory | Done | Not started | Pending on gold level |
| networking | Done | Done | Full AoRTE |
| userland | Done | Mostly done | Syscalls not verified |
| vfs | Done | Partial | Full AoRTE at places |
If you would like to analyze the formal verification status and information
yourself, Ironclad is checkable locally using gnatprove with make prove.
Further instructions are available on the project’s README.md.
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 Subtract
(Seconds1, Nanoseconds1 : in out Unsigned_64;
Seconds2, Nanoseconds2 : Unsigned_64)
with Pre =>
Is_Normalized (Nanoseconds1) and then
Is_Normalized (Nanoseconds2)
Post => Is_Normalized (Nanoseconds1);
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 proofs that the code is checked against.