Highly Automated Verification of Security Properties for Unmodified System Software

Formal verification can mathematically prove that a hypervisor or security monitor never leaks secret data, but doing so has meant writing thousands of lines of hand-crafted machine-checked proofs, so almost no real system is verified; this paper (Columbia University and CertiK — Ganxiang Yang, Jason Nieh, Ronghui Gu, and colleagues) presents Spoq2, which reduces a security property to small per-transition invariants an SMT solver can check automatically, and prunes away everything irrelevant so the solver does not choke on real, unmodified system code.

The argument in one glance

Problem

The software everything trusts is complex, and proving it secure is prohibitively hard

Operating systems, hypervisors, firmware, and security monitors sit at the foundation of every computing system, and everything above them trusts them completely. That trust is dangerous, because this software is large and complex, and its complexity hides exploitable vulnerabilities that can compromise the confidentiality and integrity of the entire machine. Formal verification offers something no amount of testing can: a mathematical proof that the software is free of whole classes of bugs — for instance, a proof that a confidential-computing monitor never leaks secret data to untrusted code. The problem is that this guarantee has been extraordinarily expensive to obtain. Traditionally, verifying a security property means a human expert manually writing formal specifications, proving that the code refines those specifications, and then constructing a machine-checked proof of the property, often thousands of lines long in a proof assistant like Coq. Proving noninterference (the property that secrets do not leak) for a single Linux KVM hypervisor took roughly 4,800 lines of hand-written Coq proof. That level of effort and expertise means almost no real system software is ever formally verified, so the strongest guarantee we know how to make stays mostly unused exactly where it would matter most.
What people did

Reduce the proof burden, or automate with an SMT solver

Researchers have tried to make this cheaper from two directions. One line of work reduces the manual proof burden while still relying on a proof assistant — the predecessor system, Spoq, cut some of the effort but still required significant hand-written Coq proofs for security properties. Another line automates verification by handing proof obligations to an SMT solver (an automated tool that decides logical formulas), as the Serval framework does — no human proof needed, in principle. Both aim at the same goal: get the security guarantee without a person writing thousands of lines of proof.
Why it fell short

Automation breaks on real code: explosion of paths, states, and pointer arithmetic

Neither approach handles real, unmodified system software well. The proof-assistant route still demands heavy expert effort per property. The SMT-automation route hits two walls the moment it meets real code. The first is path explosion: a program has combinatorially many execution paths through its branches, and considering all combinations of branch conditions overwhelms the solver. The second is solver explosion: reasoning about every possible machine state produces enormous logical formulas that the solver cannot decide in reasonable time. On top of this, existing automated frameworks like Serval do not support pointers — yet system software is saturated with pointer and memory-address manipulation, so a tool that cannot reason about pointers cannot verify real system code at all. The result is that automated verification, which works on small or specially-written programs, does not scale to the large, pointer-heavy, unmodified codebases that actually run underneath our systems. What was missing was a way to make each proof obligation small and pointer-friendly enough for an SMT solver to discharge automatically, without rewriting the software for verification.
This paper's idea

Reduce security to tiny per-transition invariants, and prune everything irrelevant

Spoq2 is the first framework to highly automate security verification of unmodified system software. It takes the code, a set of security properties, and a machine configuration (describing the abstract machine state — registers and memory objects), and builds a transition system that models the software's behavior, with transitions specified by a Coq specification automatically generated from the implementation. Its founding insight is that many security properties, including noninterference, can be reduced to establishing an inductive invariant — a property that holds in every initial state and is preserved by every transition, and therefore holds in all reachable states. Crucially, that invariant can be checked one atomic transition at a time, independently of the rest of the system, so each proof goal becomes small and self-contained enough for the Z3 SMT solver to verify automatically, after which the pieces compose into a proof of the whole. For noninterference specifically, Spoq2 builds a composed system running two executions that differ only in secret data and proves they stay indistinguishable to untrusted code. To make this tractable on real code, Spoq2 adds a suite of optimizations grounded in classic model checking: it decomposes each transition into individual execution paths (one small proof goal per path); it applies Cone-of-Influence (COI) analysis — for the first time at the fine-grained per-transition level — to compute what can actually influence the target property and discard everything else, so a branch that cannot depend on secret data is pruned rather than explored twice; it introduces pointer abstractions that turn complex address arithmetic into simple attribute accesses, eliminating the expensive bit-wise operations that choke SMT queries; and it caches SMT formulas and solver results to reuse across similar paths. Applied to four unmodified real-world codebases — the TF-RMM and TF-A Arm firmware, the SeKVM hypervisor, and the Komodo security monitor — Spoq2 cuts manual effort by up to 80 percent (thousands of lines of proof down to fewer than 200 lines of definitions) and turns verification tasks that once timed out after days into ones that finish in minutes.

