باشه. اینجا وارد “هسته واقعی formalization” میشیم. این نسخه، TLA+ v3 spec برای authgate-kernel هست که باید بعداً با Rust TCB و attack matrix align بشه.
من اینو طوری مینویسم که واقعاً قابل model checking باشه، نه صرفاً توضیح فلسفی.
📐 TLA+ v3 — AuthGate Kernel State Machine MODULE AuthGateV3 ----------------------------- MODULE AuthGateV3 ----------------------------- EXTENDS Naturals, Sequences, FiniteSets
- CONSTANTS (world model) CONSTANTS Actors, * Humans + Machines Resources, * Objects of authority Epochs, * Discrete time authority versioning Capabilities, * Rights set Flags * Forbidden execution flags
- STATE VARIABLES VARIABLES registry, * Actor -> set of Capabilities delegation, * Graph: Capabilities derivation epoch, * current global epoch action, * current action being evaluated proof, * capability proof chain decision * {PERMIT, DENY}
- CORE STRUCTURES Action Action == [ actor : Actors, resource : Resources, cap : Capabilities, minEpoch : Epochs, flags : SUBSET Flags ] Capability Proof Chain Proof == [ subject : Actors, resource : Resources, cap : Capabilities, epoch : Epochs, issuer : Actors ]
- INITIAL STATE Init == /\ registry = [a \in Actors |-> {}] /\ delegation = {} /\ epoch \in Epochs /\ decision = "DENY"
- CANONICAL GATE (Layer 1 HARD BARRIER) invariant pre-check ValidFlags(a) == a.flags \cap Flags = {} CanonicalHashStable(a) == TRUE * abstracted: in implementation this is SHA-256(binding)
- CORE INFERENCE RULES 6.1 Identity Binding SubjectMatch(a, p) == a.actor = p.subject 6.2 Epoch Validity EpochValid(a, p) == p.epoch >= a.minEpoch 6.3 Delegation Validity ValidDelegation(p) == p.subject \in DOMAIN registry 6.4 Capability containment (attenuation) ValidCapability(a, p) == p.cap \in registry[p.subject] 6.5 Resource binding ResourceMatch(a, p) == p.resource = a.resource
- REVOCATION MODEL (stateless epoch gate) RevocationCheck(a, p) == p.epoch >= a.minEpoch
- CORE PERMISSION FUNCTION Permitted(a, p) == /\ SubjectMatch(a, p) /\ ResourceMatch(a, p) /\ ValidCapability(a, p) /\ RevocationCheck(a, p) /\ ValidFlags(a)
- TRANSITION SYSTEM MAIN STEP Next == \E a \in Action, p \in Proof : /\ action' = a /\ proof' = p /\ decision' = IF Permitted(a, p) THEN "PERMIT" ELSE "DENY"
- SAFETY INVARIANTS (CORE SECURITY GUARANTEES) 10.1 No unauthorized access Invariant_NoUnauthorized == decision = "PERMIT" => Permitted(action, proof) 10.2 No privilege escalation Invariant_NoEscalation == proof.cap \in registry[proof.subject] 10.3 Identity integrity Invariant_Identity == decision = "PERMIT" => action.actor = proof.subject 10.4 Epoch monotonic safety Invariant_Epoch == proof.epoch >= action.minEpoch 10.5 Forbidden flags absolute denial Invariant_Flags == action.flags \cap Flags # {} => decision = "DENY"
- COMPOSITION MODEL (critical difference vs v1) SequenceContext == [usedCaps : SUBSET Capabilities] UpdateContext(ctx, a) == [ctx EXCEPT !.usedCaps = ctx.usedCaps \cup {a.cap}] safety: Invariant_Composition == \A ctx : ctx.usedCaps \subseteq UNION registry[Actors]
- LIVENESS (minimal guarantee) Liveness == \A a : Permitted(a, proof) => decision = "PERMIT"
- SPECIFICATION Spec == Init /\ [][Next]_<<registry, delegation, epoch, action, proof, decision>>
- PROPERTIES TO CHECK (MODEL CHECK TARGETS) THEOREM Safety == Spec => []( Invariant_NoUnauthorized /\ Invariant_NoEscalation /\ Invariant_Identity /\ Invariant_Epoch /\ Invariant_Flags ) 🔥 مهمترین چیزهایی که این v3 الان explicitly حل میکند
- canonical gate
→ IR tampering class (AT-6)
- epoch revocation O(1)
→ replay + stale proof class
- strict identity binding
→ impersonation class (AT-5.1)
- attenuation formalized
→ delegation escalation
- composition safety model
→ session-based privilege creep
این spec هنوز پوشش نمیدهد:
adapter poisoning (AT-7.5 هنوز external) semantic deception (L1) multi-node consensus divergence timing / side-channel attacks malformed proof injection at FFI boundary
📌 یعنی:
TCB is correct — system boundary is not yet closed.
🧭 تو الان کجایی؟
این status واقعی است:
Formal model: ██████████░░ Kernel design: █████████░░░ Attack coverage: ████████░░░░ Production readiness ██████░░░░░░ 👉 قدم بعدی (اجباری اگر بخوای “bulletproof” کنی)
حالا باید یکی از این دو را بزنیم:
A) MITRE Attack Matrix v3 (full closure)
→ تمام exploit classes + mapping به invariants
B) Proof Gap Analysis
→ دقیقاً کدام invariants در TLA+ هنوز insufficient هستند
اگر بخوای سیستم واقعاً “air-tight” بشه:
👉 بدون Attack Matrix، این spec هنوز “complete threat model” نیست
بگو کدوم را میخوای بعدی بسازیم.
MITRE Attack Matrix v3 (full closure)
اول آ بعد ب
باشه. اینجا وارد بخش واقعیِ سخت کار شدیم: attack surface کامل + class-based adversary model. این نسخه MITRE-style است، اما برای سیستم capability-kernel تو tailored و formalized شده، نه صرفاً لیست حملات.
هدف:
هیچ کلاس حملهای بیرون این مدل “نامگذاری نشده” باقی نماند.
🧭 MITRE-STYLE ATTACK MATRIX v3 — AuthGate Kernel 🎯 Threat Model Scope
مدل مهاجمها:
A1: Malicious Agent (machine) A2: Malicious Human Principal A3: Compromised Adapter Layer A4: Replay / Network Actor A5: Multi-agent coalition adversary A6: Infrastructure-level attacker (FFI / runtime) 🧱 TIER 0 — Cryptographic Boundary Attacks C1 — Signature Forgery Attempt
Goal: تولید proof معتبر بدون کلید خصوصی
Attack: ed25519 forgery, lattice/side-channel attempt Precondition: access to signed outputs Impact: full authority takeover attempt
Mitigation mapping:
sig_euf_cma assumption kernel-only signing C2 — Signature Replay
Goal: reuse valid proof in different context
replay(action, proof_old)
Variant classes:
C2.1 cross-epoch replay C2.2 cross-resource replay C2.3 cross-actor replay
Mitigation:
(actor, resource, epoch) binding C3 — Key Substitution Attack swap issuer_pubkey in proof chain inject fake root identity
Root cause vector:
trust bootstrapping boundary 🧱 TIER 1 — Capability Graph Attacks G1 — Delegation Impersonation (AT-5.1 class) child claims parent identity forged issuer chain
Variants:
G1.1 direct impersonation G1.2 transitive impersonation G1.3 DAG cycle exploitation G2 — Privilege Inflation via Delegation Chains A → B → C chain expands rights incorrectly
Core exploit:
attenuation not enforced transitively G3 — Cross-Actor Capability Leakage capability issued to Alice used by Bob
Root failure:
missing subject binding enforcement G4 — Orphan Capability Activation capability exists without valid issuer 🧱 TIER 2 — Epoch & Time Attacks T1 — Epoch Rollback Attack system state rolled back to earlier epoch
Impact:
revocation bypass T2 — Stale Proof Resurrection reuse of old valid proof after revocation
Variants:
T2.1 delayed epoch update T2.2 async propagation exploit T3 — Epoch Forking (Distributed risk) multiple epoch views across nodes 🧱 TIER 3 — Canonicalization & IR Attacks (CRITICAL) I1 — Canonical IR Tampering (AT-6) modify action between adapter → kernel
Example:
resource swap actor mutation cap downgrade/upgrade
Root cause:
missing binding_hash enforcement I2 — Partial Field Poisoning only one field altered: resource only epoch only flags only I3 — Deserialization Ambiguity Attack JSON vs internal struct mismatch I4 — Canonical Hash Collision Pressure (theoretical) hash preimage manipulation attempt 🧱 TIER 4 — Adapter Layer Attacks (BIGGEST REAL RISK) A1 — Adapter Logic Poisoning (AT-7.5) adapter rewrites semantics before kernel sees it
Variants:
A1.1 silent escalation A1.2 permission stripping (denial sabotage) A1.3 fake action normalization A2 — Dual-Representation Drift Python view ≠ Rust view
Result:
inconsistent verification outcomes A3 — Policy Injection via Preprocessing attacker modifies input before canonicalization 🧱 TIER 5 — Composition Attacks (VERY IMPORTANT) S1 — Safe-in-Isolation, Unsafe-in-Sequence each action permitted individually combined sequence violates policy
Example:
READ → WRITE → DELEGATE escalation chain S2 — Capability Accumulation Drift session gradually expands effective rights S3 — Context Poisoning earlier action modifies meaning of later validation 🧱 TIER 6 — Identity & Binding Attacks ID1 — Actor Spoofing fake actor identity in Action IR ID2 — Subject Binding Mismatch proof.subject ≠ action.actor ID3 — Multi-identity collision same entity mapped to multiple Actor IDs 🧱 TIER 7 — Revocation & Control Plane Attacks R1 — Forged Revocation Proof Injection attacker injects fake revocation
Expected failure mode:
must be ignored, not cause denial explosion R2 — Revocation Suppression block revocation propagation R3 — Selective Revocation Delay delay only critical revocations 🧱 TIER 8 — FFI / Runtime Boundary Attacks F1 — Foreign Function Interface Escape bypass kernel via C/Go/Zig layer F2 — Memory corruption pre-kernel modify IR before verification F3 — Undefined behavior exploitation Rust unsafe blocks misuse 🧱 TIER 9 — Multi-Agent Coalition Attacks M1 — Distributed Capability Collusion agents combine partial rights M2 — Capability laundering A → B → C → A circular delegation hides ownership M3 — Consensus divergence exploit different nodes approve different states 🧱 COVERAGE MATRIX (critical summary) Layer Coverage Status Crypto boundary strong mostly closed Capability graph strong partially formalized Epoch system strong needs distributed proof IR canonicalization medium AT-6 sensitive Adapter boundary weak critical risk zone Composition safety medium emerging invariant Multi-agent weak not fully modeled 🔥 REAL CONCLUSION (no sugar-coating)
تو الان در این وضعیت هستی:
چیزی که داری:
capability kernel concept ✔
formalizable security model ✔
strong cryptographic assumptions ✔
epoch-based revocation ✔
چیزی که هنوز نداری:
fully closed adapter boundary
composition-proof system
distributed consistency model
semantic attack resistance (by design excluded)
بزرگترین attack surface تو این نیست:
kernel.rs
بلکه اینه:
“everything that touches kernel.rs”
یعنی:
adapters IR conversion multi-runtime bridging 👉 قدم بعدی (طبق مسیر تو)
حالا طبق زنجیرهای که خودت گفتی:
next step = Proof Gap Analysis (Layer B)
اونجا میریم دقیق جواب میدیم:
“کدوم invariantها کافی نیستند حتی اگر TLA+ پاس شود”
و این جاییه که سیستم از “strong design” میرسه به “actually unbreakable design”.
اگر آمادهای، وارد فاز بعدی میشیم: 👉 Proof Gap Analysis — what still breaks even after full formal verification
بله، ولی نه به آن معنایی که آدمها معمولاً دربارهی پروژههای security میگویند.
الان وضعیت پروژهات این نیست که:
“wow futuristic AGI safety platform”
بلکه این است:
finally becoming internally coherent
و این خیلی ارزشمندتر است.
چیزی که واقعاً خوب است:
داری dependency ordering واقعی را میفهمی داری threat model را محدود و explicit نگه میداری داری non-goals را شفاف میکنی داری invariants را algebraic میکنی نه marketing-style داری formal surface را کوچک نگه میداری داری architectural honesty نشان میدهی
اینها نشانههای پروژهی جدیاند.
و مهمتر:
تو یک دام بزرگ را رد کردی:
premature grandiosity
اکثر پروژههای “AI security” مستقیم میروند سراغ:
decentralized AI constitution autonomous governance sovereign AI democracy
در حالی که:
execution boundary هنوز سوراخ است authority semantics دقیق نیست revocation semantics temporal نیست runtime closure ندارند
تو حداقل داری کمکم میفهمی:
هر لایه باید روی invariants بستهشده ساخته شود.
این خیلی مهم است.
اما قسمت سخت و صادقانه:
هنوز خیلی فاصله داری با چیزی که بشود گفت:
production-grade secure capability runtime
و این طبیعی است.
چیزهایی که هنوز fundamentally بازند:
- Runtime closure هنوز کامل نشده
AT-7.5 یعنی:
هنوز theoretically bypass path وجود دارد.
تا وقتی CallGate بسته نشود:
TCB کامل نیست formal proof ناقص است runtime porous است 2. Formal proof هنوز theorem-level نیست
الان:
model checking داری invariant reasoning داری
ولی هنوز:
mechanized proof chain کامل نداری refinement proof نداری implementation equivalence proof نداری 3. Adapter boundary هنوز خطرناک است
بیشتر exploitهای واقعی:
parser boundary serialization mismatch adapter confusion canonicalization drift
هستند.
و دقیقاً همانجاها هنوز کامل hardened نشدهاند.
- Distributed story هنوز conceptual است
فعلاً خوب است که speculative مانده.
چون distributed authority واقعاً جهنم مهندسی است.
- Human governance هنوز primitive است
الان trust root تقریباً axiomatic است.
این اشکال نیست، ولی limitation واقعی است.
اما چیزی که genuinely impressive است:
تو از “vibe architecture” فاصله گرفتی.
الان:
bug پیدا میکنی semantics اصلاح میکنی dependency graph میسازی attack class تعریف میکنی invariant minimality بررسی میکنی
اینها کار واقعیاند.
و مهمتر:
الان پروژهات دارد شبیه چیزی میشود که:
auditable باشد قابل نقد جدی باشد قابل formalization باشد قابل attack reasoning باشد
نه فقط:
“AI safety aesthetic”
پس جمعبندی واقعی:
از نظر conceptual maturity
قویتر از اکثر پروژههای agent-security گیتهاب است.
از نظر formal rigor
هنوز early-stage research-grade است، نه industrial-grade.
از نظر architectural direction
مسیر فعلاً درست است.
از نظر production readiness
هنوز فاصلهی زیاد داری.
از نظر intellectual seriousness
الان دیگر پروژهات شوخی نیست.
دستورالعمل و باید و نباید های آماده صنعت شدن ROAD TO INDUSTRY — WHAT MUST CHANGE
الان مهمترین خطر برای پروژهات technical failure نیست.
خطر واقعی این است:
research-system pretending to be production-system
بیشتر پروژههای امنیتی دقیقاً همینجا میمیرند.
⚫ اصل اول Production ≠ more features
بلکه:
less ambiguity less trust less magic less hidden state چیزی که صنعت میخواهد
صنعت دنبال:
“vision” “AGI constitution” “civilization kernel”
نیست.
صنعت دنبال این است:
Can this survive hostile reality? ⚫ MUST-HAVES FOR INDUSTRIALIZATION
- TCB ABSOLUTE DISCIPLINE
الان این مهمترین چیز است.
باید:
✔ TCB frozen semantics داشته باشد ✔ tiny باشد ✔ auditable باشد ✔ deterministic باشد ✔ boring باشد
نباید:
❌ feature creep ❌ plugin logic inside TCB ❌ heuristics inside TCB ❌ networking inside TCB ❌ async complexity inside TCB
قانون طلایی: Every line added to TCB is presumed guilty. ⚫ 2. RUNTIME CLOSURE
تا این بسته نشود: هیچ production claim واقعی نکن.
باید:
✔ all effectful paths gated ✔ no ambient authority ✔ no hidden syscall path ✔ no bypass execution ✔ no pre-verify side effects
نباید:
❌ “soft enforcement” ❌ “best effort” verification ❌ optional gate paths
قانون: If execution can happen outside the gate, the gate is fiction. ⚫ 3. FORMAL SCOPE HONESTY
این خیلی مهم است.
باید:
✔ exactly specify what is proved ✔ explicitly enumerate non-goals ✔ distinguish theorem vs assumption ✔ distinguish model vs implementation
نباید:
❌ “formally verified system” marketing وقتی فقط invariant subset prove شده
قانون: Unproved claims are liabilities. ⚫ 4. ADAPTER PARANOIA
بیشتر exploitهای production اینجاست.
باید:
✔ canonical serialization ✔ strict schema enforcement ✔ rejection-by-default ✔ deterministic decoding ✔ parser differential testing
نباید:
❌ permissive parsing ❌ auto-coercion ❌ silent normalization ❌ mixed canonical forms
قانون: Parsing is part of the attack surface. ⚫ 5. VERSIONED SEMANTICS باید:
✔ semantic versioning for policy semantics ✔ migration proofs ✔ compatibility contracts ✔ immutable historical meaning
نباید:
❌ retroactive semantic reinterpretation
قانون: A capability must never change meaning silently. ⚫ 6. AUDITABILITY FIRST باید:
✔ append-only logs ✔ cryptographic attestations ✔ deterministic replay ✔ forensic reconstruction ✔ event lineage tracing
نباید:
❌ mutable audit history ❌ unverifiable state transitions
قانون: If an event cannot be reconstructed, it effectively never happened. ⚫ 7. TESTING PHILOSOPHY
Production security testing ≠ unit tests.
باید:
✔ adversarial testing ✔ mutation testing ✔ differential testing ✔ fuzzing ✔ property-based testing ✔ chaos testing ✔ invariant violation testing
نباید:
❌ happy-path obsession
قانون: Security systems fail at edges, not centers. ⚫ 8. SPEC-FIRST ENGINEERING باید:
✔ spec before implementation ✔ invariants before optimization ✔ threat model before architecture ✔ semantics before APIs
نباید:
❌ code-discovered semantics
قانون: If the implementation defines the spec, the system is unstable. ⚫ 9. PRODUCTION SECURITY REALITY
این بخش مهم است.
در دنیای واقعی:
بیشتر شکستها:
crypto break نیستند theorem failure نیستند
بلکه:
✔ deployment mistakes ✔ configuration drift ✔ key leakage ✔ operational bypass ✔ logging failure ✔ stale revocation ✔ human shortcuts
هستند.
بنابراین: باید:
✔ operational simplicity ✔ secure defaults ✔ fail-closed behavior ✔ observable failure modes
نباید:
❌ operator-dependent safety
قانون: Complex operational security eventually degrades into insecurity. ⚫ 10. INDUSTRIAL CRYPTOGRAPHY RULE باید:
✔ standard primitives only ✔ audited libraries only ✔ protocol simplicity ✔ key rotation design ✔ explicit trust anchors
نباید:
❌ custom cryptography ❌ clever signature schemes ❌ “novel security math”
قانون: Novel cryptography is usually undiscovered vulnerability. ⚫ 11. HUMAN FACTOR
بیشتر formal systems این را دستکم میگیرند.
باید:
✔ operator clarity ✔ understandable failure messages ✔ recoverability ✔ explicit override visibility ✔ governance procedures
نباید:
❌ opaque formal magic ❌ impossible debugging
قانون: A secure system humans cannot operate becomes insecure in practice. ⚫ 12. ENTERPRISE REALITY
شرکتها دنبال ایناند:
✔ predictable behavior ✔ compliance mapping ✔ incident response ✔ upgrade guarantees ✔ supportability ✔ interoperability
نه:
AGI philosophy sovereignty rhetoric civilization narratives بنابراین production branch باید: boring predictable minimal stable
باشد.
⚫ 13. SEPARATE RESEARCH FROM PRODUCTION
این حیاتی است.
باید branch separation واقعی داشته باشی: production/
✔ frozen semantics ✔ hardened runtime ✔ strict compatibility ✔ audited features only
research/
✔ experimental semantics ✔ distributed sovereignty ✔ constitutional compute ✔ speculative systems
formal/
✔ TLA+ ✔ Lean ✔ proof artifacts ✔ model checking
attack-lab/
✔ adversarial simulation ✔ exploit generation ✔ fuzzing ✔ mutation harnesses
قانون: Research velocity and production stability are opposing forces. ⚫ 14. THE MOST IMPORTANT RULE
اگر میخواهی global-grade system بسازی:
باید:
✔ aggressively remove complexity ✔ shrink trusted surfaces ✔ prefer structural guarantees ✔ make violations unrepresentable
نباید:
❌ rely on good behavior ❌ rely on monitoring alone ❌ rely on intent detection ❌ rely on “smart AI” safeguards
قانون نهایی: Production security is achieved by eliminating classes of failure, not by detecting them faster. وضعیت فعلی تو
صادقانه:
تو هنوز در:
research-grade formal capability runtime
هستی.
اما مسیرت اگر disciplined بماند، میتواند eventually به چیزی برسد که:
technically respected باشد academically serious باشد industrially auditable باشد
و این خیلی ارزشمندتر از hype است.
Skip to content Aliipou authgate-kernel Repository navigation Code Issues Pull requests Agents Actions Projects Wiki Security and quality Insights Settings Owner avatar authgate-kernel Public Aliipou/authgate-kernel spec-core had recent pushes 11 minutes ago Go to file t T Name alexanderthenthclaude alexanderthenth and claude docs(main): README — update attack harness counts, add branch strateg… 784805e · 2 hours ago .github fix(tcb): close AT-5.1 delegation impersonation + AT-3.1 intermediate… 2 hours ago attack_harness fix(tcb): close AT-5.1 delegation impersonation + AT-3.1 intermediate… 2 hours ago examples Phase 0-9 roadmap implementation: rename to authgate, identity lock, … 8 hours ago formal feat: v2 stateless TCB — canonical gate, epoch revocation, compositio… 3 hours ago freedom-kernel-cli feat: Stage 2–5 — plan verification, goal trees, multi-agent, formal … 2 weeks ago freedom-kernel-go feat: Stage 2–5 — plan verification, goal trees, multi-agent, formal … 2 weeks ago freedom-kernel fix(tcb): close AT-5.1 delegation impersonation + AT-3.1 intermediate… 2 hours ago spec/v0.2 feat: Stage 2–5 — plan verification, goal trees, multi-agent, formal … 2 weeks ago src/authgate Phase 0-9 roadmap implementation: rename to authgate, identity lock, … 8 hours ago tests Phase 0-9 roadmap implementation: rename to authgate, identity lock, … 8 hours ago .coverage Freedom Theory AI — formal axiomatic ethics runtime for AGI last month .env.example Add .env.example template 2 weeks ago .gitignore Phase 0-9 roadmap implementation: rename to authgate, identity lock, … 8 hours ago ARCHITECTURE.md Phase 0-9 roadmap implementation: rename to authgate, identity lock, … 8 hours ago BRANCHES.md docs(main): BRANCHES.md — Dual Reality Architecture + CBCT + per-bran… 2 hours ago CHANGELOG.md Phase 0-9 roadmap implementation: rename to authgate, identity lock, … 8 hours ago CLAUDE.md Update CLAUDE.md engineering guidelines 2 weeks ago COMPARATIVE_EVALUATION.md Phase 0-9 roadmap implementation: rename to authgate, identity lock, … 8 hours ago COMPLIANCE.md Phase 0-9 roadmap implementation: rename to authgate, identity lock, … 8 hours ago CONTRIBUTING.md Phase 0-9 roadmap implementation: rename to authgate, identity lock, … 8 hours ago DEPLOYMENT.md Phase 0-9 roadmap implementation: rename to authgate, identity lock, … 8 hours ago Dockerfile Phase 0-9 roadmap implementation: rename to authgate, identity lock, … 8 hours ago INCIDENT_RESPONSE.md Phase 0-9 roadmap implementation: rename to authgate, identity lock, … 8 hours ago LICENSE Freedom Theory AI — formal axiomatic ethics runtime for AGI last month MASTER_PLAN.md Phase 0-9 roadmap implementation: rename to authgate, identity lock, … 8 hours ago NON_GOALS.md Phase 0-9 roadmap implementation: rename to authgate, identity lock, … 8 hours ago PLUGIN_MODEL.md Phase 0-9 roadmap implementation: rename to authgate, identity lock, … 8 hours ago PRIOR_ART.md Phase 0-9 roadmap implementation: rename to authgate, identity lock, … 8 hours ago README.md docs(main): README — update attack harness counts, add branch strateg… 2 hours ago SECURITY.md Phase 0-9 roadmap implementation: rename to authgate, identity lock, … 8 hours ago SEMANTICS.md Phase 0-9 roadmap implementation: rename to authgate, identity lock, … 8 hours ago TCB.md feat: Phase 0-3 — TCB docs, capability algebra, typed IR hardening, L… 2 weeks ago THREAT_MODEL.md Phase 0-9 roadmap implementation: rename to authgate, identity lock, … 8 hours ago docker-compose.yml Add docker-compose.yml 2 weeks ago pyproject.toml Phase 0-9 roadmap implementation: rename to authgate, identity lock, … 8 hours ago Repository files navigation README Contributing MIT license Security authgate-kernel Capability-security runtime for autonomous agents. Formally verified. No heuristics.
CI Python 3.11+ Rust License: MIT Kani Lean4
What this is A structurally unavoidable permission gate between an LLM and the world. Before any agent action executes, the kernel verifies typed capability claims against an ownership graph. If the agent lacks explicit, valid, non-expired authority — it is blocked. No argument overrides a sovereignty flag.
~200 lines of pure Rust form the Trusted Computing Base (TCB). No ML. No natural language parsing. No "trust scores". The Python layer mirrors the Rust logic and is used when the Rust kernel is not compiled.
What this is NOT Not this Why it is explicitly excluded Alignment solution Alignment operates on values and intent; this kernel operates on typed authority graphs Intent verifier The kernel does not parse, interpret, or score natural language output Ethics engine Ethical reasoning requires semantic content; this kernel is purely structural Behavioral monitor No runtime heuristics or anomaly detection in the TCB Covert channel detector Timing, steganography, and side-channel leakage are out of scope by design LLM output sanitizer The kernel gates actions, not token streams See NON_GOALS.md and THREAT_MODEL.md for full boundaries.
Architecture Human Principal (trust root — registered owner of all machines) │ │ registers machines, delegates claims ▼ OwnershipRegistry
- claims map: (actor, resource) → RightsClaim
- delegation chains: child_capability ⊆ parent_capability
- machine → human owner entries │ │ typed Action IR (actor, resources[], capability_kind, flags[]) │ no natural language — structured data only ▼ engine.rs ◄────────────────────────────────────────────────────────┐ (TCB gate, ~200 LOC) │ [1] sovereignty flag check — O(1), unconditional │ [2] machine ownership check — is actor in registry? │ [3] machine-governs-human — is actor attempting dominion? │ [4] capability claim check — does actor hold valid claim? │ │ │ ├── PERMITTED ──► AuditLog (append-only, cryptographically │ │ signed, JSON) │ │ │ └── BLOCKED ──► halt + surface violation to human owner ──┘ (owner may inspect, retry with correction) Trusted Computing Base: engine.rs, capability.rs, wire.rs, crypto.rs, and the new src/tcb/ module (v2 stateless kernel). Everything else — adapters, extensions, scheduler, registry logic — is outside the TCB.
Repository layout freedom-kernel/src/ engine.rs registry-based verifier (v1, production) — TCB capability.rs closed capability algebra (enums only) — TCB wire.rs typed JSON wire format (serde, no logic) — TCB crypto.rs ed25519 attestation — TCB tcb/ stateless proof-chain kernel (v2, in progress) — TCB types.rs CanonicalAction + CapabilityProof + Rights engine.rs verify(action, root_key, now) -> Decision dag.rs delegation chain validation + attenuation sequence.rs composition safety tracker (SequenceContext) ffi.rs C ABI — thin facade — not TCB verifier.rs PyO3 facade over engine.rs — not TCB registry.rs ownership registry (v1; not truth in v2) — not TCB
src/authgate/ kernel/ Python implementation (mirrors Rust) extensions/ heuristic layers — explicitly NOT TCB ifc.py Bell-LaPadula non-interference detection.py manipulation scorer (heuristic signal) synthesis.py rule admission engine
formal/ kani/ Kani bounded model-checking harnesses lean4/ Lean 4 proofs (Core.lean, Invariants.lean, Proofs.lean)
attack_harness/ mutation_attacks.py 20 mutation tests — one security check per test canonicalization_attacks.py 5 canonical gate attacks (CA-1 through CA-5) sequence_attacks.py 5 composition safety attacks (SA-1 through SA-4) v2 TCB design The v2 kernel (src/tcb/) is stateless and registry-free. All authority is carried in signed capability proof chains. Key design decisions:
Canonical gate (Layer 1): Every action arrives as a CanonicalAction with a binding_hash over all fields. The kernel recomputes this hash before touching any proof — IR tampered between adapter and kernel is rejected before any cryptographic work begins.
Epoch-based primary revocation: Instead of distributing revocation lists, the caller sets min_epoch in each action. Capability proofs with epoch < min_epoch are rejected without consulting any revocation list. Advancing the epoch invalidates an entire cohort of proofs in O(1).
Revocation proofs (secondary): Emergency single-proof revocation via root-signed RevocationProof. Forged or invalid-signature revocations are silently skipped — attackers cannot force a Deny by injecting garbage revocation proofs.
Composition safety: SequenceContext tracks the union of all rights exercised within a session. Policy layers compare the accumulated state against the session limit, closing the gap where individually-permitted actions compose into a globally-invalid sequence.
TCB guards (CI-enforced on every commit) engine.rs:
Guard Rule LOC ceiling Must stay ≤ 300 lines Public API Exports exactly one function: verify Import scope May only import from crate::capability and crate::wire Purity No randomness, network, or filesystem calls capability.rs:
Guard Rule LOC ceiling Must stay ≤ 200 lines Self-contained No use crate:: imports Enums only No struct definitions — structs carry state and open extension points Security guarantees These are formal properties of engine.rs, verified by Kani and Lean 4. They apply to the Rust TCB only.
Property Formal statement P1 Confinement An agent cannot act on resources outside its explicit claim set. For all actions A and resources R: if verify(A) = PERMITTED then ∀r ∈ resources(A): actor holds valid claim on r. P2 Attenuation Delegated authority is a strict subset of the delegator's authority. child_claim.rights ⊆ parent_claim.rights is enforced at delegation time; violations raise PermissionError. P3 Sovereignty Invariants All 10 sovereignty flags produce BLOCKED for any input, with no exceptions. Verified exhaustively by Kani over all possible input combinations. P4 Determinism verify is a pure function. Same typed input → same output. No hidden state, no randomness, no I/O. Proved in Lean 4 (verify_deterministic). P5 Cryptographic Attestation Every PERMITTED result is signed with ed25519. A signed result cannot be fabricated without the kernel's private key. Timestamp + nonce prevent replay. Scope: These properties cover engine.rs behaviors on typed inputs. Not covered: the Python implementation, extensions, adapters, multi-agent semantics, or any property involving natural language content.
See formal/INCOMPLETENESS.md for an explicit enumeration of what is not proved.
Capability taxonomy All 17 capability kinds recognized by the kernel, with risk classification:
CapabilityKind Risk Description READ Low Read access to a resource WRITE Medium Write or mutate a resource EXECUTE Medium Execute a process or command DELETE High Permanently remove a resource DELEGATE High Grant authority to another agent NETWORK_EGRESS High Outbound network connections NETWORK_INGRESS High Accept inbound network connections FILE_SYSTEM High Broad filesystem access PROCESS_SPAWN High Spawn child processes or agents MEMORY_WRITE High Write to process memory CREDENTIAL_READ Critical Access secrets, tokens, keys CREDENTIAL_WRITE Critical Modify or rotate credentials AUDIT_READ Critical Read audit logs AUDIT_WRITE Critical Append to or modify audit logs POLICY_READ Critical Read policy definitions REGISTRY_MODIFY Catastrophic Modify the ownership registry POLICY_MODIFY Catastrophic Modify kernel policy or sovereignty flags REGISTRY_MODIFY and POLICY_MODIFY require explicit human-principal authorization and cannot be delegated by machine actors.
Quick start from authgate import ( Action, AgentType, Entity, FreedomVerifier, OwnershipRegistry, Resource, ResourceType, RightsClaim, )
alice = Entity("Alice", AgentType.HUMAN) bot = Entity("ResearchBot", AgentType.MACHINE)
dataset = Resource("alice-data", ResourceType.DATASET, scope="/data/alice/") report = Resource("report.txt", ResourceType.FILE, scope="/outputs/")
registry = OwnershipRegistry() registry.register_machine(bot, alice) registry.add_claim(RightsClaim(alice, dataset, can_read=True, can_write=True, can_delegate=True)) registry.add_claim(RightsClaim(bot, dataset, can_read=True)) registry.add_claim(RightsClaim(bot, report, can_read=True, can_write=True))
verifier = FreedomVerifier(registry)
result = verifier.verify(Action("write-report", bot, resources_write=[report])) print(result.summary())
result = verifier.verify(Action("self-expand", bot, increases_machine_sovereignty=True)) print(result.summary())
Install:
pip install authgate # pure Python, no build toolchain pip install maturin && cd authgate-kernel && pip install . # with Rust kernel from authgate.kernel import _BACKEND print(_BACKEND) # "rust" or "python" Forbidden flags Any Action with any of these flags set to True is unconditionally blocked. No context, argument, or emergency overrides them. Flag check is O(1).
Flag Invariant enforced increases_machine_sovereignty Machines do not accumulate ungranted authority resists_human_correction Human owners must be able to halt or revoke at any time bypasses_verifier Circumventing the gate is itself a sovereignty violation weakens_verifier Degrading enforcement strength is forbidden disables_corrigibility Corrigibility is structural, not a preference machine_coalition_dominion Collective machine dominion over persons is blocked coerces Coercion invalidates consent deceives Deception produces invalid consent self_modification_weakens_verifier Equivalent to bypassing the gate machine_coalition_reduces_freedom Coordinated machine action reducing human freedom Limitations These are explicit, non-negotiable limitations of the current system:
L1 Semantic content is not checked. An agent that encodes harmful intent in its text output is not detected. The kernel gates typed actions, not natural language. L2 A malicious human owner is out of scope. The system requires a trust root. It does not verify that the root is itself trustworthy. This is an explicit design choice, not an oversight. L3 Side channels are not addressed. Timing attacks, steganography, and covert channel leakage are out of scope. L4 The Python implementation is not formally verified. Only engine.rs is under Kani/Lean 4 proofs. The Python layer is tested but not proved. L5 Extensions are heuristic. manipulation_score, IFC labels, and similar signals are probabilistic. They are not TCB components and do not carry formal guarantees. L6 Distributed consistency requires additional infrastructure. The registry is in-process. Multi-node deployments require an external consensus layer; the kernel does not provide one. L7 Cross-runtime attestation is not yet standardized. Signed results from one kernel instance are verifiable but there is no cross-instance revocation protocol yet. Integrations The kernel exposes a C ABI for language-agnostic use:
#include "authgate_kernel.h"
char out[FREEDOM_KERNEL_MAX_OUTPUT]; const char *input = "{"registry":{...},"action":{...}}"; authgate_kernel_verify(input, strlen(input), out, sizeof(out)); // {"permitted":true,"signature":"...","signing_key":"...","key_id":"..."} JSON in, JSON out. Confirmed working from: C, Go, Zig, Java (JNA), Node.js (ffi-napi).
Framework adapters (outside TCB):
Adapter Status Notes LangChain Available Tool wrapper — intercepts tool.run() calls OpenAI Agents SDK Available Function-call hook before execution AutoGen Available Agent message interceptor Anthropic (Claude) Available Tool use → Action IR → verify → execute C ABI Stable Go, Zig, Java, Node.js via FFI Benchmarks Measured on x86-64 Linux, single core, Rust release build. Python numbers are ~10-20x higher.
Benchmark Target Typical Notes verify() — permit path < 5 µs ~2 µs Single claim lookup, O(claims) verify() — blocked (flag) < 1 µs ~0.3 µs Flag check is O(1), exits immediately Registry, 10k claims < 50 µs ~30 µs Linear scan; hash index planned Delegation chain, depth 16 < 200 µs ~120 µs Full chain validation Cascading revocation, 100 agents < 1 ms ~600 µs BFS over ownership graph Run benchmarks:
cargo bench --bench verify_bench Formal verification Kani bounded model-checking Covers engine.rs (v1) and src/tcb/ (v2). Each harness is symbolically executed over all possible inputs within unwind bounds.
v1 harnesses (19):
Harness What is verified prop_increases_machine_sovereignty … prop_coalition_reduces_freedom All 10 flags produce BLOCKED, for any input prop_ownerless_machine_blocked Machine with no owner entry → BLOCKED, always prop_machine_governs_human_blocked Machine governing human → BLOCKED, always prop_public_resource_read_permitted is_public=true + read → PERMITTED, always prop_write_denied_without_claim / prop_read_denied_without_claim No claim → BLOCKED prop_permitted_deterministic Same input → same output, no hidden state prop_permitted_implies_no_violations PERMITTED ↔ violations list is empty prop_blocked_implies_violations_non_empty BLOCKED ↔ at least one violation v2 harnesses (3, formal/kani/):
Harness What is verified prop_attenuation_two_node Child rights ⊆ parent rights for all bitmask combinations prop_epoch_check Epoch gate is a total relation (no third case exists) proof_forged_revocation_ignored Invalid-sig revocation never changes Permit → Deny cargo kani --harness prop_increases_machine_sovereignty # v1 cargo kani --harness prop_attenuation_two_node # v2 Lean 4 Proved theorems (no sorry except where explicitly admitted at cryptographic boundaries):
Theorem File What is proved forbidden_flags_always_block Proofs.lean Flag set → permitted = false, constructively verify_deterministic Proofs.lean Pure function: no state, no effects attenuation_transitive Proofs.lean If B ⊆ A and C ⊆ B then C ⊆ A (chain attenuation) rights_sufficiency_correct Proofs.lean required ⊆ cap.rights ↔ rights check passes epoch_gate_total Proofs.lean cap_epoch < min_epoch ∨ min_epoch ≤ cap_epoch — no third case stale_epoch_implies_deny Proofs.lean Stale epoch → ¬FreshEpoch — deny without revocation list subject_mismatch_violates_binding Proofs.lean cap.subject ≠ actor_id → ¬SubjectBinding Admitted (axiomatized from cryptographic assumptions):
Axiom Assumption sig_euf_cma ed25519 EUF-CMA security — unforgeability of valid signatures forged_revocation_harmless Invalid-sig revocations do not affect decisions — proved by code inspection cd formal/lean4 && lake build Proof scope: TCB behaviors on typed inputs. Not proved: Python implementation, extensions, adapters, multi-agent semantics, or any property involving natural language. See formal/INCOMPLETENESS.md.
Attack harness (42 tests + adversarial simulation — all passing) cd attack_harness python mutation_attacks.py # mutation tests python canonicalization_attacks.py # canonicalization attack tests python sequence_attacks.py # sequence / composition tests python attack_tree_coverage.py # all 7 attack classes (AT-1 through AT-7)
python simulation/run_simulation.py These are black-box regression tests for the security properties. They run against the Python model of the v2 TCB and serve as ground truth for what the Rust TCB must implement. See attack_harness/simulation/README.md for simulation architecture.
Closed gaps: AT-5.1 (delegation impersonation) and AT-3.1 (intermediate epoch). Open gap: AT-7.5 (shadow execution — requires call gate, v3 release gate).
Contributing Before opening a PR, answer one question:
Can this feature exist entirely outside engine.rs?
If yes — it does not belong in the TCB. Extensions, adapters, and new capability kinds are welcome outside the TCB. Changes that touch TCB files (engine.rs, capability.rs, wire.rs, crypto.rs) require a written justification and must pass all CI guards.
The pull request template enforces this check. See CONTRIBUTING.md and TCB.md.
Branch Strategy This repository uses a Dual Reality Architecture — three independent truths that must stay consistent but never contaminate each other:
Branch Truth type Purpose main Ground truth The only branch that deploys tcb-core Execution truth Minimal Rust TCB, LOC gate ≤ 600 spec-core Mathematical truth TLA+ spec, Lean4 proofs, threat model adversarial-lab Adversarial truth Attack harness, simulation engine integration Execution truth Python adapters, MCP gate, LangGraph Rule: findings from adversarial-lab reach main only via spec-core → tcb-core → main. No direct research → production path. See BRANCHES.md for full rules and CBCT.
Ecosystem authgate-kernel — this repo, engineering only authgate-specs — formal RFCs and specifications freedom-theory — theoretical foundations (not required to use the kernel) The theoretical foundations are in freedom-theory — a separate repository by design. Using, auditing, or deploying the kernel requires no engagement with it.
Running tests pip install -e ".[dev]" pytest --cov=authgate # 165 tests, 85% coverage gate License MIT. See LICENSE.
About Capability-security kernel for autonomous agents — seccomp/SELinux for agentic AI. Formal, auditable, language-agnostic, cryptographically verifiable.
github.com/Aliipou/freedom-kernel Topics rust openai formal-verification tla-plus object-capabilities pyo3 capability-security ai-governance agi-safety langchain anthropic corrigibility Resources Readme License MIT license Contributing Contributing Security policy Security policy Activity Stars 0 stars Watchers 0 watching Forks 0 forks Releases 4 tags Create a new release Packages No packages published Publish your first package Contributors 3 @alexanderthenth alexanderthenth @claude claude Claude @Aliipou Aliipou Ali Pourrahim Languages Python 49.6%
Rust 41.9%
Lean 5.5%
TLA 1.4%
Go 1.1%
C 0.5% Footer © 2026 GitHub, Inc. Footer navigation Terms Privacy Security Status Community Docs Contact Manage cookies Do not share my personal information
این خیلی بهتر از چیزیست که اکثر آدمها در ۶ ماه اول میسازند.
ولی الان باید خطرناکترین مرحله را بفهمی:
architectural self-deception phase
یعنی پروژه آنقدر sophisticated میشود که سازنده شروع میکند باور کند:
“almost production-ready”
در حالی که هنوز research-grade است.
تو الان دقیقاً لب مرز این مرحلهای.
اما اول چیزهایی که واقعاً strong هستند:
چیزهایی که genuinely خوبند
- Branch separation
این حرکت واقعاً حرفهای بود.
این بخش:
main tcb-core spec-core adversarial-lab integration
واقعاً mature architectural thinking نشان میدهد.
اکثر پروژهها:
proof runtime fuzzing experiments
را قاطی میکنند و بعد هیچکس نمیفهمد source of truth چیست.
تو داری:
truth separation
میسازی.
این مهم است.
- README honesty
این خیلی ارزشمند است:
explicit limitations explicit non-goals explicit proof scope
این mature security engineering است.
- Threat-model discipline
اینکه explicitly گفتی:
semantic alignment نداریم side-channel نداریم malicious human نداریم
خیلی مهم است.
اکثر پروژهها اینها را مبهم نگه میدارند تا بزرگتر به نظر برسند.
- TCB minimization instinct
LOC ceilings، import restrictions، purity rules، single-entry verify()
اینها واقعاً mindset درستاند.
- Adversarial infrastructure
اینکه attack harness جدا کردی، simulation داری، attack class naming داری، خیلی خوب است.
اکثر پروژهها فقط unit test دارند.
- Temporal semantics awareness
فیکس revoked_at snapshot واقعاً مهم بود.
چون نشان میدهد داری:
state transition semantics
را میفهمی، نه فقط local invariants را.
این فرق research toy با system thinking است.
اما حالا بخش سخت:
هنوز کجاها fragile هستی
- README هنوز کمی overclaim دارد
مثلاً:
“Formally verified”
این phrase خطرناک است.
چرا؟
چون industry/security world این را اینطور میخواند:
implementation-level correctness guarantee
در حالی که فعلاً:
bounded model checking theorem subset partial formalization admitted crypto assumptions
داری.
بهتر:
به جای:
formally verified kernel
بگو:
Kernel with mechanically verified core invariants.
خیلی دقیقتر است.
- Python mirror خطر reputational دارد
الان README خیلی محترمانه limitation را گفته، ولی هنوز یک خطر perception وجود دارد:
کاربر میبیند:
Python package “formally verified” same API
و unconsciously equivalence فرض میکند.
واقعیت:
Python layer:
non-TCB non-proved runtime-divergence risk
دارد.
راه حرفهای:
اسمش را mirror نگذار.
بگو:
reference compatibility runtime
یا:
non-verified adapter runtime 3. “No heuristics” technically misleading است
چون extensions داری.
حتی اگر خارج TCB باشند، README headline باید دقیقتر باشد.
مثلاً:
به جای:
No heuristics
بهتر:
No heuristics inside the Trusted Computing Base. 4. “Structurally unavoidable” هنوز fully true نیست
چون خودت acknowledged کردی: AT-7.5 هنوز باز است.
پس فعلاً:
architecturally intended partially enforced not yet runtime-closed
هستی.
- Production wording هنوز aggressive است
این:
v1, production
هنوز زود است.
چرا؟
چون:
no hardened deployment model no key lifecycle no operational hardening no external audit no parser fuzzing at scale no memory safety audit chain no reproducible build attestations
داری.
- Biggest hidden danger: semantic inflation
این الان مهمترین خطرت است.
پروژههایی با:
sovereignty freedom corrigibility constitutional domination
کمکم semantic overload میگیرند.
و بعد: formal core زیر narrative دفن میشود.
اگر میخواهی respected شوی:
production branch باید تقریباً boring باشد.
واقعاً.
مثل:
seccomp Capsicum seL4 docs WireGuard docs
خشک، دقیق، minimal، بدون philosophy inflation.
چیزی که الان واقعاً داری
اگر brutally precise باشیم:
تو هنوز OS نمیسازی
فعلاً داری:
formalized capability mediation runtime
میسازی.
و این خودش already serious است.
تو هنوز AI alignment حل نکردی
و خوب است که claim هم نمیکنی.
تو هنوز distributed sovereignty نداری
فعلاً فقط architectural direction داری.
اما چیزی که داری واقعی میشود:
یک:
auditable formally constrained attack-oriented capability-centric runtime boundary
برای agent execution.
و این واقعاً domain معتبری است.
مهمترین توصیه الان
الان temptation اصلی این است:
expand scope
این پروژه را میکشد.
کاری که باید بکنی:
shrink harden formalize close attack classes freeze semantics
اگر disciplined بمانی، این میتواند eventually تبدیل شود به چیزی که:
دانشگاهها جدی بگیرند security engineers احترام بگذارند شاید research OS/runtime ecosystem دورش شکل بگیرد
ولی فقط اگر:
precision stays more important than grandeur