"""CAIN-A75-004 offline verifier (rules embedded verbatim). CAIN-A75-004 proof-review rules. Needs only the `z3-solver` package (no CAIN imports): embedded verbatim in the offline verifier, so an outsider re-runs the same checker on the same obligations. A proof claim says: "this exact source revision satisfies these security properties, checked by this toolchain". The rules treat the proof as evidence with a subject and re-check every part of it: binding the source content hashes to the stated SHA-256 and revision; the spec hashes to the stated spec hash; every property names a subject (function) that appears in the source re-proof every property is re-checked with Z3 here, on a deterministic resource budget (rlimit), not a timer: assumptions satisfiable? no -> VACUOUS (a contradiction "proves" anything) assumptions AND NOT goal satisfiable? no -> PROVED (UNSAT: no counterexample exists) yes -> REFUTED (a counterexample exists) solver returns unknown / budget hit -> NOT_PROVED (fail closed; never upgraded) claims a property the claim calls "proved" must be PROVED here; a claim that says "refuted" or "unproved" is accepted as stated (honest negative results are allowed) toolchain the stated checker must be z3; its stated version is recorded next to the version that re-checked it Verdict: VERIFIED (binding holds and every claimed proof re-proves), else NOT_VERIFIED with every failing check named. Malformed input is NOT_VERIFIED. Counterexample values go in the summary, not in the compared checks, because a solver may pick a different model; PROVED / REFUTED / VACUOUS / NOT_PROVED are stable. This proves the stated properties of the stated model. It does not prove the model matches the real code's semantics, or that the properties are the right ones; a reviewer still reads the spec. """ from __future__ import annotations import hashlib import re RLIMIT = 2_000_000 # deterministic Z3 resource budget per query MAX_SOURCE = 200_000 MAX_SMT = 20_000 _HEX = re.compile(r"^[0-9a-f]{64}$") _ID = re.compile(r"^[A-Za-z0-9_.:\-]{1,80}$") class Bad(ValueError): pass def _sha(text): return hashlib.sha256(text.encode("utf-8")).hexdigest() def spec_hash(properties): import json return hashlib.sha256(json.dumps(properties, sort_keys=True, separators=(",", ":"), ensure_ascii=True).encode()).hexdigest() def _check(decls, assumptions, goal): """Return (status, model_text). status in PROVED, REFUTED, VACUOUS, NOT_PROVED.""" import z3 ctx = z3.Context() def parse(expr_list): script = decls + "\n" + "\n".join(f"(assert {e})" for e in expr_list) return z3.parse_smt2_string(script, ctx=ctx) try: hyp = parse(assumptions) s = z3.Solver(ctx=ctx); s.set("rlimit", RLIMIT); s.add(hyp) r = s.check() if r == z3.unsat: return "VACUOUS", "" if r != z3.sat: return "NOT_PROVED", "assumptions: solver returned unknown within the budget" s2 = z3.Solver(ctx=ctx); s2.set("rlimit", RLIMIT); s2.add(hyp) s2.add(z3.Not(z3.And(*parse([goal]))) if goal else z3.BoolVal(False, ctx)) r2 = s2.check() if r2 == z3.unsat: return "PROVED", "" if r2 == z3.sat: m = s2.model() return "REFUTED", ", ".join(f"{d.name()}={m[d]}" for d in sorted(m.decls(), key=lambda d: d.name())) return "NOT_PROVED", "solver returned unknown within the budget" except z3.Z3Exception as e: raise Bad(f"SMT-LIB does not parse: {str(e)[:160]}") def evaluate(claim): checks, summary = [], {"properties": {}, "counterexamples": {}} def c(cid, ok, detail=""): checks.append({"id": cid, "ok": bool(ok), "detail": detail}) return ok try: import z3 # noqa: F401 except ImportError: return "NOT_VERIFIED", [{"id": "toolchain.available", "ok": False, "detail": "z3-solver is not installed here"}], summary try: if not isinstance(claim, dict) or claim.get("schema") != "cain42.a75.proof.claim.v1": raise Bad("not a cain42.a75.proof.claim.v1 claim") src, spec, tc, claimed = claim.get("source"), claim.get("spec"), claim.get("toolchain"), claim.get("claims") if not all(isinstance(x, dict) for x in (src, spec, tc, claimed)): raise Bad("source, spec, toolchain and claims must be objects") content = src.get("content") if not isinstance(content, str) or not (0 < len(content) <= MAX_SOURCE): raise Bad("source.content must be a non-empty string") props = spec.get("properties") if not isinstance(props, list) or not props or len(props) > 50: raise Bad("spec.properties must be a list of 1-50 properties") if not isinstance(claim.get("signer"), str) or not _ID.match(claim["signer"]): raise Bad("signer must be an identifier") # binding c("binding.source_hash", src.get("sha256") == _sha(content), "the proof is about exactly this source content") c("binding.revision", isinstance(src.get("revision"), str) and re.match(r"^[0-9a-f]{7,64}$", src["revision"] or "") is not None, f"revision {src.get('revision')!r}") c("binding.spec_hash", spec.get("sha256") == spec_hash(props), "the claim names exactly this specification") c("toolchain.checker", tc.get("checker") == "z3", f"checker {tc.get('checker')!r} (this engine re-checks with z3)") summary["toolchain"] = {"claimed": tc.get("version"), "rechecked_with": None} try: import z3 as _z summary["toolchain"]["rechecked_with"] = _z.get_version_string() except Exception: # noqa: BLE001 pass seen = set() for p in props: if not isinstance(p, dict): raise Bad("a property must be an object") pid = p.get("id") if not isinstance(pid, str) or not _ID.match(pid) or pid in seen: raise Bad(f"property id {pid!r} missing, malformed or duplicated") seen.add(pid) decls, assm, goal = p.get("declarations", ""), p.get("assumptions", []), p.get("goal") if not isinstance(decls, str) or not isinstance(assm, list) or not all(isinstance(a, str) for a in assm) or not isinstance(goal, str): raise Bad(f"{pid}: declarations (string), assumptions (strings) and goal (string) are required") if len(decls) + sum(len(a) for a in assm) + len(goal) > MAX_SMT: raise Bad(f"{pid}: SMT-LIB larger than {MAX_SMT} characters") subj = p.get("subject") c(f"{pid}.subject_in_source", isinstance(subj, str) and _ID.match(subj) is not None and re.search(rf"\b{re.escape(subj)}\b", content) is not None, f"subject {subj!r} must appear in the bound source") status, model = _check(decls, assm, goal) summary["properties"][pid] = status if model: summary["counterexamples"][pid] = model said = claimed.get(pid) c(f"{pid}.claim_stated", said in ("proved", "refuted", "unproved"), f"claimed {said!r}") if said == "proved": c(f"{pid}.reproved", status == "PROVED", f"claimed proved; re-checked: {status}") elif said == "refuted": c(f"{pid}.refutation_holds", status == "REFUTED", f"claimed refuted; re-checked: {status}") c(f"{pid}.not_vacuous", status != "VACUOUS", "the assumptions are satisfiable" if status != "VACUOUS" else "the assumptions contradict each other") extra_claims = sorted(set(claimed) - seen) c("claims.no_unknown_properties", not extra_claims, f"claims about properties not in the spec: {extra_claims}" if extra_claims else "") except Bad as e: checks.append({"id": "input.well_formed", "ok": False, "detail": str(e)}) return "NOT_VERIFIED", checks, summary except Exception as e: # noqa: BLE001 checks.append({"id": "input.error", "ok": False, "detail": f"{type(e).__name__}: {e}"[:200]}) return "NOT_VERIFIED", checks, summary return ("VERIFIED" if all(x["ok"] for x in checks) else "NOT_VERIFIED"), checks, summary # ---------------------------------------------------------------------------- offline verifier (no CAIN imports) # Every name below is prefixed _kit_verifier_ / _b64 / _hl / _json / _sys so it cannot shadow a name in the rules above. import base64 as _b64, hashlib as _hl, json as _json, sys as _sys _KIT_VERIFIER_GENESIS = _hl.sha256(b"cain42.a75.proof.genesis").hexdigest() def _kit_verifier_canon(o): return _json.dumps(o, sort_keys=True, separators=(",", ":"), ensure_ascii=True).encode() def _kit_verifier_sha(o): return _hl.sha256(_kit_verifier_canon(o)).hexdigest() def _kit_verifier_main(argv): from cryptography.hazmat.primitives.asymmetric.ed25519 import Ed25519PublicKey if len(argv) < 2: print("usage: verify_offline.py run.json --pinned-key BASE64"); return 2 run = _json.load(open(argv[1])) pin = argv[argv.index("--pinned-key") + 1] if "--pinned-key" in argv else None problems, prev, recs = [], _KIT_VERIFIER_GENESIS, run.get("records") or [] for i, r in enumerate(recs): body = {k: v for k, v in r.items() if k not in ("record_hash", "signature_b64")} if _kit_verifier_sha(body) != r.get("record_hash"): problems.append(f"record {i}: record_hash does not match") if body.get("subject_sha256") != _kit_verifier_sha(body.get("subject")): problems.append(f"record {i}: subject_sha256 does not match") if pin and r.get("public_key_b64") != pin: problems.append(f"record {i}: different key than the pinned one") try: Ed25519PublicKey.from_public_bytes(_b64.b64decode(pin or r.get("public_key_b64"))).verify( _b64.b64decode(r.get("signature_b64", "")), str(r.get("record_hash")).encode()) except Exception: problems.append(f"record {i}: signature does not verify") if r.get("prev_record_hash") != prev: problems.append(f"record {i}: chain link broken") v, checks, _ = evaluate(r.get("subject")) if v != r.get("verdict") or checks != r.get("checks"): problems.append(f"record {i}: re-running the rules gives {v}, the record says {r.get('verdict')}") prev = r.get("record_hash") if run.get("run_hash") != _kit_verifier_sha([r.get("record_hash") for r in recs]): problems.append("run_hash does not match") for p in problems: print(" -", p) if not pin: print("WARNING: no --pinned-key given; the signature was checked against the key inside the file") print("VERDICT:", "VERIFIED" if not problems else "TAMPERED OR INVALID", f"(CAIN-A75-004, {len(recs)} record(s), verdicts {run.get('verdicts')})") return 0 if not problems else 1 if __name__ == "__main__": _sys.exit(_kit_verifier_main(_sys.argv))