Why this problem is worth solving

The software at the bottom of the stack is the software a security failure hurts most, and it is precisely where strong guarantees have been unaffordable.

Every application, no matter how carefully written, ultimately trusts the operating system, hypervisor, firmware, and security monitors beneath it; a vulnerability there can undermine the security of everything running on the machine. These are also among the hardest programs to get right, being large, concurrent, and full of low-level detail. Formal verification is the only technique that can actually rule out entire classes of security bugs rather than just find some of them by testing — a real proof that, for example, confidential data can never flow to untrusted code. But because obtaining such proofs has required thousands of lines of expert hand-written proof per property, verification has been reserved for a handful of specially-built systems, leaving the vast majority of real system software unverified. Bringing the cost down enough that ordinary, unmodified system codebases can be verified would put the strongest available security guarantee within reach exactly where the stakes are highest. That is why automating this, rather than merely reducing the manual effort a little, is a significant step: it changes verification from a heroic one-off effort into something that could be applied broadly.

The obstacle is that real code makes automated reasoning explode, so the whole game is shrinking each proof obligation.

An SMT solver can automatically decide logical questions, but only up to a size limit; feed it a formula that captures every path and every state of a real program and it will never finish. Two forces drive that blow-up: the combinatorial number of execution paths through branches, and the vast space of machine states. So the entire strategy for automated verification is to make each thing the solver must decide small and self-contained. Spoq2’s reduction of a security property to an inductive invariant is powerful precisely because inductiveness is a local condition — it only asks whether each single transition preserves the invariant, which can be checked one transition at a time, without reasoning about the whole program’s behavior at once. That turns one impossible global proof into many small independent ones. But even a single transition can contain many paths and irrelevant state, so the reduction alone is not enough; it must be paired with aggressive pruning that removes anything that cannot affect the property, and with a way to handle pointers cheaply, or the individual proof goals are still too big. The design is essentially a campaign to keep every question the solver sees within the size it can actually answer, which is why the pruning, the pointer abstraction, and the caching matter as much as the core reduction.

What people did before, and where it broke

Hand-write machine-checked proofs in a proof assistant. Manually specify the system and prove security properties in Coq. Where it broke. It demands thousands of lines of proof and deep expertise per property (about 4,800 lines of Coq for one hypervisor’s noninterference), so almost no real system is verified.
Reduce the proof burden but keep the proof assistant (Spoq). Cut some manual effort while still using Coq for the security proofs. Where it broke. It still required significant hand-written proof work for security properties, so verification remained expensive and expert-bound.
Automate verification with an SMT solver (Serval). Hand proof obligations to an automated solver instead of a human. Where it broke. Real code causes path explosion and solver explosion, and the framework does not support pointers — which system software uses everywhere — so it cannot verify real system code.
Verify only specially-written or retrofitted code. Restructure software to make it amenable to automated verification. Where it broke. It cannot be applied to the large, unmodified codebases already running underneath real systems.
The gap. No framework made each proof obligation small enough, and pointers cheap enough, for an SMT solver to automatically verify security properties of unmodified, real-world system software.

How Spoq2 works

From an unmodified codebase to automatically-checked security proofs

↓ →
new
↓ →
new
↓ →
new
↓ →
new
↓ →
new

