6cb0140fae
The public history carried kat/__pycache__/mlkem768_reference.cpython-314.pyc, a compiled Python artifact embedding the operator's absolute local path. Text secret scanners do not read compiled binaries, which is exactly how it slipped through, and removing it from the tip would have left it reachable through the old root commits. So this repository is republished from a single clean root. This root also carries, from the previously unpublished line of work: - corrected LICENSE year, LICENSING.md, VERIFY-POLICY.md, and CITATIONS-UNRESOLVED.md remeasured 2026-08-11 (101 paths, README aligned) - O-018: run_consensus_verification.py ran 19 of 29 models and reported PASS; it now runs all 29, and computemarket_smt.py gains resolveByTimeout / reclaimUnsettled cases plus a negative control - O-006: the word 'audited' removed from next to Bouncy Castle, twice, after a concurrent edit resurrected it - O-014: prior art named and dated - Algorand's native falcon_verify shipped about ten months before AERE's precompiles; the primacy claim is withdrawn where it was implied - bench/ scripts parametrized so they actually run for an outsider (the earlier textual sanitization left $STAGING unexpanded inside Python strings) - AIP-2/AIP-3 errata with measured figures, spec remeasurements at 2026-08-01, and the spec-zk-stack retractions (owner is an operational key, not the Foundation; 'maximally sound' withdrawn; aggregator V1 deprecated) The redacted bench-host environment files from the sanitized line are kept exactly as published; the unredacted local variants are not carried.
266 lines
15 KiB
Python
266 lines
15 KiB
Python
#!/usr/bin/env python3
|
|
# -----------------------------------------------------------------------------
|
|
# hybridauthorizer_smt.py
|
|
#
|
|
# SMT proof (z3) of the SAFETY invariants of AereHybridAuthorizer, the LIVE (mainnet
|
|
# chain 2800, deployed 2026-07-12) crypto-agility CONSUMER over AereCryptoRegistry, at
|
|
# 0x168F2A6a3071e7654CF1784a6f5d7BC8e1a582E0
|
|
#
|
|
# Contracts:
|
|
# contracts/contracts/pqc/AereHybridAuthorizer.sol (this consumer)
|
|
# contracts/contracts/pqc/AereCryptoRegistry.sol (resolveActive / verify it routes to)
|
|
#
|
|
# Style follows formal-consensus/spokepool_smt.py: PROVED = negation UNSAT under the
|
|
# exact Solidity guards; each proof is paired with a firing NEGATIVE CONTROL.
|
|
#
|
|
# TARGET INVARIANTS (from the build task):
|
|
# H1 ONLY AN ACTIVE SCHEME AUTHORIZES: any successful check verifies under an id
|
|
# whose status is ACTIVE (never DEPRECATED, never REVOKED). This reduces to
|
|
# resolveActive's postcondition: it returns ONLY an ACTIVE id.
|
|
# H2 A REVOKED id AUTHORIZES NOTHING: a REVOKED id with no ACTIVE successor makes
|
|
# resolveActive revert -> the fail-closed view returns false; a REVOKED id WITH
|
|
# an ACTIVE successor routes verification to the SUCCESSOR (an ACTIVE id), so the
|
|
# revoked scheme's verifier is never the one that authorizes.
|
|
# H3 RESOLUTION TERMINATES and is FAIL-CLOSED: the successor walk halts within the
|
|
# bounded number of rows (returns ACTIVE or reverts -- even on a cycle), and any
|
|
# revert (unknown / dead-end / cycle) is caught by checkAuthorized and reported
|
|
# as false. The default+preference resolution (algorithmFor) always feeds
|
|
# resolveActive a single reference id, so the whole pipeline terminates.
|
|
#
|
|
# ASSUMPTIONS (bound every PROVED):
|
|
# A1. Registry `verify(id,...)` is itself fail-closed and only returns true for an
|
|
# id whose status is ACTIVE or DEPRECATED with a real signature (its own
|
|
# fail-closed gate + the precompile oracle -- proven separately in the halmos
|
|
# R1 suite and cryptoregistry_smt.py). Here we model the routed verifier as a
|
|
# FREE boolean the adversary controls, EXCEPT it is gated by the routed id's
|
|
# status, exactly as AereCryptoRegistry.verify does.
|
|
# A2. resolveActive's loop bound (hops 0.._count) is the source's structural bound;
|
|
# we prove the pigeonhole soundness of the SuccessorCycle revert for a
|
|
# representative registry size and the general fail-closed composition.
|
|
# A3. Design model, not compiled bytecode (the halmos suite is the bytecode layer).
|
|
# -----------------------------------------------------------------------------
|
|
from z3 import (Int, Bool, Array, IntSort, BoolSort, Select, Solver, And, Or, Not,
|
|
Implies, If, Distinct, sat, unsat)
|
|
|
|
# AereCryptoRegistry.Status
|
|
UNKNOWN, ACTIVE, DEPRECATED, REVOKED = 0, 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()
|
|
wit = {}
|
|
for d in m.decls():
|
|
try: wit[str(d)] = m[d].as_long()
|
|
except Exception:
|
|
try: wit[str(d)] = bool(m[d])
|
|
except Exception: wit[str(d)] = "?"
|
|
print(" witness:", wit)
|
|
return ok
|
|
|
|
print("### AereHybridAuthorizer -- ACTIVE-only authorization, revoked-authorizes-nothing, terminate+fail-closed\n")
|
|
|
|
# =============================================================================
|
|
# Model of AereCryptoRegistry.resolveActive as a bounded walk over N rows, and of
|
|
# verify as a status-gated routed verifier. status[] and successor[] are symbolic
|
|
# (the adversary/owner picks any registry configuration).
|
|
# =============================================================================
|
|
N = 6 # representative registry size (matches the halmos R3 suite scale; 5 live rows + spare)
|
|
|
|
def resolveActive_model(startId, status, successor, exists):
|
|
"""
|
|
Faithful model of resolveActive: from startId, follow successor until an ACTIVE
|
|
row (return it, reverted=False) or a dead-end/unknown/cycle (reverted=True).
|
|
Returns (reverted, resolvedId). Unrolled to N+1 hops == the source loop bound.
|
|
Encoded as a nested If exactly mirroring the Solidity control flow.
|
|
"""
|
|
reverted = False # python-level fold producing a z3 expression
|
|
resolved = Int('resolved_never') # placeholder, overwritten below via If-chain
|
|
# We build the expression bottom-up. Represent the walk result as (revBool, idInt).
|
|
# Start from the terminal (after N+1 hops with no ACTIVE => SuccessorCycle revert).
|
|
rev = True # if we exhaust the bound, resolveActive reverts (cycle)
|
|
rid = Int('rid_cycle')
|
|
# Walk backwards is awkward; instead build forward with a fixed unroll:
|
|
return _walk(startId, status, successor, exists, 0)
|
|
|
|
def _walk(id_expr, status, successor, exists, hop):
|
|
# if hops > N -> cycle revert
|
|
if hop > N:
|
|
return (True, id_expr) # reverted (SuccessorCycle)
|
|
exists_i = Select(exists, id_expr)
|
|
st_i = Select(status, id_expr)
|
|
nxt_i = Select(successor, id_expr)
|
|
# recurse for the "advance" branch
|
|
adv_rev, adv_id = _walk(nxt_i, status, successor, exists, hop + 1)
|
|
# if !exists -> revert; elif ACTIVE -> return id; elif successor==0 -> revert; else advance
|
|
rev = If(Not(exists_i == 1), True,
|
|
If(st_i == ACTIVE, False,
|
|
If(nxt_i == 0, True, adv_rev)))
|
|
rid = If(Not(exists_i == 1), id_expr,
|
|
If(st_i == ACTIVE, id_expr,
|
|
If(nxt_i == 0, id_expr, adv_id)))
|
|
return (rev, rid)
|
|
|
|
def registry_verify_model(idv, status, exists, precompile_says):
|
|
"""AereCryptoRegistry.verify status gate: false unless exists AND status in
|
|
{ACTIVE, DEPRECATED}; then returns the (adversary-controlled) precompile bool."""
|
|
st = Select(status, idv)
|
|
ex = Select(exists, idv)
|
|
gate = And(ex == 1, Or(st == ACTIVE, st == DEPRECATED))
|
|
return And(gate, precompile_says)
|
|
|
|
# symbolic registry
|
|
status = Array('status', IntSort(), IntSort())
|
|
successor = Array('successor', IntSort(), IntSort())
|
|
exists = Array('exists', IntSort(), IntSort()) # 1 == exists
|
|
|
|
# ---- H1 : resolveActive returns ONLY an ACTIVE id -> only ACTIVE authorizes ----
|
|
# checkAuthorized authorizes iff resolveActive succeeds (rev==False) AND verify(resolved).
|
|
# We prove: whenever resolveActive returns without reverting, status[resolved]==ACTIVE.
|
|
s = Solver()
|
|
startId = Int('startId')
|
|
rev, resolved = resolveActive_model(startId, status, successor, exists)
|
|
s.add(Not(rev)) # resolveActive returned a value
|
|
s.add(Select(status, resolved) != ACTIVE) # claim it returned a non-ACTIVE id
|
|
check("H1 resolveActive returns ONLY an ACTIVE id (never DEPRECATED/REVOKED)", s)
|
|
|
|
# corollary H1b: a successful authorization's routed id is ACTIVE (never REVOKED).
|
|
s = Solver()
|
|
startId = Int('startId'); precompile = Bool('precompileSaysValid')
|
|
rev, resolved = resolveActive_model(startId, status, successor, exists)
|
|
authorized = And(Not(rev), registry_verify_model(resolved, status, exists, precompile))
|
|
s.add(authorized)
|
|
s.add(Or(Select(status, resolved) == REVOKED, Select(status, resolved) == DEPRECATED, Select(status, resolved) == UNKNOWN))
|
|
check("H1b a successful authorization is verified under an ACTIVE id (never REVOKED/DEPRECATED/UNKNOWN)", s)
|
|
|
|
# ---- NEG-CTRL H1: an authorizer that verifies under the REQUESTED id (skips
|
|
# resolveActive) can authorize under a REVOKED scheme's verifier. --------------
|
|
s = Solver()
|
|
reqId = Int('requestedId'); precompile = Bool('precompileSaysValid')
|
|
# BUG: verify directly on the requested id, no resolveActive gate.
|
|
s.add(Select(status, reqId) == REVOKED, Select(exists, reqId) == 1)
|
|
# a broken verifier that ignores the status gate (models "no fail-closed") + precompile true
|
|
buggy_authorized = precompile
|
|
s.add(buggy_authorized, precompile == True)
|
|
check("NEG-CTRL skipping resolveActive + status gate CAN authorize under a REVOKED id", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ---- H2 : a REVOKED start id authorizes nothing ----------------------------------
|
|
# Case (a): REVOKED with NO successor -> resolveActive reverts -> checkAuthorized false.
|
|
s = Solver()
|
|
startId = Int('startIdA')
|
|
s.add(Select(exists, startId) == 1, Select(status, startId) == REVOKED, Select(successor, startId) == 0)
|
|
rev, resolved = resolveActive_model(startId, status, successor, exists)
|
|
s.add(Not(rev)) # claim it did NOT revert (i.e. authorized something)
|
|
check("H2a REVOKED id with no successor -> resolveActive reverts (fail-closed, authorizes nothing)", s)
|
|
|
|
# Case (b): REVOKED WITH an ACTIVE successor -> the id that verifies is the ACTIVE
|
|
# successor, and it is NOT the revoked id. (The revoked scheme's verifier is unused.)
|
|
s = Solver()
|
|
startId, succId = Int('startIdB'), Int('succId')
|
|
s.add(Select(exists, startId) == 1, Select(status, startId) == REVOKED, Select(successor, startId) == succId)
|
|
s.add(succId != 0, succId != startId, Select(exists, succId) == 1, Select(status, succId) == ACTIVE)
|
|
rev, resolved = resolveActive_model(startId, status, successor, exists)
|
|
s.add(Not(rev))
|
|
s.add(resolved == startId) # claim the REVOKED id itself is what verified
|
|
check("H2b REVOKED id routes to its ACTIVE successor (revoked id itself never verifies)", s)
|
|
|
|
# ---- NEG-CTRL H2: a resolver that returns the first row REGARDLESS of status lets
|
|
# a revoked id be used directly. -----------------------------------------------
|
|
s = Solver()
|
|
startId = Int('startId2'); precompile = Bool('p')
|
|
s.add(Select(status, startId) == REVOKED, Select(exists, startId) == 1)
|
|
# BUG resolver: returns startId whatever its status; verify then only checks the precompile.
|
|
buggy_resolved = startId
|
|
s.add(precompile == True)
|
|
s.add(And(buggy_resolved == startId, precompile)) # authorized under the revoked id
|
|
check("NEG-CTRL a status-blind resolver authorizes directly under a REVOKED id", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ---- H3 : termination -- the bounded walk always halts (returns ACTIVE or reverts).
|
|
# By construction of the N+1 unroll: every path in resolveActive_model reaches a leaf
|
|
# (ACTIVE return, successor==0 revert, unknown revert, or the hop>N cycle revert).
|
|
# We prove there is NO input on which the modelled walk fails to produce a verdict,
|
|
# i.e. (rev is a total boolean expression). Equivalent SMT check: rev XOR (not rev)
|
|
# is a tautology -> its negation is UNSAT.
|
|
s = Solver()
|
|
startId = Int('startId3')
|
|
rev, resolved = resolveActive_model(startId, status, successor, exists)
|
|
s.add(Not(Or(rev, Not(rev)))) # negate totality (law of excluded middle)
|
|
check("H3 resolveActive is total within the loop bound (always halts: ACTIVE or revert)", s)
|
|
|
|
# H3-pigeonhole soundness: if the walk visits N+1 DISTINCT non-ACTIVE, non-terminal
|
|
# rows it is a genuine cycle -- there is no acyclic chain of length N+1 over N rows.
|
|
# Model the visited-node sequence v0..vN over ids in 1..N; require all Distinct and
|
|
# all non-terminal; z3 must find it UNSAT (pigeonhole) -> the cycle revert is not a
|
|
# false alarm (it only fires on real cycles / dead-ends).
|
|
s = Solver()
|
|
vs = [Int(f'v{i}') for i in range(N + 1)] # N+1 visited ids
|
|
for v in vs:
|
|
s.add(v >= 1, v <= N) # only N real rows exist
|
|
s.add(Distinct(*vs)) # claim: N+1 distinct rows visited
|
|
check("H3b pigeonhole: no acyclic successor walk of length _count+1 exists (cycle revert is sound)", s)
|
|
|
|
# ---- H3 fail-closed composition: checkAuthorized returns false whenever resolveActive
|
|
# reverts (the try/catch). Prove: rev == True => authorized == False. ---------
|
|
s = Solver()
|
|
startId = Int('startId4'); precompile = Bool('pc')
|
|
rev, resolved = resolveActive_model(startId, status, successor, exists)
|
|
# checkAuthorized: try resolveActive { active=a } catch { return false }; try verify ...
|
|
authorized = And(Not(rev), registry_verify_model(resolved, status, exists, precompile))
|
|
s.add(rev) # resolveActive reverted
|
|
s.add(authorized) # claim it still authorized
|
|
check("H3c fail-closed: a reverting resolveActive forces checkAuthorized to return false", s)
|
|
|
|
# ---- NEG-CTRL H3: a NON-fail-closed consumer that treats a revert as 'authorized'
|
|
# (or lets it bubble as success) authorizes on a dead-ended chain. --------------
|
|
s = Solver()
|
|
startId = Int('startId5')
|
|
rev, resolved = resolveActive_model(startId, status, successor, exists)
|
|
s.add(Select(exists, startId) == 1, Select(status, startId) == REVOKED, Select(successor, startId) == 0)
|
|
# BUG: authorized := True on revert (fail-OPEN)
|
|
buggy_authorized = If(rev, True, False)
|
|
s.add(buggy_authorized)
|
|
check("NEG-CTRL a fail-OPEN consumer authorizes when the successor chain dead-ends", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ---- default+preference resolution terminates & is fail-closed (algorithmFor) ------
|
|
# algorithmFor(account) = preferred==0 ? default : preferred -> a SINGLE reference id,
|
|
# always well-defined (no loop), then fed to resolveActive (proven terminating above).
|
|
# Prove the selection is a total function (always yields exactly one id).
|
|
s = Solver()
|
|
pref, default_, chosen = Int('preferred'), Int('defaultId'), Int('chosen')
|
|
chosen_expr = If(pref == 0, default_, pref)
|
|
s.add(chosen == chosen_expr)
|
|
s.add(Not(Or(chosen == default_, chosen == pref))) # negate: chosen is neither -> impossible
|
|
check("H3d algorithmFor resolution is total (preference else default; always one id)", s)
|
|
|
|
# ------------------------------------------------------------------------------
|
|
print("\n=== SUMMARY ===")
|
|
allok = True
|
|
for name, tag, ok, kind in results:
|
|
print(f" {tag:9} [{kind}] {name}")
|
|
allok = allok and ok
|
|
print()
|
|
print("AereHybridAuthorizer:")
|
|
if allok:
|
|
print(" PROVED (under A1 registry fail-closed verify + A2 loop bound): resolveActive")
|
|
print(" returns ONLY an ACTIVE id, so ONLY an ACTIVE scheme ever authorizes (H1/H1b);")
|
|
print(" a REVOKED id either dead-ends to a fail-closed false or is transparently")
|
|
print(" routed to its ACTIVE successor -- the revoked scheme's verifier never")
|
|
print(" authorizes (H2a/H2b); and the whole resolution pipeline terminates within the")
|
|
print(" loop bound (H3/H3b pigeonhole) and is fail-closed on every revert (H3c/H3d).")
|
|
print(" Four NEG-CTRLs fire, confirming resolveActive, the status gate, and the")
|
|
print(" try/catch fail-closed wrapper are each load-bearing.")
|
|
else:
|
|
print(" NOT fully established (see FAILED / unexpected result above).")
|
|
import sys
|
|
sys.exit(0 if allok else 1)
|