The test was green, and that was the problem. I had to look past the expected result to find out why it was green.

MVM’s OCI workload path behaved the way the security documentation said it should: the workload could not elevate privilege. At first glance, that looked like confirmation that the boundary was working.

Then I followed the path more carefully.

The workload was not setting no_new_privs, and it inherited a much wider capability bounding set than the design allowed. The test image simply happened not to contain a useful setuid binary or dangerous file capability. Its root filesystem was read-only, so the expected outcome still held.

The promise was true for the image we had tested. It was not true for the reason we had documented.

That distinction is almost invisible in a demo. It is the difference between a security property and a lucky environment.

A sentence can hide an entire proof chain

Security documentation is full of short, confident sentences:

  • workloads cannot elevate privilege
  • secrets never enter the guest
  • production images are sealed
  • egress is denied by default
  • a tampered filesystem will not boot

Each sentence compresses several separate questions. Who is the attacker? Which platforms and modes are in scope? What mechanism enforces the property? What happens when that mechanism is unavailable? Which test would fail if somebody removed it?

Without those answers, the sentence is not yet a guarantee. It is a design intention.

After the OCI bug, I started treating every public security claim as a four-part object:

claim=scope+mechanism+witness+limits\text{claim} = \text{scope} + \text{mechanism} + \text{witness} + \text{limits}

The scope tells us where the statement applies. The mechanism names the code or platform feature that enforces it. The witness is the evidence that should break when the mechanism breaks. The limits say where the sentence stops being true.

Leave one of those parts implicit and the claim will eventually drift.

The claim should lead to code and back again

MVM keeps a machine-readable claims catalog because prose is too easy to leave behind.

The useful shape is not a checklist of slogans. It is a graph from a named threat to a scoped claim, then to the mechanism and the evidence that exercises it:

flowchart LR
    T[Named threat] --> C[Scoped claim]
    C --> M[Enforcement mechanism]
    M --> W[Named witness]
    W --> CI[CI or hardware lane]
    C --> L[Explicit limits]
    L --> C

Take the sentence “a tampered root filesystem fails to boot.” That depends on a block-backed backend, dm-verity metadata, the root hash being passed to the kernel, an initramfs that performs the verified mount, and a test that corrupts data and observes failure before guest userspace starts.

The phrase is eight words. The proof chain crosses several subsystems.

The catalog gives reviewers somewhere to ask a precise question: which link in that chain changed?

A witness has to be capable of hurting

A test named after a property is not necessarily evidence for it.

It may assert the wrong layer. It may never reach the dangerous branch. It may be skipped on the only platform where the mechanism exists. Worst of all, it may stay green when the check it supposedly proves is deleted.

The question I now care about is not “Do we have a test?” It is:

Have we watched this witness turn red when the guarantee was broken?

For small policy checks, the fastest answer is still to plant the defect deliberately. Remove the refusal. Widen the capability set. Change the allow-list result. Swap two fields. Then run the named witness.

A green suite is reassuring. Making it fail on purpose is how we learn what the reassurance is worth.

Mutation testing automates some of this. It can remove conditions, invert branches, and alter return values around code such as:

if destination_is_allowed {
    permit()
} else {
    deny()
}

A surviving mutant there deserves attention.

Mutation testing is not a universal proof system. Hardware behavior, timing, and external effects often need live integration lanes instead. MVM records those limits rather than pretending every security property can be reduced to a fast unit test.

Some witnesses only exist on real KVM or Hypervisor.framework hosts. A mock cannot prove that the operating system enforced a vCPU limit, and a parser test cannot prove that a corrupt root filesystem failed before userspace. If those lanes run nightly rather than on every pull request, the claim should say so. Otherwise readers assume a merge gate that does not exist.

The scheduling of the witness is part of the guarantee’s current strength.

The boring boundary is often the dangerous one

One of the less glamorous areas this discipline exposed was FFI layout.

MVM has #[repr(C)] structures that cross into device-mapper, Hypervisor.framework, and other native interfaces. It is tempting to treat layout assertions as ordinary interoperability hygiene.

They are security code.

A capability structure with the wrong offset can widen privilege. A device-mapper structure with the wrong layout can load the wrong table. A VMM exit structure read at the wrong offset can make the runtime misinterpret why a vCPU stopped. The dangerous failure is not always a crash; sometimes it is a plausible value read from the wrong field.

A useful layout contract therefore includes:

  • size and alignment
  • every security-relevant field offset
  • values derived from the authoritative C headers
  • checks on every supported architecture
flowchart TB
    H[Authoritative C header] --> D[sizeof, alignof, offsetof]
    D --> R[Rust const assertions]
    R --> B[Cross-architecture build]
    B --> W[Claim witness]

Printing Rust’s current size_of::<T>() and pasting it into an assertion would only make the program agree with itself. The expected value has to come from the external contract.

This work feels tedious until the day it prevents the runtime from parsing a security boundary incorrectly.

Not every real property is ready to become a headline

Infrastructure projects have a strong incentive to promote every mechanism into a broad promise.

I have become more conservative about that.

A scanner may detect exact secret fingerprints across buffered frames while still being defeatable by encoding or derivation. A resource budget may be admitted consistently while CPU enforcement still differs by backend. A redaction layer may work on MVM-owned cleartext but not inside end-to-end TLS.

Those are useful mechanisms. They are also qualified.

MVM uses preview claims to keep that middle state visible. A preview claim can say what is implemented, where it applies, which witness exists, what remains unsupported, and what would have to change before the wording becomes stronger.

That is not timid security writing. It is version control for confidence.

A narrow claim can grow as evidence accumulates. An oversized one usually has to be walked back after users have already relied on it.

Returning to the green OCI test

The no_new_privs bug was useful because it exposed exactly how a claim can drift.

The workload could not elevate in the image we tested, but the path did not enforce the rule named in the security model. A future image containing a setuid binary or file capability could have changed the result without touching the code reviewers believed mattered.

The fix narrowed the agent’s bounding set after its final privileged setup step, emptied the workload’s set immediately before exec, and applied no_new_privs before the workload began. During the same work, we found a separate bug in a 64-slot capability loop that used a 32-bit shift.

Specific claims lead to specific code, and specific code leads to specific bugs. That is why architecture diagrams alone are not enough.

Try to make the test lie

Before publishing a security sentence, deliberately remove the mechanism it names. Widen the capability set. Skip the refusal. Change the layout assertion. Then run the witness and make sure it turns red.

Before I am comfortable publishing a security sentence now, I want four plain answers:

Who is the attacker?
“Untrusted workload” and “malicious host” are different threat models.

What enforces the property?
Not what usually happens. The exact mechanism.

What turns red?
A unit test, integration test, fuzz target, mutation gate, or live backend lane that fails when the mechanism breaks.

Where does the sentence stop?
The platform, mode, lifecycle state, encryption boundary, or known limitation where the claim no longer applies.

The green test taught me that a correct outcome is not enough. A security property has to be true for a reason the repository can name—and the repository has to notice when that reason disappears.

That is what I mean when I say a security claim is code. Without the mechanism and the witness around it, it is only copy.


Next: The Snapshot Copied the Keys Too