The idea

Break one impossible global proof into many small, independent ones. Spoq2’s core move is to reduce a whole-system security property to an inductive invariant that can be checked one atomic transition at a time, so each proof goal is small and self-contained rather than a monolithic argument about the entire program. Making verification tractable by decomposing it into independent local pieces that can each be discharged on their own, instead of reasoning about the whole system at once, is the same approach the work on lightweight modular verification for WebAssembly-to-native compilation covered elsewhere on this site takes, turning a global proof into many small modular ones. Spoq2 applies this to security properties of system code, where the local unit is a single transition of the modeled machine.

Prove secrets never leak by tracking what can influence what. For noninterference, Spoq2 runs two executions that differ only in private data and proves untrusted code cannot tell them apart, using Cone-of-Influence analysis to determine which variables secret data can actually reach. Reasoning about information flow — which parts of the system a secret can influence, and ensuring it cannot reach anything observable — is the same principle the work on a principled framework for low-leakage, high-performance design (Untangle) covered elsewhere on this site is built on, tracing how information propagates to bound what leaks. Spoq2 uses this flow analysis not to design hardware but to prune the proof: anything secret data cannot influence is guaranteed identical across the two executions and can be discarded.

Build the analyzable model automatically from the real artifact. Rather than ask a human to write a formal model, Spoq2 constructs the transition system directly from the unmodified implementation, generating the machine model and transition specification from the code and machine configuration. Automatically lifting a formal, analyzable model out of a low-level artifact so security can be reasoned about without hand-building the model is the same idea the work on lifting micro-update models from RTL for formal security analysis covered elsewhere on this site develops, extracting the model from the real design instead of a manual abstraction. Spoq2 does this for system source code, which is what lets it verify software as-is rather than a rewritten version.

Following a security proof through Spoq2

Proving a page-freeing routine never leaks secure-world data

A trace, drawn from the paper's worked example, of how Spoq2 verifies noninterference for a function that frees a memory page.

Step 1 of 5

State the property as noninterference

A confidential-computing monitor must ensure a page tagged SECURE is never leaked to the untrusted Non-Secure world. Spoq2 formalizes this as noninterference: two executions that differ only in secure-page contents must produce identical public data (status, tag, and non-secure page contents).

Public data must match across the two executions; secret data may differ.

Why it works

Inductive invariants make the proof local. Proving a property over the whole system at once is intractable → but checking that each atomic transition preserves an invariant is a local, independent question → so one impossible global proof becomes many small ones an SMT solver can handle.
Per-transition pruning stops the explosion. Enumerating all paths and states overwhelms the solver → but Cone-of-Influence analysis discards whatever cannot influence the property, per transition → so a branch independent of secret data is proven once, not explored across two executions.
Pointer abstraction keeps queries small. Real system code’s address arithmetic produces expensive bit-wise SMT formulas → but modeling pointers as simple attribute accessors → so the solver avoids the bit-wise operations that would otherwise make queries intractable.
Information-flow reasoning is exactly what noninterference needs. Noninterference is about secrets not reaching observable outputs → but Cone-of-Influence directly computes what secret data can influence → so proving no flow to public variables both establishes the property and prunes the search.
Building the model from the code enables unmodified verification. Hand-writing a model for each system is expensive and ties verification to rewritten code → but generating the transition system from the real implementation → so Spoq2 verifies software as-is, with minimal manual effort.

What it costs (trade-offs and scope)

Cone-of-Influence is conservative. COI is a fast but over-approximate analysis: it may keep some variables that do not truly influence the property, so it does not prune everything in principle prunable, trading some precision for speed — occasionally leaving larger proof goals than strictly necessary.
Some manual effort remains. Spoq2 reduces manual work by up to 80 percent, not to zero: a user still supplies the security properties and a machine configuration and writes a modest set of definitions (under 200 lines in the reported cases), so it is highly automated rather than fully push-button.
It targets properties reducible to inductive invariants. The approach applies to security properties, such as noninterference, that can be cast as inductive invariants on transitions; properties that do not fit that shape would need different machinery.
Verification is only as good as the model and configuration. The guarantee is about the transition system built from the code and the supplied abstract machine model; assumptions baked into the machine configuration, or behavior outside the model (such as hardware details not captured), bound what the proof actually covers.
The results are on specific codebases. The up-to-80-percent effort reduction and minutes-versus-days speedups come from four particular systems (TF-RMM, TF-A, SeKVM, Komodo) and their properties; the exact gains depend on the code and the properties verified.

