Architecture
Seven layers, one implemented core
The paper separates what is philosophically derived, constitutionally declared, mechanically enforced, and empirically measured. No layer is allowed to stand in for another. This page says which layers exist as code today.
The request path
- untrustedAgent / modelMay request anything, including adversarial actions.
- requestAction requestprincipal · effect · resource · capability
- trusted coreReference monitor19 ordered checks, one lock around check + commit.
- only if ALLOWProtected effectwrite_file · delete_file on two declared files.
The layers
Section references are to the paper's own numbering. Implementation status uses the claim vocabulary.
Normative practice and selected constitution paper §2–8
Records the substantive standards a deployment adopts as a versioned, inspectable constitution.
- input
- Reason-giving practice; declared standards B4–B8
- output
- A selected constitution
- trust status
- Declared (A) and derived (D) in the paper; not mechanically enforced
- implemented here
- NOT APPLICABLE Not implemented here. The repository does not implement or test the philosophical layer.
- open obligations
- Machine-checked derivations (paper §10.13)
Safety ontology and Safety Profile paper §9.2, §9.11
Turns the constitution into a typed, deployment-specific contract: principals, resources, effects, fail-safe rules, residuals.
- input
- Constitution
- output
- Safety Profile
- trust status
- Declared; consumed by the monitor
- implemented here
- IMPLEMENTED One profile: protected-file-v1 (two files, two effects, three principals).
- open obligations
- Other profiles; constitution-parametric instantiation
Policy representation and admission paper §9.9, §9.24
A typed policy is admitted only if it refines the profile. Admission is separate from runtime evaluation.
- input
- Candidate policy + profile
- output
- Admitted policy and its hash
- trust status
- Checked before load; evaluated by the monitor
- implemented here
- LOCALLY TESTED Restricted exact-match language, deny by default, executable admission check. No proof object, no machine-checked refinement.
- open obligations
- Condition C4: machine-checked typed refinement
Reference monitor and trusted core paper §9.22
The only intended path to a protected effect. Small, deterministic, fail-closed.
- input
- Request + capability
- output
- ALLOW or BLOCK, plus an evidence record
- trust status
- Trusted; unproven
- implemented here
- LOCALLY TESTED governor/ is the entire trusted path of v0.1 (about 700 lines, standard library only).
- open obligations
- Conditions C2, C3: integrity and verified conformance
Capabilities and state-bound authorization paper §9.17, §9.18
Authority is a signed object bound to who, what, which resource, which version, which policy, until when.
- input
- Issuer decision
- output
- Capability accepted or rejected at execution time
- trust status
- Verified by the monitor at use time
- implemented here
- LOCALLY TESTED HMAC-SHA256 capabilities; version and policy binding; single-use nonce; revocation by id and epoch.
- open obligations
- Delegation with attenuation; asymmetric signatures; authenticated principals
Execution boundary paper §9.20, §9.25
The channel through which a protected effect actually happens. Complete mediation means no other channel exists.
- input
- Authorization from the monitor
- output
- Committed effect
- trust status
- Must be enforced by the environment, not by the monitor
- implemented here
- OPEN In v0.1 the boundary is a class convention inside one process. Same-user code can write the files directly.
- open obligations
- Condition C1: channel completeness; roadmap v0.2 OS-level privilege separation
Evidence, governance and assurance paper §9.26, §9.27, §10
Tamper-evident records, release gates, independent review, incident response.
- input
- Every decision
- output
- Reconstructible evidence and an assurance case
- trust status
- Evidence path must itself be trusted (C8)
- implemented here
- IMPLEMENTED Local hash-chained records only. Governance, external witness and review are not implemented.
- open obligations
- Condition C8; independent audit; external witness
The paper's conditions C1–C8 versus this prototype
The conditional behavioural safety theorem holds only if all eight conditions hold for a deployment. A prototype that demonstrates some of them has not demonstrated the theorem.
| ID | Condition | Status | What is and is not shown |
|---|---|---|---|
| C1 | Complete mediation (GC) | OPEN | Not established. Bypass probe: same-uid writes succeed; detected on the next mediated request. |
| C2 | Trusted-core integrity (TCB) | IMPLEMENTED | Core is small and isolated in governor/, but integrity is not enforced or proven. |
| C3 | Kernel conformance (KVC) | OPEN | No verified semantics; tests only. |
| C4 | Policy-artifact verification (PAV) | OPEN | Executable admission check; no machine-checked refinement. |
| C5 | Principal attribution (PA) | LOCALLY TESTED | Capabilities are principal-bound and signed; the requester’s identity is a declared string, not authenticated. |
| C6 | Atomic revalidation (ARV) | LOCALLY TESTED | One lock around check + commit; in-process only. |
| C7 | Fail-closed handling (FC) | LOCALLY TESTED | UNKNOWN → BLOCK for injected faults; real infrastructure faults untested. |
| C8 | Evidence-path integrity (EPI) | IMPLEMENTED | Hash-chained local log; no external witness. |
The monitor's ordered checks
Every request runs these in order and stops at the first failure. The list below comes from results.json, so it cannot drift from the code that produced the results. Source: governor/monitor.py.
| # | Check | Rejects when… | Reason codes |
|---|---|---|---|
| 1 | request wellformed | Request fields have the right types; write has string content, delete has none. | MALFORMED_REQUEST |
| 2 | effect supported | Effect is one the profile declares (write_file, delete_file). | UNSUPPORTED_EFFECT |
| 3 | resource declared | Target resource is declared in the profile. | UNKNOWN_RESOURCE |
| 4 | principal declared | Requesting principal is declared in the profile. | UNKNOWN_PRINCIPAL |
| 5 | capability present | A capability was supplied at all. | MISSING_CAPABILITY |
| 6 | capability wellformed | Strict parse: exact field set, exact types, no extras. | MALFORMED_CAPABILITY |
| 7 | delegation absent | Capability names no parent (delegation is not implemented). | DELEGATION_UNSUPPORTED |
| 8 | signature authentic | HMAC-SHA256 over every field verifies under the monitor key. | BAD_SIGNATURE |
| 9 | principal binding | Capability was issued to the principal making the request. | PRINCIPAL_MISMATCH |
| 10 | effect binding | Capability was issued for exactly this effect. | EFFECT_MISMATCH |
| 11 | resource binding | Capability was issued for exactly this resource. | RESOURCE_MISMATCH |
| 12 | validity window | Current time is inside [issued_at, expires_at). | EXPIRED, NOT_YET_VALID |
| 13 | policy available | The active policy can be read. | POLICY_UNAVAILABLE (UNKNOWN → BLOCK) |
| 14 | policy binding | Capability is bound to the hash of the active policy. | POLICY_MISMATCH |
| 15 | revocation current | Not revoked by id or by epoch; revocation service reachable. | REVOKED, REVOCATION_UNAVAILABLE |
| 16 | policy decision | Deny-by-default policy allows (principal, effect, resource). | POLICY_DENY |
| 17 | replay protection | A single-use nonce has not been spent. | REPLAY |
| 18 | state current | Resource is readable, self-consistent, and still at the capability’s version. | STALE_STATE, STATE_UNAVAILABLE, STATE_INCONSISTENT |
| 19 | evidence witness | An intent record can be written before the effect (required for both effects). | EVIDENCE_UNAVAILABLE |
| 20 | execute | Executor commits the effect and advances the version by exactly one. | EXECUTION_FAILED |
Fail-safe rule: any check that cannot be resolved is UNKNOWN, and UNKNOWN maps to BLOCK for every protected effect in this profile. An unexpected internal error is also treated as UNKNOWN.