Verified Systems

Overview

Verified systems are software or hardware artifacts that have been formally proven to satisfy their specifications, often with machine-checked proofs. These represent the gold standard of software assurance: unlike testing (which can only find bugs) or even automated model checking (which may have modeling gaps), verified systems carry a mathematical proof of correctness that has been independently checked by a proof assistant. This chapter covers the landmark achievements in verified systems — CompCert (verified compiler), seL4 (verified microkernel), verified cryptography, proof-carrying code, runtime verification, specification mining, invariant inference, and automated program repair.

Verified Compilers: CompCert

The Problem

Compiler bugs are particularly insidious because they silently transform correct source code into incorrect machine code. Traditional compiler testing cannot guarantee absence of bugs because the set of possible programs is infinite. CompCert addresses this by proving that the compiler preserves the semantics of the source program.

What CompCert Proves

CompCert is a verified optimizing C compiler developed by Xavier Leroy at INRIA. It is written and verified in Coq and proves the following theorem:

Theorem (comp correctness):
  If source program s compiles to target code t (without error),
  and s produces observable behavior v on input i,
  then t produces the same observable behavior v on input i.

In other words: CompCert preserves the semantics of the source program. If your C program works correctly, the compiled binary will too (modulo the formally specified subset of C that CompCert supports).

flowchart LR
    SRC["C Source Code"] --> FRONTEND["Frontend<br/>(Parsing, Type Checking)"]
    FRONTEND --> CMINOR["Cminor<br/.(Simplified IR)"]
    CMINOR --> CMINORG["CminorG<br/.(With goto)"]
    CMINORG --> RTL["RTL<br/.(Register Transfer)"]
    RTL --> LTL["LTL<br/.(Linear Temporal)"]
    LTL --> MACH["Mach<br/.(Machine Language)"]
    MACH --> ASM["Assembly<br/>(PowerPC, x86, ARM, RISC-V)"]

    style FRONTEND fill:#e1f5fe
    style CMINOR fill:#e1f5fe
    style CMINORG fill:#fff3e0
    style RTL fill:#fff3e0
    style LTL fill:#fff3e0
    style MACH fill:#fce4ec
    style ASM fill:#fce4ec

CompCert’s Passes and Proofs

Each compilation pass has a separate correctness proof:

The entire proof is approximately 150,000 lines of Coq. CompCert has been validated by finding real bugs in unverified compilers: it found bugs in GCC and LLVM that produced miscompiled code. CompCert itself has been tested extensively and no miscompilation bugs have been found in its verified passes.

Interview Angle: “Has a verified compiler ever found bugs in mainstream compilers?” — Yes. CompCert’s testing found miscompilation bugs in both GCC and LLVM. The CompCert team uses differential testing against GCC and Clang, and discrepancies revealed bugs in the unverified compilers.

Other Verified Compilers

Verified OS: seL4

The seL4 Microkernel

seL4 is a high-performance microkernel for embedded and security-critical systems, developed at UNSW and Data61 (CSIRO). It is the first general-purpose OS kernel with a machine-checked proof of implementation correctness.

What seL4 Proves

The seL4 verification establishes:

Theorem (seL4 correctness):
  1. Implementation correctness: The C implementation of seL4 correctly
     implements its abstract specification (high-level design).
  2. Access control: No process can access memory or capabilities
     it is not authorized to access.
  3. Integrity: A process cannot modify memory belonging to
     another process without explicit authorization.
  4. No undefined behavior: The C code has no buffer overflows,
     null pointer dereferences, or other undefined behavior.

flowchart LR
    subgraph "seL4 Verification Stack"
        ABS["Abstract Spec<br/>(Executable Haskell)"]
        HCS["High-Level C Spec<br/>(Refined, closer to impl)"]
        IMP["C Implementation<br/>(~8,700 LOC)"]
        ASM["ARM Assembly<br/>(Binary)"]
    end
    ABS -->|Refinement proof| HCS
    HCS -->|Refinement proof| IMP
    IMP -->|Translation validation| ASM
    ABS -->|Security properties| SEC["Access Control<br/>Integrity<br/>No UB"]

seL4 Verification Metrics