The evaluation

Verifying security properties of system software

Property	Manual proof-assistant	SMT automation without pointers	Spoq2
Manual effort
Handles pointers
Path and solver explosion
Works on unmodified code
Verification time

A comparison of ways to verify security properties of system software. By reducing a property to inductive invariants checked one atomic transition at a time, pruning with per-transition Cone-of-Influence analysis, abstracting pointers to avoid bit-wise SMT operations, and caching solver results, Spoq2 automatically verifies four unmodified real-world codebases (TF-RMM, TF-A, SeKVM, Komodo) with up to 80 percent less manual effort — thousands of proof lines down to fewer than 200 lines of definitions — turning tasks that timed out after days into ones finishing in minutes. Exact figures should be read from the paper.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

This explainer is based on the paper’s full text (the authors’ copy hosted at Columbia University, of the ASPLOS 2026 paper). The described system is the paper’s: Spoq2 is the first framework to highly automate security verification of unmodified system software. It takes a set of security properties, a software implementation, and a machine configuration (abstract machine states such as registers and memory objects), builds a transition system whose transitions are a Coq specification generated from the implementation, and reduces security properties (such as noninterference) to inductive invariants checked per atomic transition by the Z3 SMT solver, then composed. Its optimizations, grounded in model checking, are: decomposing transitions into individual execution paths; extending Cone-of-Influence analysis to the fine-grained per-transition level to prune irrelevant conditionals, states, and clauses; pointer abstractions that turn address arithmetic into attribute accessors to avoid expensive bit-wise SMT operations; and caching of SMT formulas and Z3 results. For noninterference, Spoq2 composes two executions that differ only in private data and proves they remain indistinguishable. The paper evaluates Spoq2 on four unmodified codebases — TF-RMM v0.3.0 (Arm CCA Realm Management Monitor), TF-A v2.13 (Arm-A EL3 secure-world firmware), the SeKVM hypervisor for Linux 6.1, and the Komodo security monitor — reporting up to an 80 percent reduction in manual effort (thousands of lines of security proofs to fewer than 200 lines of definitions) and verification tasks that once timed out after days completing within minutes. It is open-sourced. The prior figure of about 4,800 lines of manual Coq for a Linux KVM hypervisor’s noninterference is the paper’s citation of earlier work. The step-by-step walkthrough follows the paper’s worked example but is a simplified illustration. Exact algorithms, the COI and pointer-abstraction details, and the full evaluation should be read from the paper.

Background

Why we keep raising the bar on trusting the software beneath everything

It helps to see Spoq2 within a broad pattern: the software at the foundation of a system — kernels, hypervisors, firmware, security monitors — is the software whose failure is most catastrophic, so the computing field keeps inventing stronger ways to trust it. Testing can only show the presence of some bugs, never their absence, which for a component the whole machine depends on is a fundamentally unsatisfying guarantee. The response has been a long march toward stronger assurances: better isolation to contain what untrusted code can do, hardware mechanisms to enforce boundaries, and, at the strongest end, formal proofs that rule out entire classes of failure. Each step trades effort for confidence, and the recurring obstacle is cost — the strongest guarantees have been the most expensive, so they get used least where they are needed most. Spoq2’s contribution is to attack that cost for formal proof specifically, automating what used to take thousands of lines of expert hand-proof so that the guarantee can reach ordinary, unmodified system code. This shared goal of making the trusted core of a system dependable, even in the presence of complex or untrusted code, is the same terrain the work on lightweight fault isolation for system software covered elsewhere on this site occupies, hardening the foundation everything else relies on. Spoq2 pursues it through proof rather than runtime isolation: by shrinking each proof obligation until an SMT solver can discharge it, it brings mathematical security guarantees within reach of the real systems that most need them.

