#!/usr/bin/env python3 # ----------------------------------------------------------------------------- # bitstring_status_smt.py # # SMT proof (z3) of the REVOCATION-BIT MONOTONICITY (terminal), no-silent-no-op, # epoch-monotonicity, and bit-frame-isolation invariants of AereBitstringStatusList, # the W3C Bitstring Status List v1.0 for credential revocation / suspension. Plus # load-bearing NEGATIVE CONTROLS for the terminal-revocation guard and the bit mask. # # Contract: contracts/contracts/compliance/AereBitstringStatusList.sol # # A status list is a bitset; each credential owns one status bit at a numeric index. # A list is created for exactly one W3C purpose: # Revocation (purpose 0): a set bit is PERMANENT (monotonic, terminal) -- matching # revocation's terminal semantics. # Suspension (purpose 1): a bit is REVERSIBLE (may be set and later cleared). # setStatus(listId, index, value) fail-closes on each guard (else revert, no change): # S0 controller-only: msg.sender == l.controller (NotController) # S1 in range: index < l.capacity (IndexOutOfRange) # S2 no silent no-op: current != value (NoStatusChange) # S3 terminal revocation: NOT (purpose == Revocation AND value == false) # (RevocationIsTerminal) # then _setBit(index, value) and epoch += 1. # # REVOCATION MONOTONICITY (the target): # on a Revocation list, the only enabled bit transition is 0 -> 1, so once a # credential's status bit is 1 (revoked) it can NEVER return to 0 (un-revoked). # # Method: model the guards + the single-bit update as first-order constraints and # prove each property by asserting its NEGATION under the guards (UNSAT). Bit isolation # uses the standard frame relation over an uninterpreted index->bit function (as in the # append-only models). Each NEG-CTRL removes exactly one guard and shows the attack # becomes SAT. Suspension reversibility is intentional and is NOT a safety violation, # so the monotonicity property is asserted ONLY for Revocation lists. This checks the # DESIGN-level state logic, NOT the compiled EVM bytecode. # # NOTE (honest scope). The zero-knowledge NON-REVOCATION path (verifyNonRevocation + # the SP1 circuit) is [MEASURE]: the circuit is pending and the on-chain path is fail- # closed off until a verifier + vkey are configured; its constructor codeless-verifier # guard (L1) and fail-closed binding are covered by the aere-pq-screen Hardhat tests, # not modelled here. This model covers the fully-implemented on-chain bit mechanics. # ----------------------------------------------------------------------------- from z3 import (Int, Bool, Function, IntSort, BoolSort, Solver, And, Or, Not, Implies, ForAll, If, sat, unsat) REVOCATION, SUSPENSION = 0, 1 results = [] def check(name, s, expect_unsat=True, kind="PROOF"): r = s.check() if expect_unsat: ok = (r == unsat); tag = "PROVED" if ok else "FAILED" else: ok = (r == sat); tag = "CEX-FOUND" if ok else "FAILED" results.append((name, tag, ok, kind)) print(f"[{tag:9}] ({kind}) {name}: z3={r} (expected {'unsat' if expect_unsat else 'sat'})") if r == sat: m = s.model() print(" witness:", {str(d): m[d] for d in m.decls()}) return ok def set_status_ok(sender, controller, index, capacity, current, value, purpose): """setStatus's fail-closed guards S0..S3. The bit changes iff all hold.""" return And( sender == controller, # S0 NotController index < capacity, index >= 0, # S1 IndexOutOfRange current != value, # S2 NoStatusChange Not(And(purpose == REVOCATION, value == False)), # S3 RevocationIsTerminal ) print("### AereBitstringStatusList -- REVOCATION MONOTONICITY + epoch + bit-frame isolation\n") # ---- RM REVOCATION MONOTONICITY: on a Revocation list an enabled transition can only # be 0 -> 1. Model current/value as {0,1} bits; under the guards, prove the new bit # is >= the old bit. Negation: a Revocation transition sets the new bit BELOW the # old one (a 1 -> 0 clear, i.e. un-revoke). UNSAT (terminal guard blocks it). s = Solver() sender, controller = Int('sender'), Int('controller') index, capacity = Int('index'), Int('capacity') curBit, valBit, purpose = Int('curBit'), Int('valBit'), Int('purpose') s.add(Or(curBit == 0, curBit == 1), Or(valBit == 0, valBit == 1)) s.add(purpose == REVOCATION) s.add(set_status_ok(sender, controller, index, capacity, curBit == 1, valBit == 1, purpose)) # current/value as booleans newBit = valBit # _setBit writes `value` s.add(newBit < curBit) # NEGATION: the bit was cleared (un-revoke) check("RM a revocation bit is monotone: once revoked it can never be un-revoked", s) # ---- RM2 the only enabled Revocation transition is 0 -> 1. Negation: an enabled # Revocation transition has old bit already 1 (so it must be a 1->1 no-op or a # 1->0 clear, both forbidden). UNSAT: an enabled revocation write starts from 0. s = Solver() sender, controller = Int('sender'), Int('controller') index, capacity = Int('index'), Int('capacity') curBit, valBit, purpose = Int('curBit'), Int('valBit'), Int('purpose') s.add(Or(curBit == 0, curBit == 1), Or(valBit == 0, valBit == 1)) s.add(purpose == REVOCATION) s.add(set_status_ok(sender, controller, index, capacity, curBit == 1, valBit == 1, purpose)) s.add(curBit == 1) # NEGATION: revoke an already-revoked bit check("RM2 an enabled revocation transition always starts from an unset bit (0 -> 1)", s) # ---- NS NO SILENT NO-OP: setStatus requires current != value, so every recorded # mutation is a real state change. Negation: a write with current == value. UNSAT. s = Solver() sender, controller = Int('sender'), Int('controller') index, capacity = Int('index'), Int('capacity') current, value, purpose = Bool('current'), Bool('value'), Int('purpose') s.add(set_status_ok(sender, controller, index, capacity, current, value, purpose)) s.add(current == value) # NEGATION: a no-op write succeeded check("NS every recorded status mutation is a real change (NoStatusChange guard)", s) # ---- CTRL CONTROLLER-ONLY: a status write requires msg.sender == controller. # Negation: a non-controller mutates a bit. UNSAT. s = Solver() sender, controller = Int('sender'), Int('controller') index, capacity = Int('index'), Int('capacity') current, value, purpose = Bool('current'), Bool('value'), Int('purpose') s.add(set_status_ok(sender, controller, index, capacity, current, value, purpose)) s.add(sender != controller) # NEGATION: a stranger flipped a bit check("CTRL only the list controller can mutate a status bit", s) # ---- EP EPOCH MONOTONICITY: every mutation does epoch += 1, so the version counter # strictly increases (a freshness anchor a published root binds to). Negation: # the post-epoch does not exceed the pre-epoch. UNSAT. s = Solver() epPre, epPost = Int('epPre'), Int('epPost') s.add(epPre >= 0, epPost == epPre + 1) # l.epoch += 1 s.add(Not(epPost > epPre)) # NEGATION check("EP the list epoch strictly increases on every bit mutation", s) # ---- FR BIT-FRAME ISOLATION: setStatus(index) changes ONLY that bit; every other # index keeps its value (the _setBit word-mask touches one bit). Model bits as an # index->bit function; the update sets bit(index) = value and preserves the rest. # Negation: some other index k != index changed. UNSAT. bB = Function('bB', IntSort(), IntSort()) # bits BEFORE the write bA = Function('bA', IntSort(), IntSort()) # bits AFTER the write s = Solver() idx = Int('idx'); v = Int('v'); k = Int('k') s.add(Or(v == 0, v == 1)) s.add(bA(idx) == v) # the target bit takes `value` s.add(ForAll([k], Implies(k != idx, bA(k) == bB(k)))) # every other bit is preserved kk = Int('kk') s.add(kk != idx, bA(kk) != bB(kk)) # NEGATION: a neighbour bit changed check("FR setting one status bit leaves every other credential's bit unchanged", s) # ============================ NEGATIVE CONTROLS ============================== # ---- NEG-CTRL 1 (drop the terminal guard): a BUGGY setStatus without the # RevocationIsTerminal check lets a Revocation list CLEAR a set bit, un-revoking a # credential that revocation semantics say is permanently revoked. ------------- s = Solver() sender, controller = Int('sender'), Int('controller') index, capacity = Int('index'), Int('capacity') curBit, valBit, purpose = Int('curBit'), Int('valBit'), Int('purpose') s.add(Or(curBit == 0, curBit == 1), Or(valBit == 0, valBit == 1)) s.add(purpose == REVOCATION) # BUG: S3 removed; the write needs only controller + range + a real change. buggy_ok = And(sender == controller, index < capacity, index >= 0, curBit != valBit) s.add(buggy_ok) s.add(curBit == 1, valBit == 0) # a 1 -> 0 clear on a Revocation list check("no-terminal-guard list CAN clear a revocation bit (un-revoke a credential)", s, expect_unsat=False, kind="NEG-CTRL") # ---- NEG-CTRL 2 (drop the bit mask / frame): a BUGGY _setBit that also disturbs a # neighbouring index flips another credential's status while setting one bit. s = Solver() idx = Int('idx'); v = Int('v'); kk = Int('kk') s.add(Or(v == 0, v == 1)) s.add(bA(idx) == v) # BUG: no frame preservation; a different index kk is free to change. s.add(kk != idx, bA(kk) != bB(kk)) # a neighbour bit flipped as collateral check("no-mask list CAN flip a neighbouring credential's bit while setting one", s, expect_unsat=False, kind="NEG-CTRL") # ------------------------------------------------------------------------------ print("\n=== SUMMARY ===") allok = True for name, tag, ok, kind in results: print(f" {tag:9} [{kind}] {name}") allok = allok and ok print() if allok: print("AereBitstringStatusList revocation-list safety:") print(" PROVED -- on a Revocation list a status bit is monotone: the only enabled transition is") print(" 0 -> 1 (RM/RM2), so once a credential is revoked it can never be un-revoked; every") print(" recorded mutation is a real change (NS, no silent no-op), only the controller can write") print(" (CTRL), the epoch strictly increases on every mutation (EP, the freshness anchor), and") print(" setting one bit leaves every other credential's bit unchanged (FR, frame isolation).") print(" Two NEG-CTRLs fire: dropping the terminal guard un-revokes a credential, and dropping") print(" the bit mask flips a neighbour's status, so both are load-bearing.") print(" SCOPE (honest): Suspension lists are intentionally REVERSIBLE, so the monotonicity") print(" property is asserted only for Revocation lists (purpose 0). The zero-knowledge non-") print(" revocation path (verifyNonRevocation + SP1 circuit) is [MEASURE]: the circuit is pending") print(" and the on-chain path is fail-closed off until configured; its codeless-verifier (L1)") print(" guard and fail-closed binding are covered by the aere-pq-screen Hardhat tests, not") print(" modelled here. Application-layer compliance tooling, no funds, no PII on chain (an") print(" anonymous bitset keyed by numeric index), consensus classical ECDSA QBFT. DESIGN-level") print(" state logic, not the compiled EVM bytecode.") else: print(" NOT fully established (see FAILED / unexpected CEX above).") import sys sys.exit(0 if allok else 1)