I found a security property in MVM that was true for the wrong reason.
The OCI workload path did not set no_new_privs, and the workload inherited a much wider capability bounding set than the design allowed. The image happened to ship without setuid binaries or dangerous file capabilities, and the root filesystem was read-only, so the expected outcome still held.
That was not good enough.
The documentation named a mechanism. The code was relying on circumstance.
Those two states can look identical in a demo. They are very different systems.
“It works” is not the same as “it is enforced”
Security writing is full of sentences like these:
- workloads cannot escape
- secrets never enter the guest
- production images are sealed
- egress is denied by default
- tampered filesystems do not boot
Each sentence compresses a lot of work.
What is the attacker allowed to control? Which platforms are in scope? What exact mechanism enforces the property? What happens when the mechanism is unavailable? Which test proves the claim? Would that test fail if the relevant check were deleted?
Without those answers, the sentence is aspiration.
I now think of a security claim as a four-part object:
Miss one and the claim is unstable.
The claim graph
MVM keeps a claims catalog because prose drifts.
The useful shape is not a flat list of promises. It is a graph from threat to enforcement to evidence:
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
For example, “tampered rootfs fails to boot” is not one thing.
It depends on a block-backed backend, dm-verity metadata, the root hash on the kernel command line, an initramfs that actually performs the verified mount, and a test that flips data and observes failure before userspace runs.
The phrase is short. The proof chain is not.
That is why the catalog matters. It gives reviewers somewhere to ask, “Which link changed?”
A witness has to bite
A test named after a security property is not automatically evidence for that property.
It may assert the wrong layer. It may never reach the dangerous branch. It may pass if the mechanism is deleted. It may be skipped on the only platform where the code runs.
The question is simple:
Have we seen the witness fail when the guarantee is broken?
That question is more uncomfortable than “Do we have tests?” It is also far more useful.
MVM uses a few different ways to answer it.
Plant the defect
For small checks, the fastest method is still the blunt one: break the code on purpose and run the witness.
Remove the refusal. Widen the capability set. Change a constant. Swap two fields. If the named test stays green, it was never proving the claim.
This sounds obvious. It is not common practice.
A green test suite is emotionally reassuring. Deliberately making it red is how you learn what it actually covers.
Use mutation testing where it fits
Mutation testing automates the planted-defect idea. It changes operators, removes conditions, alters return values, and checks whether tests catch the mutant.
It is especially useful for small policy decisions:
if destination_is_allowed {
permit()
} else {
deny()
}A surviving mutant around code like that is worth investigating.
Mutation testing is not a universal proof system. Hardware paths, timing behavior, and external side effects can be poor fits. MVM records accepted misses where a fast unit test cannot replace a live backend witness.
The important part is not pretending every mutant is equally meaningful.
Treat CI-only witnesses honestly
Some properties only exist on a real KVM or Hypervisor.framework host. A mock cannot prove that a vCPU quota was enforced by the operating system. A parser test cannot prove that a tampered rootfs fails before guest userspace.
Those claims need hardware lanes.
That creates a practical problem: hardware lanes are slower, less available, and sometimes not run on every pull request. The claim catalog has to say that. Otherwise a nightly witness gets read as an immediate merge gate when it is not one.
Again, the limit is part of the claim.
ABI layout is security code
One of the less glamorous discoveries in MVM was how many #[repr(C)] structs crossed a foreign boundary without a complete layout contract.
This is easy to dismiss as FFI hygiene.
It is not.
A capability struct with the wrong field offset can widen privilege. A device-mapper struct with the wrong layout can load the wrong table. A Hypervisor.framework exit struct with the wrong offset can make the VMM misread why a vCPU stopped.
The dangerous failure is often not a clean crash. It is a plausible value in the wrong field.
So the contract needs more than size:
- size
- alignment
- every security-relevant field offset
- values derived from the authoritative C header
- checks on every supported architecture
Printing Rust’s current size_of::<T>() and pasting the result into an assertion proves nothing. The program would be agreeing with itself.
The number has to come from the external ABI.
flowchart TB
H[Authoritative C header] --> D[sizeof, alignof, offsetof]
D --> R[Rust const assertions]
R --> B[Cross-architecture build]
B --> W[Claim witness]
This work is boring right up until it prevents a security boundary from being parsed incorrectly.
Preview claims are useful
There is pressure in infrastructure projects to turn every implemented mechanism into a headline.
I have become more conservative.
MVM has properties that are real but qualified. For example, a secret scanner may catch exact fingerprints across buffered frames while still being defeatable by encoding or derivation. A resource budget may be enforced at admission on every platform while CPU enforcement differs by backend and wall-clock termination is not implemented.
Those should not be flattened into a single broad promise.
The project uses preview claims for this reason. A preview claim can name:
- what is implemented
- what is witnessed
- where it applies
- which limits remain
- what decision would be required to promote it
That is not weakness. It is version control for confidence.
A narrowly stated claim can grow. An overstated claim usually has to be walked back.
The repository should notice drift
A security document that only humans read will drift from the code.
The catalog in MVM is machine-checked in a few ways:
- a claim cannot point at a witness that no longer exists
- security-relevant handlers have to remain represented in policy schemas
- generated protocol surfaces are checked for drift
- dependency and reproducibility gates run in CI
- mutation witness baselines cannot be silently weakened
- platform capability shortfalls fail closed instead of degrading
None of these checks proves the whole system secure.
Together, they make a particular class of dishonesty harder: claiming a mechanism after it has disappeared.
That is a worthwhile property for a repository to have.
The OCI bug was a useful warning
Back to no_new_privs.
The outcome looked right. The workload could not elevate in the image we tested.
But the path did not enforce the rule the way the security model said it did. A future image with a setuid binary or file capability could have changed the result without touching the code that reviewers thought mattered.
The fix had two drop points:
- narrow the agent’s bounding set after the last privileged setup step
- empty the workload’s set immediately before
exec
no_new_privs is applied before the workload starts, so file capabilities and setuid bits become inert. The implementation also found a separate bug in a 64-slot capability loop that used a 32-bit shift.
This is why I do not want security guarantees to live only in architecture diagrams.
Code paths are specific. Bugs are specific. Claims have to be specific too.
What I now require from a claim
Before I am comfortable putting a security sentence in MVM’s public posture, I want four answers.
Who is the attacker?
”Untrusted workload” and “malicious host” are different threat models.
What enforces the property?
Not what usually happens. Not what the current image happens to contain. The actual mechanism.
What turns red?
A unit test, integration test, fuzz target, mutation gate, or live backend lane that would fail if the mechanism broke.
Where does the sentence stop being true?
Platform, mode, encryption boundary, lifecycle state, or known limitation.
If I cannot answer one of those, the wording is not ready.
A security claim is code, plus the evidence around that code.
Otherwise it is just copy.