Chapter 21 — Web3, blockchain and cryptoasset security: system models
Lesson map
Lesson 21 published. Map, example, EX061.
flowchart TD
N0["Learning outcomes"]
N1["21.1 States and transitions"]
N2["21.2 Invariants"]
N3["21.3 Actors and powers"]
N4["Synthesis"]
N0 --> N1 --> N2 --> N3 --> N4
N4 --> EX["Worked example"]
EX --> Q["Exercise EX061"]
Logical drawing
flowchart LR
N0["Learning outcomes"]
N1["21.1 States and transitions"]
N2["21.2 Invariants"]
N3["21.3 Actors and powers"]
N4["Synthesis"]
N0 --> N1 --> N2 --> N3 --> N4 --> Q["EX061"]
[Learning outcomes]
|
v
[21.1 States and transitions]
|
v
[21.2 Invariants]
|
v
[21.3 Actors and powers]
|
v
[Synthesis]
|
v
[Worked example] --> [Exercise EX061]
Learning outcomes
You will (1) model the voucher system's states and transitions; (2) identify invariants; (3) model actors and their powers.
21.1 States and transitions
Sofia models the voucher contract as a state machine. Its state is the set of balances, total supply, the paused flag and the role assignments. Transitions are issue, transfer, redeem, pause, unpause and change role. Each transition has preconditions, such as the caller holding the right role or having enough vouchers, and effects on the state. Writing the model as a table makes gaps visible: she notices that the design did not say whether redemption is allowed while paused. The board decides it should not be, and the specification is updated before any contract code is written.
21.2 Invariants
An invariant is a property that must hold in every reachable state. Sofia lists the voucher system's invariants: total supply equals the sum of balances; no balance is negative; weekly issuance never exceeds the cap; only the minter role can increase supply. For each transition she checks that, if the invariants hold before, they still hold after. This reasoning, done on paper first, guides the tests she later writes. Invariants are powerful because they summarise correctness in a few sentences, and violations can be detected automatically by monitoring software that compares the live ledger with them.
21.3 Actors and powers
The model also lists actors: members, the shop, coordinators, the issuing service, three keyholders, three validator operators and the board. For each, Sofia records what they can do directly and what they can influence indirectly. Coordinators cannot mint, but their approvals cause minting. Validator operators cannot change balances, but two of them together could stop the ledger. This actor model reveals indirect powers that a contract-only view would miss. She uses it to decide where extra checks are needed, such as a second coordinator approving any week with unusually many shifts.
Worked example
Sofia's state model blocks redemption while paused, lists four invariants and reveals that coordinators indirectly cause minting.
Synthetic case. The model and actors are synthetic.
Errors and limits
Modelling only direct contract powers misses actors who cause outcomes indirectly.
Exercises
- EX061 — Specification gap. What gap did the state table reveal? Rubric: 3 = whether redemption is allowed while paused;; 2 = redemption when paused;; 1 = vague;; 0 = none.
- EX062 — Invariant example. Give one voucher invariant. Rubric: 3 = total supply equals the sum of balances;; 2 = no negative balance;; 1 = supply grows;; 0 = none.
- EX063 — Indirect power. What indirect power do coordinators have? Rubric: 3 = their approvals cause minting;; 2 = approvals;; 1 = vague;; 0 = none.
Synthesis
State, invariant and actor models make a token system's correctness and risks explicit.
Continue studying — chapter 21 of 40
← Chapter 20 (draft) · Course chapter index · Chapter 22 (draft) →