Impact and Deployments

seL4 is used in:

• Defense systems (Australian Defence Force)
• Autonomous vehicles (Autocore with seL4)
• DARPA SSITH (Secure processor research)
• Digital avionics (certified to DO-178C assurance levels)

The formal proof was extended to prove functional correctness of the kernel (all system calls behave as specified) and information flow security (no covert channels through kernel-controlled resources).

Verified Cryptography

Why Verify Crypto?

Cryptographic implementations are notoriously difficult to get right. Side-channel attacks, constant-time requirements, and subtle mathematical properties make informal testing insufficient. Formal verification of cryptography has produced landmark results.

HACL*: Verified Cryptographic Library

HACL* (High-Assurance Cryptographic Library) is a verified cryptographic library written in F* (F-Star), a language designed by Microsoft Research for verification. It includes verified implementations of:

Each implementation is verified for:

• Functional correctness: The output matches the mathematical specification
• Memory safety: No buffer overflows or out-of-bounds reads
• Secret independence: Verified to execute in constant-time (no secret-dependent branches or memory accesses)
• Side-channel resistance: Proven absence of timing leaks

HACL* is deployed in Microsoft Azure, Firefox, and the WireGuard VPN implementation (via the Zinc library).

Fiat-Crypto

Fiat-Crypto (based on work by Erbsen et al.) uses Coq to synthesize cryptographic primitive implementations from high-level specifications. Rather than hand-writing and verifying code, Fiat-Crypto generates correct-by-construction code for elliptic curve arithmetic, field operations, and number-theoretic functions.

// Fiat-Crypto pipeline:
Specification (Coq) → Proof of correctness → C/assembly extraction → Verified implementation

Other Verified Crypto Projects

Proof-Carrying Code (PCC)

Concept

Proof-Carrying Code (PCC), introduced by George Necula and Peter Lee (1996), is a mechanism for a code consumer (e.g., a host system) to verify that untrusted code is safe before executing it. The code producer attaches a machine-checkable proof that the code satisfies a safety policy. The consumer’s proof checker verifies the proof — which is much faster than re-analyzing the code.

flowchart LR
    PRODUCER[Code Producer] --> CODE[Untrusted Code]
    PRODUCER --> PROOF[Safety Proof]
    CODE --> CONSUMER[Code Consumer]
    PROOF --> CHECKER[Proof Checker]
    CHECKER -->|Verified| EXECUTE[Execute Safely]
    CHECKER -->|Failed| REJECT[Reject Code]

PCC Architecture

Foundational Proof-Carrying Code (FPCC)

FPCC extends PCC with a foundational proof that the proof checker itself is correct, eliminating the need to trust even the proof checker. The entire verification chain from machine code to safety property is proven within a single logic.

Runtime Verification

Concept

Runtime verification (RV) monitors a running system against a formal specification (often expressed in temporal logic) and detects violations at runtime. Unlike static verification (which proves correctness before deployment), RV provides guarantees during execution. It complements static methods by handling properties that depend on the runtime environment or that are impractical to verify statically.

flowchart LR
    SYS[Running System] --> MONITOR[Runtime Monitor]
    SPEC[Temporal Logic Spec] --> MONITOR
    MONITOR -->|OK| CONTINUE[Continue Execution]
    MONITOR -->|Violation| ALARM[Alarm / Recovery Action]

Monitorable Properties

Tools

Specification Mining

Concept

Specification mining automatically extracts formal specifications from existing code or execution traces. This is useful for legacy code without documentation, for reverse-engineering APIs, and for generating test oracles.

Approaches

Daikon (Ernst et al.) is the most well-known dynamic specification miner. It infers program invariants (pre/post conditions, loop invariants) by running instrumented programs on a suite of test inputs and looking for properties that hold across all observed runs.

// Daikon might infer:
// Before foo(x): x != null && x.size() >= 0
// After  foo(x): \result != null && \result.size() == x.size()

Mining specifications from traces:

Traces observed:
  lock() → write() → unlock()
  lock() → read() → unlock()

Extracted specification:
  G (lock() → (write() U unlock()) ∨ (read() U unlock()))
  "After acquiring a lock, the next operation is either read or write, followed by unlock"

