Formal Verification
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 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.
How much is formally verified?
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 | Peding on arch ports | Peding 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 | Full AoRTE with sporadic small errors |
| 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 | Mostly done | Full AoRTE mostly, syscall bodies have errors |
| vfs | Done | Partial | Full AoRTE on registry, drivers unverified |
*Past silver level, SPARK provides no objective measures to quantify verification coverage. Thus, this field is just a statement on quality from the developers.
Obtaining factual results
If you would like some hard numbers to back up the claims, Ironclad is checkable locally using gnatprove with:
make prove
Further instructions are available on the project's README.
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);
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.