4a0b48588c
Aere Network public source. Everything here can be checked against the live chain (chain id 2800, https://rpc.aere.network). Scope note, stated up front rather than buried: consensus on chain 2800 is classical secp256k1 ECDSA QBFT. The post-quantum work in this repository is at the signature, precompile, account and transport layers. Nothing here makes the consensus post-quantum, and no document in it should be read as claiming so.
189 lines
11 KiB
Python
189 lines
11 KiB
Python
#!/usr/bin/env python3
|
|
# -----------------------------------------------------------------------------
|
|
# recovery_registry_smt.py
|
|
#
|
|
# SMT proof (z3) of the FAIL-CLOSED, APPEND-ONLY, REPLAY-PROOF guarantees of
|
|
# AereRecoveryRegistry, the on-chain attested consensus-recovery evidence trail
|
|
# authenticated by the LIVE Falcon-512 precompile (0x0AE1). Plus load-bearing
|
|
# NEGATIVE CONTROLS for the per-operator nonce and for append-only.
|
|
#
|
|
# Contract: contracts/contracts/AereRecoveryRegistry.sol
|
|
#
|
|
# submitRecovery() records a recovery event ONLY if a real Falcon-512 signature by
|
|
# the registered operator key over THIS contract's per-operator, per-nonce record
|
|
# hash verifies on-chain (fail-closed), then appends the record and consumes the
|
|
# nonce. The safety-critical guarantees:
|
|
# AP. APPEND-ONLY. Records live in a push-only array; recordId is the index; there
|
|
# is no edit/delete/owner path. A committed record is never rewritten.
|
|
# NO. STRICTLY-INCREASING per-operator nonce. Each write consumes op.nonce and sets
|
|
# op.nonce = nonce + 1; the record hash BINDS the nonce, so a (record, signature)
|
|
# pair cannot be replayed to rewrite history.
|
|
# FC. FAIL-CLOSED. An invalid / short / tampered Falcon-512 signature records nothing
|
|
# and advances no nonce (a stale caller on an un-activated chain, where 0x0AE1
|
|
# returns empty, also records nothing).
|
|
#
|
|
# recordHash = keccak256(abi.encode(RECORD_DOMAIN, chainId, this, operatorId, nonce,
|
|
# halt, resume, faultKind, nValidators, quorum, aliveDuringFault))
|
|
#
|
|
# We model the guards / append relation as first-order constraints and prove each
|
|
# property by asserting its NEGATION and showing z3 returns UNSAT. keccak256 is
|
|
# modelled as an INJECTIVE function in the nonce ([VERIFY]); Falcon-512 verification
|
|
# is modelled as an EUF-CMA predicate: a signature produced over message m1 verifies
|
|
# ONLY for m1 ([VERIFY]: 0x0AE1 precompile soundness). Each NEG-CTRL removes exactly
|
|
# one guard and shows the corresponding attack becomes SAT. This checks the
|
|
# DESIGN-level logic, NOT the compiled EVM bytecode.
|
|
# -----------------------------------------------------------------------------
|
|
from z3 import (Int, Bool, Function, IntSort, BoolSort, Solver, And, Or, Not,
|
|
Implies, ForAll, sat, unsat)
|
|
|
|
FAULT_CRASH, FAULT_NETSPLIT, FAULT_BYZANTINE = 1, 2, 3
|
|
|
|
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 wellformed(halt, resume, blocknum, faultKind, nV, quorum, alive):
|
|
"""submitRecovery()'s parameter guards (else revert, record nothing)."""
|
|
return And(
|
|
Or(faultKind == FAULT_CRASH, faultKind == FAULT_NETSPLIT, faultKind == FAULT_BYZANTINE),
|
|
halt >= 1, resume >= halt, resume <= blocknum, # InvalidHeights
|
|
nV >= 1, quorum >= 1, quorum <= nV, alive <= nV, # InvalidValidatorSet
|
|
)
|
|
|
|
print("### AereRecoveryRegistry -- APPEND-ONLY + STRICT NONCE + FAIL-CLOSED (Falcon-512)\n")
|
|
|
|
# ---- FC FAIL-CLOSED: a record is written ONLY if the Falcon-512 signature verifies.
|
|
# Model write_ok = wellformed AND verifyFalcon. Negation: a record is written
|
|
# with an invalid signature. UNSAT (PQCVerificationFailed guard). ------------
|
|
s = Solver()
|
|
halt, resume, blocknum = Int('halt'), Int('resume'), Int('blocknum')
|
|
faultKind, nV, quorum, alive = Int('faultKind'), Int('nV'), Int('quorum'), Int('alive')
|
|
verifyFalcon = Bool('verifyFalcon')
|
|
write_ok = And(wellformed(halt, resume, blocknum, faultKind, nV, quorum, alive), verifyFalcon)
|
|
s.add(write_ok, Not(verifyFalcon)) # NEGATION
|
|
check("FC a record is written only if the Falcon-512 signature verifies (fail-closed)", s)
|
|
|
|
# ---- FC2 WELL-FORMED: a written record has a valid fault kind, coherent heights,
|
|
# and a coherent validator set. Negation: a written record violates one. UNSAT.
|
|
s = Solver()
|
|
halt, resume, blocknum = Int('halt'), Int('resume'), Int('blocknum')
|
|
faultKind, nV, quorum, alive = Int('faultKind'), Int('nV'), Int('quorum'), Int('alive')
|
|
verifyFalcon = Bool('verifyFalcon')
|
|
write_ok = And(wellformed(halt, resume, blocknum, faultKind, nV, quorum, alive), verifyFalcon)
|
|
s.add(write_ok)
|
|
s.add(Or(And(faultKind != FAULT_CRASH, faultKind != FAULT_NETSPLIT, faultKind != FAULT_BYZANTINE),
|
|
halt < 1, resume < halt, resume > blocknum,
|
|
nV < 1, quorum < 1, quorum > nV, alive > nV)) # NEGATION
|
|
check("FC2 a written record is well-formed (fault kind / heights / validator set)", s)
|
|
|
|
# ---- NO STRICTLY-INCREASING nonce: a successful write sets op.nonce = nonce + 1.
|
|
# Negation: the post-write nonce does not strictly exceed the consumed one. UNSAT.
|
|
s = Solver()
|
|
nonce, noncePost = Int('nonce'), Int('noncePost')
|
|
s.add(nonce >= 0)
|
|
s.add(noncePost == nonce + 1) # effect of a successful write
|
|
s.add(Not(noncePost > nonce)) # NEGATION
|
|
check("NO the per-operator nonce strictly increases on every write", s)
|
|
|
|
# ---- RP REPLAY REJECTED: a signature produced over the nonce-k record hash cannot
|
|
# authorize a write once the nonce has advanced to k+1. The record hash BINDS the
|
|
# nonce (injective in nonce), and Falcon verification is EUF-CMA (a sig over m1
|
|
# verifies only for m1). At nonce k+1 the contract recomputes hash(k+1) != hash(k)
|
|
# and requires verify(pk, hash(k+1), sig_k); that is infeasible. UNSAT. -------
|
|
Hn = Function('Hn', IntSort(), IntSort()) # recordHash as a function of nonce (fixed op/payload)
|
|
verify = Function('verify', IntSort(), IntSort(), BoolSort()) # verify(message, sig) -> valid?
|
|
s = Solver()
|
|
# keccak injectivity in the nonce [VERIFY]:
|
|
a, b = Int('a'), Int('b')
|
|
s.add(ForAll([a, b], Implies(Hn(a) == Hn(b), a == b)))
|
|
k = Int('k'); sig_k = Int('sig_k')
|
|
s.add(k >= 0)
|
|
# EUF-CMA: the adversary's signature sig_k verifies ONLY over the nonce-k hash [VERIFY]:
|
|
m = Int('m')
|
|
s.add(ForAll([m], Implies(verify(m, sig_k), m == Hn(k))))
|
|
# The replay attempt: reuse sig_k when the live nonce is k+1, so the contract checks
|
|
# verify(Hn(k+1), sig_k). A write requires that to be true.
|
|
replay_write_ok = verify(Hn(k + 1), sig_k)
|
|
s.add(replay_write_ok) # NEGATION: the replay is accepted
|
|
check("RP a nonce-k signature cannot be replayed at nonce k+1 (record hash binds nonce)", s)
|
|
|
|
# ---- AP APPEND-ONLY: a committed record is never rewritten. Model the record array
|
|
# as index->value with the append relation (a write only pushes at index len).
|
|
# Negation: an already-committed index changes value. UNSAT. ----------------
|
|
rB = Function('rB', IntSort(), IntSort()) # records BEFORE the write
|
|
rA = Function('rA', IntSort(), IntSort()) # records AFTER the write
|
|
s = Solver()
|
|
L = Int('L'); newRec = Int('newRec'); i = Int('i')
|
|
s.add(L >= 0)
|
|
s.add(ForAll([i], Implies(And(i >= 0, i < L), rA(i) == rB(i)))) # existing entries preserved
|
|
s.add(rA(L) == newRec) # new record only at index L
|
|
j = Int('j')
|
|
s.add(j >= 0, j < L, rA(j) != rB(j)) # NEGATION: a committed record mutated
|
|
check("AP the records array is append-only (a committed record cannot be rewritten)", s)
|
|
|
|
# ============================ NEGATIVE CONTROLS ==============================
|
|
|
|
# ---- NEG-CTRL 1 (drop the nonce binding): if the record hash did NOT bind the nonce
|
|
# (a fixed hash Hc regardless of nonce), a signature valid over Hc replays at the
|
|
# next submit: verify(Hc, sig) stays true, so a second identical record is written.
|
|
s = Solver()
|
|
Hc = Int('Hc') # BUG: nonce-independent record hash
|
|
sig = Int('sig')
|
|
verify2 = Function('verify2', IntSort(), IntSort(), BoolSort())
|
|
s.add(verify2(Hc, sig)) # the operator's original signature
|
|
# second submit recomputes the SAME Hc (nonce not bound) and re-checks the SAME sig:
|
|
replay_ok = verify2(Hc, sig) # -> still true, write succeeds
|
|
s.add(replay_ok)
|
|
check("no-nonce-binding registry CAN replay one signature to rewrite history", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ---- NEG-CTRL 2 (drop append-only): a BUGGY mutable records array that overwrites an
|
|
# EXISTING recordId. A committed recovery record is silently changed. ---------
|
|
s = Solver()
|
|
L = Int('L'); j = Int('j'); newRec = Int('newRec')
|
|
s.add(L >= 1, j >= 0, j < L)
|
|
# BUG: the write targets an existing index j (overwrite), so rA(j) != rB(j) is allowed.
|
|
s.add(rA(j) == newRec, rB(j) != newRec) # committed record rewritten
|
|
check("mutable-records registry CAN silently overwrite a committed recovery record", 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("AereRecoveryRegistry evidence-trail safety:")
|
|
print(" PROVED -- a record is written only if the Falcon-512 signature verifies (FC) and is")
|
|
print(" well-formed (FC2), the per-operator nonce strictly increases on every write (NO), a")
|
|
print(" nonce-k signature cannot be replayed once the nonce advances because the record hash")
|
|
print(" binds the nonce (RP), and the records array is append-only so a committed record can")
|
|
print(" never be rewritten (AP). Two NEG-CTRLs fire: dropping the nonce binding lets one")
|
|
print(" signature replay to rewrite history, and a mutable records array silently overwrites a")
|
|
print(" committed record.")
|
|
print(" [VERIFY] FALCON-512 PRECOMPILE (0x0AE1): the signature-validity bit is produced by the")
|
|
print(" live native precompile activated on mainnet 2800 at block 9,189,161; its soundness")
|
|
print(" (EUF-CMA of Falcon-512, correct precompile input parsing, empty-return-is-invalid on an")
|
|
print(" un-activated chain) is a trusted primitive, modelled here as the verify predicate, not")
|
|
print(" re-proved. keccak256 injectivity (the nonce-bound record hash) is [VERIFY], modelled.")
|
|
print(" DESIGN: this contract records ATTESTATIONS about recovery events; it does not observe")
|
|
print(" consensus, halt the chain, or activate PQ consensus (still classical ECDSA QBFT). The")
|
|
print(" uint64 nonce cannot realistically overflow. This checks the guard logic, not the")
|
|
print(" compiled EVM bytecode.")
|
|
else:
|
|
print(" NOT fully established (see FAILED / unexpected CEX above).")
|
|
import sys
|
|
sys.exit(0 if allok else 1)
|