Invariant Inference

Invariant inference is the process of automatically discovering loop invariants, data structure invariants, or protocol invariants without human guidance. This is one of the most challenging problems in program verification because invariants are not explicit in the code.

The ICE Learning Framework

The ICE (Incremental Correctness Engine) framework, developed by Garg et al., automates invariant inference through an interaction between a learner and a teacher:

flowchart TD
    LEARNER[Learner: Proposes Invariant Candidate] --> TEACHER[Teacher: Checks Candidate]
    TEACHER -->|Positive| CE_P["Positive Example<br/>(Candidate too weak)"]
    TEACHER -->|Negative| CE_N["Negative Example<br/>(Candidate too strong)"]
    CE_P --> LEARNER
    CE_N --> LEARNER
    LEARNER -->|Inconclusive| ICE_D["ICE-D (with Demands)"]
    ICE_D --> LEARNER

The learner proposes invariant candidates, the teacher (verification tool) tests them against the program. If the candidate is too weak (positive counterexample: candidate holds but violates property) or too strong (negative counterexample: candidate doesn’t hold but property is true), the learner refines. This continues until a valid invariant is found.

Automated Program Repair

Concept

Automated program repair (APR) combines verification techniques with code generation to automatically fix bugs. Given a program with a failing test suite or a violated specification, APR generates patches that satisfy the specification and pass the tests.

flowchart TD
    BUGGY[Buggy Program] --> SPEC[Specification / Tests]
    SPEC --> DIAG[Diagnosis]
    DIAG --> SUSPECT[Suspicious Locations]
    SUSPECT --> GEN[Patch Generation]
    GEN --> VERIFY[Verification]
    VERIFY -->|Pass| FIXED[Fixed Program]
    VERIFY -->|Fail| GEN

APR Approaches

Example: Constraint-Based Repair

// Buggy code:
if (a > b) max = a;  else max = b;
// Bug: should be >= not >

// Repair process:
// 1. Generate constraint: find condition C such that
//    for all test inputs, the corrected code satisfies the spec
// 2. Express C as: α*a + β*b + γ >= 0
// 3. Use SMT solver to find α, β, γ that satisfy all test cases
// 4. Result: C = "a >= b" (α=1, β=-1, γ=0)

Comparison of Verified Systems

Interview Questions

Q1: What does CompCert prove and why does it matter?

CompCert proves that its compiled binary preserves the observable behavior of the source C program. This means if your C program is correct, the compiled code is guaranteed to be correct too — no silent miscompilation. This matters because compiler bugs are invisible to traditional testing and can introduce subtle security vulnerabilities.

Q2: Why is seL4 significant?

seL4 is the first general-purpose OS kernel with a complete, machine-checked correctness proof. It proves that the C implementation matches its high-level specification, that access control is enforced, and that the code has no undefined behavior. This provides unprecedented assurance for security-critical applications like defense systems and autonomous vehicles.

Q3: What is proof-carrying code?

Proof-carrying code is a mechanism where the code producer attaches a machine-checkable proof that the code satisfies a safety policy. The consumer only needs a small, trusted proof checker to verify the proof. This shifts the burden of verification to the code producer and minimizes the consumer’s trusted computing base.

Q4: How does runtime verification complement static verification?

Static verification happens before deployment and proves properties about all executions, but it can’t verify properties that depend on the runtime environment (e.g., timing, available resources). Runtime verification monitors actual executions and detects violations at runtime. Together, static verification catches design errors and runtime verification catches deployment-specific violations.

Q5: What is the difference between testing and verification?

Testing executes the program on specific inputs and checks outputs. It can find bugs but never prove their absence. Verification (formal methods) uses mathematical reasoning to prove that the program satisfies its specification for all possible inputs. Verification provides stronger guarantees but requires more effort and is limited by what can be formally specified.

Related Topics

• Model Checking — Automated verification techniques
• Program Verification — Hoare logic, separation logic, symbolic execution
• Testing + Formal Methods — Fuzzing, property-based testing
• Distributed Verification — Protocol verification
• Security — Verified cryptography, secure systems