Chapter 24 — Web3, blockchain and cryptoasset security: methods I
Lesson map
Lesson 24 published. Map, example, EX070.
flowchart TD
N0["Learning outcomes"]
N1["24.1 Invariants"]
N2["24.2 Replaying logs"]
N3["Lab — Invariant replay"]
N4["24.3 Interpreting violations"]
N5["Synthesis"]
N0 --> N1 --> N2 --> N3 --> N4 --> N5
N5 --> EX["Worked example"]
EX --> Q["Exercise EX070"]
Logical drawing
flowchart LR
N0["Learning outcomes"]
N1["24.1 Invariants"]
N2["24.2 Replaying logs"]
N3["Lab — Invariant replay"]
N4["24.3 Interpreting violations"]
N5["Synthesis"]
N0 --> N1 --> N2 --> N3 --> N4 --> N5 --> Q["EX070"]
[Learning outcomes]
|
v
[24.1 Invariants]
|
v
[24.2 Replaying logs]
|
v
[Lab — Invariant replay]
|
v
[24.3 Interpreting violations]
|
v
[Synthesis]
|
v
[Worked example] --> [Exercise EX070]
Learning outcomes
You will (1) use invariants to reason about token systems; (2) replay logs to check invariants; (3) interpret violations.
24.1 Invariants
An invariant is a property that must hold in every state. For the credit system, Jonas states three: the sum of all balances equals total supply; no balance is negative; and total supply never exceeds the configured cap. The EthTrust specification describes invariant testing as checking assumptions that should remain true in all circumstances. Invariants are powerful because they do not depend on particular inputs: if any sequence of operations breaks one, there is a defect or misuse to investigate.
24.2 Replaying logs
Jonas writes a standard-library script that replays a synthetic log of mints, transfers and burns, tracking balances and supply, and reports any step that would break an invariant. It reads only the synthetic log and prints results. Replaying recorded history against invariants is a practical method for both testing contracts before deployment and auditing operations afterwards, because it checks what actually happened rather than what was intended. Jonas tests the script first on a short log with one deliberate overdraft and one deliberate cap breach, confirming that both are reported at the expected steps before using the lab log.
Lab — Invariant replay
"""Replay a synthetic token log and check supply invariants (read-only)."""
LOG = [("mint", None, "coop", 1000), ("transfer", "coop", "h01", 200), ("transfer", "coop", "h02", 150),
("transfer", "h01", "h03", 50), ("burn", "h02", None, 30), ("transfer", "h03", "h04", 60),
("transfer", "h02", "h05", 100), ("mint", None, "coop", 500)]
CAP = 1400
def main():
bal, supply, issues = {}, 0, []
for i, (op, src, dst, amt) in enumerate(LOG):
if src is not None:
if bal.get(src, 0) < amt:
issues.append(f"step {i}: {src} balance {bal.get(src, 0)} < {amt}"); continue
bal[src] -= amt
if dst is not None:
bal[dst] = bal.get(dst, 0) + amt
supply += amt if op == "mint" else -amt if op == "burn" else 0
if supply > CAP:
issues.append(f"step {i}: supply {supply} exceeds cap {CAP}")
if sum(bal.values()) != supply:
issues.append(f"step {i}: balances != supply")
print("steps", len(LOG), "final supply", supply, "holders", sum(1 for v in bal.values() if v))
for x in issues:
print("issue:", x)
if __name__ == "__main__":
main()
Run with python3 lab_invariant.py. Verified output:
steps 8 final supply 1470 holders 5
issue: step 5: h03 balance 50 < 60
issue: step 7: supply 1470 exceeds cap 1400
24.3 Interpreting violations
The replay processes eight steps and reports two issues. At step 5, h03 tries to transfer 60 while holding only 50; the script rejects the step, as a correct contract would. At step 7, a mint raises supply to 1,470, above the 1,400 cap, meaning the synthetic log contains a mint the cap should have blocked. Jonas explains that the first is the system working correctly, while the second indicates either a cap misconfiguration or a missing check, and would trigger investigation.
Separating expected rejections from unexpected successes keeps the replay from raising alarms on correct behaviour.
Worked example
The replay of eight steps rejects an overdraft at step 5 and flags supply of 1,470 exceeding the 1,400 cap at step 7.
Synthetic case. The log and script are synthetic; EEA EthTrust is a real source.
Errors and limits
Treating every invariant report as an attack ignores cases where the check simply rejected invalid input.
Exercises
- EX070 — Three invariants. State the three invariants. Rubric: 3 = balances sum to supply, none negative, supply under cap;; 2 = three;; 1 = one;; 0 = none.
- EX071 — Step 5 meaning. What does step 5 show? Rubric: 3 = an overdraft correctly rejected;; 2 = rejection;; 1 = attack;; 0 = none.
- EX072 — Step 7 meaning. What does step 7 show? Rubric: 3 = supply 1,470 exceeds 1,400 cap;; 2 = cap breach;; 1 = vague;; 0 = none.
Synthesis
Invariants checked by replay reveal defects and misconfigurations that example tests can miss.
Continue studying — chapter 24 of 50
← Chapter 23 (draft) · Course chapter index · Chapter 25 (draft) →