If you remember only three things

1. Operating systems, hypervisors, firmware, and security monitors are trusted by everything above them, but their size and complexity hide exploitable vulnerabilities. Formal verification can prove entire classes of security bugs absent — for instance, that a confidential-computing monitor never leaks secret data (noninterference) — but obtaining such proofs has meant a human expert writing thousands of lines of machine-checked proof per property (about 4,800 lines of Coq for one hypervisor), so almost no real system is verified. Automating this with an SMT solver fails on real code because considering all branches and states causes path and solver explosion, and existing automated tools do not even support the pointers that system code uses everywhere.
2. Spoq2 is the first framework to highly automate security verification of unmodified system software. It models the code as a transition system and reduces security properties to inductive invariants — properties true initially and preserved by every atomic transition — which can be checked one transition at a time, making each proof goal small and self-contained enough for the Z3 SMT solver to verify automatically. For noninterference it composes two executions differing only in secrets and proves they stay indistinguishable. To keep this tractable on real code, it decomposes transitions into individual execution paths, applies Cone-of-Influence analysis at the per-transition level to prune anything that cannot influence the property, abstracts pointers into simple attribute accesses to avoid expensive bit-wise SMT operations, and caches solver results.
3. On four unmodified real-world codebases — the TF-RMM and TF-A Arm firmware, the SeKVM hypervisor for Linux 6.1, and the Komodo security monitor — the paper reports Spoq2 proves security properties with up to 80 percent less manual effort (thousands of proof lines reduced to fewer than 200 lines of definitions) and turns verification tasks that once timed out after days into ones finishing in minutes. The trade-offs: Cone-of-Influence is conservative (over-approximate), some manual effort remains (properties and a machine configuration must be supplied), the approach fits properties reducible to inductive invariants, and the guarantee is bounded by the model and machine configuration. It is open-sourced.

Check yourself

Check your understanding

1. Why has formally verifying security properties of real system software been so rarely done?
2. What goes wrong when you try to automate this verification with an SMT solver on real system code?
3. What is Spoq2's core idea for making security verification automatic and scalable?
4. How does Spoq2's per-transition Cone-of-Influence analysis help, and what does the paper report overall?

Sources

The paper is “Highly Automated Verification of Security Properties for Unmodified System Software” by Ganxiang Yang, Wei Qiang, Yi Rong, Xuheng Li, Fanqi Yu, Jason Nieh, and Ronghui Gu (Columbia University; Ronghui Gu is also affiliated with CertiK), published at ASPLOS 2026, DOI 10.1145/3779212.3790171. It received a Best Paper Honorable Mention, is open access under CC BY, and is open-sourced at github.com/VeriGu.

This explainer is written from the paper’s full text (the authors’ Columbia-hosted copy). Spoq2 is the first framework to highly automate security verification of unmodified system software. It models the code as a transition system (with a Coq specification generated from the implementation and states from a machine configuration) and reduces security properties such as noninterference to inductive invariants checked per atomic transition by the Z3 SMT solver, then composed. To scale to real code it decomposes transitions into individual execution paths, extends Cone-of-Influence analysis to the per-transition level to prune irrelevant conditionals, states, and clauses, introduces pointer abstractions that replace expensive bit-wise SMT operations with attribute accessors, and caches SMT formulas and solver results. For noninterference it composes two executions differing only in private data and proves indistinguishability is preserved. Evaluated on four unmodified codebases — TF-RMM v0.3.0, TF-A v2.13, the SeKVM hypervisor for Linux 6.1, and the Komodo security monitor — the paper reports up to an 80 percent reduction in manual effort (thousands of proof lines to fewer than 200 lines of definitions) and verification tasks that once timed out after days completing within minutes. Numbers are the paper’s own; exact mechanisms and full results should be confirmed in the paper.