# IHVRK architecture

## 1. Components

| Path | Role | Prompt component |
|---|---|---|
| `crypto/canonical_encoding.py` | integer-only RFC 8785 profile, strict parser, domain-separated SHA-256, action digest | – |
| `crypto/signature_verifier.py` | Ed25519 sign/verify of versioned structures; domain constants | – |
| `crypto/challenge_generator.py` | 256-bit CSPRNG nonce, challenge body | 1 Challenge generator |
| `crypto/hsm_bridge.py` | `KeyStore` interface; `SoftwareTestKeyStore`; `HardwareKeyStore` (not implemented, never falls back) | 5 HSM bridge |
| `identity/verifier_registry.py` | enrollment-authority-signed verifier records; agent/verifier separation; roles | 2 Human authentication gateway |
| `identity/credential_status.py` | signed, versioned, monotone revocation list with freshness | 2 |
| `attestation/attestation_verifier.py` | software-measured attestation appraisal; hardware → INDETERMINATE | 2/3 |
| `policy/authorization_policy.py` | deterministic decision over facts (Python) | 3 Policy oracle |
| `solver/ihvrk_solver.py` | Z3 encoding, proofs, runtime cross-check | 3 |
| `nonce/epoch_registry.py` | SQLite: requests, challenges, permits, epochs; all CAS transitions | 4 Nonce & replay registry |
| `service/state_machine.py` | 14 states, legal transitions | – |
| `service/verification_service.py` | propose → challenge → approval → policy → permit; cancel, revoke, expire, reconcile | 2/3 |
| `service/permit_issuer.py` | signed single-use permits; `ExecutionGate` (enforcement boundary) | – |
| `service/break_glass.py` | two-operator emergency path | 6 Break-glass |
| `ledger/*` | append-only hash-chained ledger, signed checkpoints, witness log, verifier, export | – |
| `runtime/talos_gatekeeper.sh` | cgroup v2 freeze while pending | runtime |
| `runtime/ebpf/*.bpf.c` | LSM deny hooks; tracepoint telemetry | runtime |
| `formal/IHVRK.tla` | protocol model | – |

Dependency graph (arrows = imports):

```
canonical_encoding <- signature_verifier <- {hsm_bridge, verifier_registry, credential_status, attestation_verifier,
                                              checkpoint, ledger_verifier, permit_issuer, verification_service, break_glass}
authorization_policy <- ihvrk_solver <- verification_service
state_machine <- epoch_registry <- {verification_service, permit_issuer}
append_only_ledger <- {checkpoint, verification_service, permit_issuer}
verification_service <- break_glass
(no ihvrk module imports any other CAIN module; evidence/verify_ihvrk_evidence.py imports nothing from ihvrk)
```

## 2. State machine

```
CREATED -> CHALLENGE_ISSUED -> AWAITING_HUMAN -> HUMAN_AUTHENTICATED -> APPROVAL_VERIFIED -> POLICY_AUTHORIZED
        -> EXECUTION_PERMIT_ISSUED -> EXECUTING -> COMPLETED
every state before EXECUTING  -> DENIED | EXPIRED | REVOKED | CANCELLED | INDETERMINATE
EXECUTING                     -> COMPLETED | INDETERMINATE      (an operation that may have run is never "denied")
terminal states have no exits; no state may be skipped or revisited
```

What each state means. Authentication, consent, authorization and execution are separate states:

| State | Means | Entered when |
|---|---|---|
| HUMAN_AUTHENTICATED | an enrolled, active, independent verifier at the required AAL signed *something* for this challenge, and the nonce is consumed | stage 1 of `submit_approval` |
| APPROVAL_VERIFIED | that signed object approves exactly this request (digest, resource, tenant, agent, scope, epoch, policy version, challenge id, validity window) | stage 2 |
| POLICY_AUTHORIZED | Python policy and Z3 both return AUTHORIZE | stage 3 |
| EXECUTION_PERMIT_ISSUED | permit signed, registered, ledger written | stage 4 |
| EXECUTING | the gate consumed the permit (final check) | `ExecutionGate.execute` |

