Skip to content

Your first check, in five minutes

You will download a real evidence bundle, check it with twenty lines of Python, then try to forge it and watch the check catch you.

You need Python 3. Nothing else: no Mokili, no account, no network after the download.

The story behind the file

A train door closes on a passenger's bag strap. Its controller, 120 lines of Ada, is supposed to back off before the force on the strap passes 150 N. A team ran the door and its controller in Mokili, and sent the run to an assessor as one file. You are the assessor.

The film of that run is on mokili.dev, act 1.

1. Download two files

  • door-bundle.json: the run, 2.3 MB. It holds the door's model, the scenario, the run, its result, and the three compiled files the run used.
  • check_bundle.py: the check, twenty lines.

Put them in the same folder.

2. Run the check

$ python check_bundle.py door-bundle.json
model is unchanged             ok
scenario is unchanged          ok
run is unchanged               ok
result is unchanged            ok
scenario names the model       ok
run names the scenario         ok
run names the result           ok
file 3c7e8b016b0a is unchanged ok
file cf77d01a6df0 is unchanged ok
file f28a02fd0a48 is unchanged ok

Ten answers, ten ok. Here is what the script did.

Every record in the file carries a fingerprint: the SHA-256 of its content. Change one character of the record, and the fingerprint no longer matches. The script recomputes each fingerprint and compares.

The records also name each other by fingerprint. The scenario names the model it runs. The run names the scenario and the result. So the four records form a chain, and the script checks every link.

modelsha256:a2a2…scenariosha256:1c5b…runsha256:1a3e…resultsha256:7b62…namesnamesnamesfilesdoor, controllerChange any box, and its fingerprintno longer matches the arrow that points at it. modelsha256:a2a2…scenariosha256:1c5b…runsha256:1a3e…resultsha256:7b62…namesnamesnamesChange any box: its fingerprintno longer matches the arrow to it.

3. Look inside

The file is plain JSON. Read what it claims with look.py:

$ python look.py
The same stop with a bag strap in the doorway from the start
  HOLDS - REQ-DOOR-01 (A caught passenger is not hurt) holds at all 2001 samples
  HOLDS - REQ-DOOR-02 (No open door on a moving train) holds at all 2001 samples
  VIOLATED - REQ-DOOR-03 (The door closes and locks in time) violated: close_request
  peak force on the strap: 108 N at t = 6.5 s

The force peaks at 108 N, under the 150 N limit. The third requirement is violated, and that is right: a door that locks on time with a strap in it has met the wrong requirement.

4. Play the forger

Suppose the sender wanted a better number. Lower the peak from 108 N to 99 N:

import json
bundle = json.load(open("door-bundle.json"))
bundle["result"]["series"]["obstacle_force"]["points"][325][1] = 99.0
json.dump(bundle, open("forged.json", "w"))

Check the forged file:

$ python check_bundle.py forged.json
...
result is unchanged            DOES NOT MATCH
...

One number changed among 2 001, and the result's fingerprint gave it away.

5. Forge more carefully

A careful forger recomputes the result's fingerprint and writes the new one into the file:

import hashlib, json
bundle = json.load(open("forged.json"))
text = json.dumps(bundle["result"], sort_keys=True, separators=(",", ":"), ensure_ascii=False)
bundle["digests"]["result"] = "sha256:" + hashlib.sha256(text.encode()).hexdigest()
json.dump(bundle, open("forged2.json", "w"))

$ python check_bundle.py forged2.json
...
result is unchanged            ok
run names the result           DOES NOT MATCH
...

The result now matches its own fingerprint, but the run still names the old one. To hide that, the forger must change the run. Then the run's fingerprint changes, and so on up the chain.

The forger can rewrite the whole chain. So the last link has to reach you by another road: the fingerprint of the run, read out on a call, or a seal signed with the sender's key. That is question 2, on Verifying a bundle.

What you just showed

You showed You did not show
The four records belong together. Who produced the file. A seal does.
Nothing in them, and no file, was edited after the export. That the door model describes the real door. The credibility record argues that, and the type test confirms it.
What the run claims: the verdicts, the force, the instant. That rerunning the model gives the same result. lakisa reproduce does.

Next

  • Verifying a bundle: the seal, the rerun, and what each verdict means.
  • The record formats: every field of what you just read.
  • Your own bundle checks the same way. The script does not know about doors.

The door's compiled model carries the OpenModelica run-time, under the BSD licence: its notice. The example itself is Apache-2.0.