Skip to main content

Formal verification

Some of the checks a verifier runs are written down twice: once as code, and once as a model, a small description of the rules in a language called Lean. Lean is a proof assistant. A proof is an argument Lean checks step by step, so a proved statement cannot be wrong about the model, only about whether the model matches the world.

A model on its own guards nothing; the risk is in the gap between the model and the code. So each model here also writes the tests for the real code. The model computes the expected answer for every test case, the test runs the real verifier on a real input, and the two must agree. If anyone edits the model without regenerating the tests, the build fails.

Three terms come up below:

  • A spec is the list of rules the model states, each as a numbered requirement such as "the verifier MUST refuse a receipt whose sandbox allows networking".
  • MC/DC (modified condition/decision coverage) means every requirement is, in at least one test case, the only rule that is broken. That proves each check in the code is actually exercised and actually decides the answer.
  • A mutant is a copy of the code with one deliberate bug. Running the tests against mutants measures whether they catch real mistakes.

Mac launch receipts​

When an agent runs on a Mac node, the node starts it in a box: a launchd job with a Seatbelt sandbox. The node then signs a launch receipt saying how the box was built and what it read back from it. A verifier credits the receipt only if every rule holds: the box is the published one, the job is that box's own, only the node can start it, the node itself read the sandbox and found networking and the protected paths denied, the agent runs as its own non-root user, and the receipt does not claim more coverage than it has.

What is guaranteed. The model proves that a receipt is credited exactly when every one of its requirements holds. It also proves something about which process the sandbox reading is about. On a Mac, the launchd job's own process is the observer that watches the agent, not the agent, and it runs unsandboxed. The receipt therefore carries the agent's process id separately, and the model proves a credited receipt's sandbox reading always names the agent and never the observer.

How it reaches the code. The model writes 1,893 test cases. Each changes one or two fields of a valid receipt (every value of every field, and every pair of fields), signs it, and runs the real verifier, checking exactly which rows refuse it. Every requirement is the sole cause of a refusal in at least one case, except two that another requirement always reports alongside.

A worked example. Case agentPid=4242+sbPid=4242 is a receipt whose job is process 4242, and which says the agent is also 4242 and that the sandbox was read on 4242. Everything else is valid. It is refused under the job row (B4), because the "agent" it names is the observer. That is the case that proves the observer rule is checked on its own: no other rule is broken.

What is not covered.

  • Lineage. The rules also require the agent to be a descendant of the observer, as Endpoint Security saw it. No receipt field records that today, so no verifier can check it, and the model proves the verifier credits a receipt whose agent is not a descendant. The tests for that case are marked as expected failures until the field exists. Until then, no Mac receipt is credited at all.
  • Order. The sandbox must be applied before the agent says hello. No field records the order.
  • The rows Linux shares (the signature, the node's registration, the session key, the receipt time) are held at valid values, not varied.
  • Which reason. The tests check which row refuses, not the wording.
  • The node's own checks before it signs are not modelled.

When the tests were first run, an independent reviewer wrote 12 mutants without seeing them. The tests caught 10. The two misses were fields the model lacked (a source string that looks like the node's, and a root agent); both fields were added, and the extended tests catch all 12.

For the full list of requirements, each tied to its proof, its test case and the code it constrains, see the generated specification, SPEC.md, in the formal/receipt-v5 directory of the source repository.