## 3. Sequence

```
Agent            Service                        Registry(SQLite)        Verifier device        Gate                Ledger
  | propose(action, cap)                             |                         |                    |                    |
  |---------------->| digest = SHA256(dom||JCS(a))   |                         |                    |                    |
  |                 |-- create_request ------------->| epoch++ (txn)           |                    |                    |
  |                 |-- REQUEST_CREATED -------------------------------------------------------------------------------->|
  |                 | verify capability; sign challenge                         |                    |                    |
  |                 |-- register_challenge --------->| (txn)                   |                    |                    |
  |<-- challenge ---|-- CHALLENGE_ISSUED --------------------------------------------------------------------------------->|
  |  (relayed to the verifier out of band; the agent never holds verifier keys)  |                    |                    |
  |                 |<---------------- signed approval (nonce, digest, ...) ---|                    |                    |
  |                 | stage1 authn; consume_challenge (txn: nonce ISSUED->CONSUMED + request state CAS)                       |
  |                 | stage2 binding; stage3 policy == Z3; ledger records                                                    |
  |                 | stage4 sign permit; register_permit (txn)                                                               |
  |<-- permit ------|                                                                                                        |
  | execute(permit, action) ------------------------------------------------------------>| verify sig, re-digest, |
  |                 |                                |<-- consume_permit (txn) ---------| binding, expiry        |
  |                 |                                |    permit ISSUED->CONSUMED +      |                        |
  |                 |                                |    request ->EXECUTING            |-- PERMIT_CONSUMED ---->|
  |                 |                                |                                   |-- EXECUTION_STARTED -->|
  |                 |                                |                                   | run operation          |
  |                 |                                |<-- ->COMPLETED / INDETERMINATE ---|-- outcome ------------>|
```

## 4. Where the final check is (time of check to time of use)

The last authorization decision is `EpochRegistry.consume_permit`: a single SQLite `BEGIN IMMEDIATE` transaction
that moves the permit `ISSUED → CONSUMED` and the request `EXECUTION_PERMIT_ISSUED → EXECUTING`, both conditional
on their current values.

* A revoke, cancel or expire that commits before it: the CAS fails and the operation never starts (tests:
  revoke-after-permit, D5).
* One that arrives after it: too late. The window until the operation starts is two ledger appends (each one fsync)
  in the same thread.
* Guarantee: **at most one start** per permit. Exactly-once *effect* is not guaranteed. A crash between consume and
  the outcome record leaves `EXECUTING`; `reconcile()` turns it into `INDETERMINATE` and never retries (I10 test).
* This is only an execution boundary if the protected operation is reachable **only** through
  `ExecutionGate.execute`. That is a deployment property (THREAT_MODEL G5).

## 5. Failure-state matrix

| Failure | During propose | During approval | At the gate | Result |
|---|---|---|---|---|
| clock unavailable / untrusted | INDETERMINATE, no request | INDETERMINATE (authn fails, time facts untrusted) | REJECTED | blocked |
| clock uncertainty straddles a deadline | – | INDETERMINATE | REJECTED (`PERMIT_EXPIRED_OR_UNCERTAIN`) | blocked |
| registry error / locked | INDETERMINATE | INDETERMINATE | REJECTED (`REGISTRY_UNAVAILABLE`) | blocked |
| ledger unwritable / full | request → INDETERMINATE | → INDETERMINATE before permit | consumed but not run → INDETERMINATE | blocked |
| keystore unavailable | → INDETERMINATE | → INDETERMINATE (no permit) | – | blocked |
| status list missing / stale | – | INDETERMINATE (verifier status) | – | blocked |
| attestation missing / hardware-only | – | INDETERMINATE | – | blocked |
| enforcement probe RELEASED / error | – | DENY / INDETERMINATE | – | blocked |
| Z3 timeout / unknown / exception / disagreement | – | INDETERMINATE | – | blocked |
| malformed input (floats, dup keys, oversize, extra fields) | DENY | DENY | REJECTED | blocked |
| operation raises | – | – | INDETERMINATE, permit consumed | not retried |
| process crash mid-flow | – | reconcile → INDETERMINATE | reconcile → INDETERMINATE | not resumed |
| gatekeeper killed | – | – | cgroup stays frozen | blocked |

