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.
237 lines
13 KiB
Python
237 lines
13 KiB
Python
#!/usr/bin/env python3
|
|
# -----------------------------------------------------------------------------
|
|
# credential_registry_smt.py
|
|
#
|
|
# SMT proof (z3) of the FAIL-CLOSED trust guarantees of Aere Network's federated
|
|
# compliance passport: AereTrustRegistry (the accredited-issuer trusted list) and
|
|
# AereVerifiableCredential (the W3C VC 2.0 anchor + verifier). Plus load-bearing
|
|
# NEGATIVE CONTROLS for the accreditation gate and the append-only status history.
|
|
#
|
|
# Contracts: contracts/contracts/compliance/AereTrustRegistry.sol
|
|
# contracts/contracts/compliance/AereVerifiableCredential.sol
|
|
#
|
|
# The safety-critical, fail-closed guarantees modelled here:
|
|
# A. ISSUANCE requires accreditation. anchorCredential() records a credential ONLY
|
|
# if the issuer isAccredited(issuerId, type) == true, i.e. status == Active AND
|
|
# the credential type is in the issuer's scope, AND the issuer's Falcon-512
|
|
# signature over the credential digest verifies (via the live precompile 0x0AE1
|
|
# through the Trust Registry). A non-accredited issuer cannot issue.
|
|
# B. APPEND-ONLY status history. Every status transition is pushed to an append-only
|
|
# log; a committed record is never rewritten (the current status is a pointer,
|
|
# the history is immutable).
|
|
# C. TERMINAL revocation. Revoked is terminal: no transition path returns a revoked
|
|
# issuer to Active (revoke has no inverse; reinstate only lifts Suspended).
|
|
# D. FAIL-CLOSED verification. isValid()/verifyPresented() return true ONLY when the
|
|
# issuer is (still) accredited, the credential is within its validity window, and
|
|
# it is not revoked on its Bitstring Status List entry; expired, not-yet-valid,
|
|
# revoked, or un-accredited all resolve to NOT valid, never a false positive.
|
|
#
|
|
# Status enum (Solidity): None=0, Active=1, Suspended=2, Revoked=3.
|
|
#
|
|
# We model the guards / transitions as first-order constraints and prove each
|
|
# property by asserting its NEGATION and showing z3 returns UNSAT. Each NEG-CTRL
|
|
# removes exactly one guard and shows the corresponding attack becomes SAT.
|
|
# Append-only history is modelled with the standard "writes only push" relation
|
|
# over an uninterpreted index->value function. 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, If, sat, unsat)
|
|
|
|
NONE, ACTIVE, SUSPENDED, 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()
|
|
print(" witness:", {str(d): m[d] for d in m.decls()})
|
|
return ok
|
|
|
|
def accredited(status, inScope):
|
|
"""AereTrustRegistry.isAccredited: Active AND type in scope (fail-closed otherwise)."""
|
|
return And(status == ACTIVE, inScope)
|
|
|
|
def within_validity(now, validFrom, validUntil):
|
|
"""AereVerifiableCredential.isWithinValidity: not-yet-valid and expired both fail."""
|
|
return And(now >= validFrom, Or(validUntil == 0, now <= validUntil))
|
|
|
|
print("### AereTrustRegistry + AereVerifiableCredential -- FAIL-CLOSED compliance trust\n")
|
|
|
|
# ---- A ISSUANCE requires accreditation. anchorCredential() succeeds ONLY if the
|
|
# issuer is accredited for the type AND its PQC signature verifies. Model the
|
|
# anchor's success predicate = isAccredited AND sigValid AND withinValidity.
|
|
# Negation: an anchor succeeds yet the issuer is NOT accredited. UNSAT. -------
|
|
s = Solver()
|
|
status, inScope = Int('status'), Bool('inScope')
|
|
sigValid = Bool('sigValid')
|
|
now, vFrom, vUntil = Int('now'), Int('vFrom'), Int('vUntil')
|
|
anchor_ok = And(accredited(status, inScope), sigValid, within_validity(now, vFrom, vUntil))
|
|
s.add(anchor_ok)
|
|
s.add(Not(accredited(status, inScope))) # NEGATION: not accredited yet issued
|
|
check("A anchorCredential requires issuer accreditation (non-accredited cannot issue)", s)
|
|
|
|
# ---- A2 A non-accredited issuer is any of: None / Suspended / Revoked, OR Active
|
|
# but out-of-scope. For every such issuer, anchor_ok is false. Negation: some
|
|
# non-accredited issuer anchors. UNSAT. ------------------------------------
|
|
s = Solver()
|
|
status, inScope = Int('status'), Bool('inScope')
|
|
sigValid = Bool('sigValid')
|
|
now, vFrom, vUntil = Int('now'), Int('vFrom'), Int('vUntil')
|
|
s.add(status >= NONE, status <= REVOKED)
|
|
not_accredited = Or(status != ACTIVE, Not(inScope))
|
|
anchor_ok = And(accredited(status, inScope), sigValid, within_validity(now, vFrom, vUntil))
|
|
s.add(not_accredited, anchor_ok) # NEGATION: not-accredited AND anchored
|
|
check("A2 a suspended/revoked/None or out-of-scope issuer cannot anchor", s)
|
|
|
|
# ---- A3 PQC signature is required (fail-closed): anchor_ok => sigValid. Negation:
|
|
# an anchor succeeds with an invalid/tampered issuer signature. UNSAT. -------
|
|
s = Solver()
|
|
status, inScope = Int('status'), Bool('inScope')
|
|
sigValid = Bool('sigValid')
|
|
now, vFrom, vUntil = Int('now'), Int('vFrom'), Int('vUntil')
|
|
anchor_ok = And(accredited(status, inScope), sigValid, within_validity(now, vFrom, vUntil))
|
|
s.add(anchor_ok, Not(sigValid)) # NEGATION
|
|
check("A3 anchorCredential requires a valid Falcon-512 issuer signature (fail-closed)", s)
|
|
|
|
# ---- B APPEND-ONLY status history: a committed record is never silently rewritten.
|
|
# Model the log as index->value with the append relation: a transition only
|
|
# pushes at index == len, leaving every existing index untouched. Negation:
|
|
# some already-committed index changes value. UNSAT under append-only. -------
|
|
hB = Function('hB', IntSort(), IntSort()) # history BEFORE the transition
|
|
hA = Function('hA', IntSort(), IntSort()) # history AFTER the transition
|
|
s = Solver()
|
|
L = Int('L'); newVal = Int('newVal'); i = Int('i')
|
|
s.add(L >= 0)
|
|
# append semantics: existing entries preserved, new entry only at index L.
|
|
s.add(ForAll([i], Implies(And(i >= 0, i < L), hA(i) == hB(i))))
|
|
s.add(hA(L) == newVal)
|
|
j = Int('j')
|
|
s.add(j >= 0, j < L, hA(j) != hB(j)) # NEGATION: a committed entry mutated
|
|
check("B status history is append-only (a committed record cannot be rewritten)", s)
|
|
|
|
# ---- C TERMINAL revocation: from Revoked, no enabled transition returns to Active.
|
|
# Transition guards: suspend(Active->Suspended), reinstate(Suspended->Active),
|
|
# revoke(!Revoked->Revoked). Model the next status as a guarded choice; from
|
|
# Revoked every guard is disabled, so status stays Revoked. Negation: starting
|
|
# Revoked, some transition yields Active. UNSAT. ---------------------------
|
|
s = Solver()
|
|
cur = Int('cur'); nxt = Int('nxt'); op = Int('op') # op: 1=suspend 2=reinstate 3=revoke
|
|
s.add(cur == REVOKED)
|
|
# enabled transitions and their results (a disabled op leaves status unchanged):
|
|
suspend_ok = And(op == 1, cur == ACTIVE)
|
|
reinstate_ok = And(op == 2, cur == SUSPENDED)
|
|
revoke_ok = And(op == 3, cur != REVOKED)
|
|
nxt_def = If(suspend_ok, SUSPENDED,
|
|
If(reinstate_ok, ACTIVE,
|
|
If(revoke_ok, REVOKED, cur))) # no enabled op from Revoked -> unchanged
|
|
s.add(nxt == nxt_def)
|
|
s.add(nxt == ACTIVE) # NEGATION: revoked issuer reinstated
|
|
check("C revocation is terminal (a Revoked issuer can never return to Active)", s)
|
|
|
|
# ---- D FAIL-CLOSED live validity of an ANCHORED credential. isValid() returns true
|
|
# ONLY if the issuer is STILL accredited AND within validity AND not revoked.
|
|
# Negation: isValid true yet un-accredited OR out-of-window OR revoked. UNSAT.
|
|
s = Solver()
|
|
exists = Bool('exists')
|
|
status, inScope = Int('status'), Bool('inScope')
|
|
now, vFrom, vUntil = Int('now'), Int('vFrom'), Int('vUntil')
|
|
revokedBit = Bool('revokedBit')
|
|
isValid = And(exists, accredited(status, inScope),
|
|
within_validity(now, vFrom, vUntil), Not(revokedBit))
|
|
s.add(isValid)
|
|
s.add(Or(Not(accredited(status, inScope)),
|
|
Not(within_validity(now, vFrom, vUntil)),
|
|
revokedBit)) # NEGATION
|
|
check("D isValid is fail-closed (accredited AND within-window AND not-revoked)", s)
|
|
|
|
# ---- D2 FAIL-CLOSED verification of a PRESENTED credential. verifyPresented() adds
|
|
# the PQC signature check on top of D. Negation: true yet a signature/accred/
|
|
# window/revocation failure slipped through. UNSAT. ------------------------
|
|
s = Solver()
|
|
status, inScope = Int('status'), Bool('inScope')
|
|
sigValid = Bool('sigValid')
|
|
now, vFrom, vUntil = Int('now'), Int('vFrom'), Int('vUntil')
|
|
revokedBit = Bool('revokedBit')
|
|
presented_ok = And(accredited(status, inScope), sigValid,
|
|
within_validity(now, vFrom, vUntil), Not(revokedBit))
|
|
s.add(presented_ok)
|
|
s.add(Or(Not(accredited(status, inScope)), Not(sigValid),
|
|
Not(within_validity(now, vFrom, vUntil)), revokedBit)) # NEGATION
|
|
check("D2 verifyPresented is fail-closed (accred + PQC sig + window + not-revoked)", s)
|
|
|
|
# ============================ NEGATIVE CONTROLS ==============================
|
|
|
|
# ---- NEG-CTRL 1 (drop the accreditation check): a BUGGY anchor that skips
|
|
# isAccredited lets a SUSPENDED / REVOKED / out-of-scope issuer anchor a
|
|
# credential. z3 finds a revoked issuer issuing. ---------------------------
|
|
s = Solver()
|
|
status, inScope = Int('status'), Bool('inScope')
|
|
sigValid = Bool('sigValid')
|
|
now, vFrom, vUntil = Int('now'), Int('vFrom'), Int('vUntil')
|
|
# BUG: accreditation gate removed; anchor succeeds on signature + window alone.
|
|
buggy_anchor_ok = And(sigValid, within_validity(now, vFrom, vUntil))
|
|
s.add(buggy_anchor_ok)
|
|
s.add(status == REVOKED) # a revoked issuer...
|
|
s.add(Not(accredited(status, inScope))) # ...is not accredited, yet anchors
|
|
check("no-accreditation-check registry CAN let a revoked issuer issue a credential", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ---- NEG-CTRL 2 (allow a status overwrite): a BUGGY mutable history that rewrites an
|
|
# EXISTING index instead of appending. A committed record is silently changed.
|
|
s = Solver()
|
|
L = Int('L'); j = Int('j'); newVal = Int('newVal')
|
|
s.add(L >= 1, j >= 0, j < L)
|
|
# BUG: the write targets an existing index j (overwrite), so hA(j) != hB(j) is allowed.
|
|
s.add(hA(j) == newVal, hB(j) != newVal) # committed entry rewritten
|
|
check("mutable-history registry CAN silently rewrite a committed status record", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ---- NEG-CTRL 3 (fail-open validity): a BUGGY verifier that ignores the validity
|
|
# window accepts an EXPIRED credential. z3 finds an expired credential passing.
|
|
s = Solver()
|
|
status, inScope = Int('status'), Bool('inScope')
|
|
now, vFrom, vUntil = Int('now'), Int('vFrom'), Int('vUntil')
|
|
revokedBit = Bool('revokedBit')
|
|
# BUG: no within-validity check; validity ignored.
|
|
buggy_valid = And(accredited(status, inScope), Not(revokedBit))
|
|
s.add(buggy_valid)
|
|
s.add(vUntil != 0, now > vUntil) # the credential is EXPIRED
|
|
check("no-validity-window verifier CAN accept an expired credential", 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("AereTrustRegistry + AereVerifiableCredential trust safety:")
|
|
print(" PROVED -- issuance requires accreditation (A/A2) and a valid Falcon-512 issuer")
|
|
print(" signature (A3), the status history is append-only so a committed record cannot be")
|
|
print(" rewritten (B), revocation is terminal (C), and both the anchored (isValid, D) and")
|
|
print(" presented (verifyPresented, D2) verification paths are fail-closed on expired,")
|
|
print(" not-yet-valid, revoked, or un-accredited. Three NEG-CTRLs fire: dropping the")
|
|
print(" accreditation gate lets a revoked issuer issue, a mutable history silently rewrites a")
|
|
print(" committed record, and a fail-open verifier accepts an expired credential.")
|
|
print(" [VERIFY] FALCON-512 PRECOMPILE (0x0AE1): the issuer-signature validity bit is produced")
|
|
print(" by the live native precompile through AerePQCKeyRegistry.verifyWithKey; its soundness")
|
|
print(" (EUF-CMA of Falcon-512, correct precompile parsing) is a trusted primitive, modelled")
|
|
print(" here as the sigValid predicate, not re-proved. The Bitstring Status List and the live")
|
|
print(" issuer status are trusted external oracles for the revocation / accreditation bits.")
|
|
print(" DESIGN: application-layer compliance tooling, no funds, consensus stays classical")
|
|
print(" ECDSA QBFT; this checks the guard logic, not the compiled EVM bytecode. Legal weight")
|
|
print(" of any accreditation is an external regulatory matter, not asserted by the model.")
|
|
else:
|
|
print(" NOT fully established (see FAILED / unexpected CEX above).")
|
|
import sys
|
|
sys.exit(0 if allok else 1)
|