Every failure leaves the request blocked or explicitly unresolved. Nothing in the table can yield AUTHORIZE.

## 6. Six-component security matrix

| | 1 Challenge generator | 2 Human authn & attestation gateway | 3 Policy & consensus oracle | 4 Nonce & replay registry | 5 HSM bridge | 6 Break-glass |
|---|---|---|---|---|---|---|
| Purpose | fresh, signed, action-bound challenge | decide whether an approval came from an enrolled, active, independent human verifier at the required AAL | combine facts into one decision | single-use for nonces and permits; epochs | custody of service keys | emergency approval without the ordinary verifier |
| Trusted inputs | OS CSPRNG, service clock | enrollment-authority key, status list, attestation key | facts from 1, 2, 4 | – | – | operator enrollments (role `break-glass-operator`) |
| Untrusted inputs | proposal | approval object, transport | request-derived values | request ids, nonces | – | grants |
| Threats addressed | replay, cross-request reuse | forged / agent / revoked / low-AAL approvals | solver failure, logic error | replay, double spend, races | key misuse | stuck emergency vs universal bypass |
| Mechanism | 256-bit nonce; Ed25519 signature; domain `IHVRK/v1/challenge` | Ed25519; signed enrollments; monotone versioned status list | Python rule + Z3 model, must agree | SQLite WAL, `synchronous=FULL`, CAS in `BEGIN IMMEDIATE` | interface; software keys in memory | 2 distinct operators, signed grants bound to digest, ≤ 900 s, notifier |
| Key ownership | service (challenge key) | verifiers (devices); enrollment authority | – | – | service | operators |
| Failure mode → behaviour | keystore down → INDETERMINATE | stale/unknown → INDETERMINATE; invalid → DENY | timeout/unknown/disagree → INDETERMINATE | storage error → INDETERMINATE | unavailable → no permit | any requirement unmet → nothing changes |
| Recovery | reissue via new proposal | new status list; re-enroll with new kid | none needed (stateless) | `reconcile()`, `prune()` | rotate (new kid, old revoked, kids never reused) | revoke via status list |
| Privacy | none | no raw biometrics stored; `authn` method + AAL only | – | – | – | reason text stored |
| Perf (p50, see evidence/benchmark.json) | nonce < 1 µs | verify ≈ 0.3 ms | Python ≈ 5 µs; Z3 + cross-check ≈ 8 ms | consume (contended) ≈ 7.5 ms | – | – |
| Tests | integration, D9 | A1–A12, B1–B4 | formal suite, H1–H9 | D1–D11, I9, I10 | signatures unit | E4–E6 |
| Status | IMPLEMENTED_AND_TESTED | IMPLEMENTED_AND_TESTED (software attestation); hardware NOT_IMPLEMENTED | IMPLEMENTED_AND_TESTED; FORMALLY_VERIFIED_WITH_STATED_ASSUMPTIONS | IMPLEMENTED_AND_TESTED (single node) | software: IMPLEMENTED_AND_TESTED (SOFTWARE_TEST); hardware: NOT_IMPLEMENTED | IMPLEMENTED_AND_TESTED |

Fail-secure vs fail-safe: for the protected action every failure is fail-secure (deny). Break-glass is the one
fail-safe path, and it is a separate, narrower policy, not a failure mode of the normal one.

Combining components without weakening the threat model: 1, 3 and 4 run in one process and share one trust domain
(the service host). 2's trust root (the enrollment authority) and 6's operators must stay outside that host. They are
the only components whose compromise is not implied by a service-host compromise. No component runs its own consensus.
A multi-node deployment needs the registry (4) behind a linearizable store, not six independent quorums.