diff --git a/silo/MOTIVATION.adoc b/silo/MOTIVATION.adoc new file mode 100755 index 0000000..95ed0f1 --- /dev/null +++ b/silo/MOTIVATION.adoc @@ -0,0 +1,98 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Silo: motivation +:toc: macro +:icons: font + +toc::[] + +== The user we are designing for + +Not the diligent operator. The *non-expert, low-effort* user — the one who will +paste a live API key into a shell, a config, a chat window, or a public repo, and +who will *not* rotate it, *not* read the warning, and *not* perform any reversal +step we offer. This user is where the real losses happen, so this user is the +design centre. (Not "zero-knowledge" — that term is reserved for ZK proofs; here +we mean low expertise and low diligence, nothing cryptographic.) + +The governing principle is *ALARP* (As Low As Reasonably Practicable), not +"solved". We are not promising a secret cannot be compromised. We are reducing the +_consequence_ of the compromises this user will inevitably cause, to as low as is +practicable *given that they will do nothing*. A control that requires user effort +has, for this user, an effectiveness of zero. + +== The problems, stated honestly + +. *Distinctive prefixes leak value.* `AKIA…`, `ghp_…`, `sk_live_…` tell a thief + which stolen blob is an AWS root key and which is a throwaway automation token. + The prefix that helps defenders (secret scanning) also helps the attacker + *triage*. (The AWS account id is even decodable from the access-key id alone.) + +. *Secrets in the clear survive everywhere.* Shell history, clipboard history + (`cbdhsvc` on Windows; pinned items persist to disk), `/proc//cmdline`, + logs, backups. None of these are reachable by a type system. + +. *"Secure deletion" is a lie on modern hardware.* The estate's own RMO + (`januskey`, `valence-shell`) uses a 3-pass overwrite; on an SSD the FTL remaps + writes and the original blocks survive. `valence-shell` documents this and has a + matching open Coq gap (`obliterate_overwrites_all_blocks`). The theorem does not + hold on the actual disk. + +. *The lazy user will not reverse.* Any scheme whose safety depends on the user + running an "undo" or "shred" step has already failed for this user. + +== The reframe: turn each problem into the basis of the design + +[cols="1,2",options="header"] +|=== +| Problem | Turned into + +| Prefixes leak *value* | A *uniform envelope* — every secret looks the same (a + UUID-shaped handle). Denies the attacker triage. +| A public transform is only obfuscation | The uniformity must be *keyed* + (Format-Preserving Encryption) — or, better, carry *no secret at all*. +| FPE still holds the secret in the blob | *Tokenisation*: the handle is a + *reference*, not ciphertext. It contains zero secret material, so a leaked + handle is *inert*. +| Uniformity blinds our own leak detection | Register the *envelope shape* as the + scanned pattern. We detect "a silo secret leaked" (actionable) without + disclosing "an AWS root key leaked" (value). Net gain, not a trade. +| RMO overwrite is unsound on SSD | *Crypto-shred by handle*: destroy the one + 32-byte vault key. Irrecoverability reduces to "the key is gone and AES holds" — + provable — instead of defeating an SSD controller. +| The lazy user will not reverse | *Inert by default.* Nothing to reverse, because + a leaked handle grants nothing. Maximal ALARP for zero user effort. +|=== + +== The one-line thesis + +*Make every secret look the same, and make the sameness contain nothing.* A +UUID-shaped handle that references a vault entry is simultaneously: the uniform +disguise the user asked for, the runtime realisation of the secret type +`S ℓ A` (you hold the handle, you cannot open it without the vault — the modality +with no `reflect`), and a *sound* RMO (destroy the referenced key and every copy +of the handle everywhere dies at once). + +== What this explicitly does NOT solve + +Stated up front so no reader over-claims: + +* It does *not* protect against code running *as the user* on the same machine at + the moment of use — that code can ask the vault and get the plaintext. No + user-space design closes this; it is the OS threat model. +* It does *not* clean the clipboard or shell history. Those need the separate + mechanisms (clipboard opt-out formats, `HistorySaveStyle SaveNothing`, keyring). +* It does *not* remove the need to *rotate* a secret already leaked in plaintext. + A handle protects secrets *minted through the silo*; it cannot retroactively + un-leak a raw key that was pasted before siloing. + +The design is a consequence-reducer for the careless-by-default case, not a +confidentiality proof. That is precisely what ALARP asks for. + +== Position in the pipeline + +Incubator (`idea -> alpha`) entry. Theory upstream in +`epistemic-types/docs/secret-types.adoc`; runtimes it composes with are +`januskey` / `valence-shell` (RMR/RMO) and the platform key stores +(`keyctl` on Linux, DPAPI/TPM on Windows). Graduates to its own typed repo when +the handle/vault core and the HMAC envelope have a conformance suite. diff --git a/silo/docs/DESIGN.adoc b/silo/docs/DESIGN.adoc new file mode 100755 index 0000000..088224f --- /dev/null +++ b/silo/docs/DESIGN.adoc @@ -0,0 +1,145 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Silo: design +:toc: macro +:toclevels: 3 +:icons: font +:source-highlighter: rouge +:stem: latexmath + +[abstract] +The mechanical design of the silo: the handle format, the vault, the HMAC +envelope, the leak-detection rule, and crypto-shred RMO. Motivation and the ALARP +framing are in `../MOTIVATION.adoc`; the type theory is in +`epistemic-types/docs/secret-types.adoc`. + +toc::[] + +== Two constructions, ranked + +Both make secrets look uniform; they differ in what the envelope contains. + +=== A. Tokenisation (handle) — preferred + +The visible artefact is a *handle* that contains no secret material: + +---- +SILO-- +---- + +* `uuid` — a random 128-bit identifier. Carries no information about the secret, + its provider, or its value. This is the "all of them look the same" property: + an AWS root key and a throwaway token are indistinguishable handles. +* `hmac` — a truncated HMAC over the uuid, keyed by a silo *instance* key. Not a + CRC: an HMAC also *authenticates that this silo minted the handle*, so a thief + cannot forge silo-shaped tokens and a finder cannot validate one offline. + +The real secret lives in the *vault*, indexed by `uuid`. The handle is what the +lazy user pastes into env vars, configs, `.bashrc`, chat, git. *A leaked handle is +inert* — it references a vault the leak-recipient cannot reach. + +This is the runtime realisation of `S ℓ A` (`epistemic-types/docs/secret-types.adoc`): +you can pass the handle around freely (`map` under the modality) but cannot open it +(`no reflect`). The clearance `ℓ` is stored beside the vault entry and checked at +resolve time. + +=== B. Format-preserving envelope (FPE) — fallback, stateless + +When a vault lookup is impossible (fully offline, no daemon), fall back to +*keyed* FPE (NIST FF1 / FF3-1): the secret is *encrypted* into a uniform shape. +Weaker than A — the secret is still in the blob, so a leaked envelope plus a leaked +key is a compromise — but stateless. Use only where tokenisation cannot run. The +user correctly anticipated the cost: the envelope grows ("now the thing is longer"), +because a 40-char AWS secret does not fit in 128 bits. + +[IMPORTANT] +==== +A public transform is *not* construction B. Without a key, permute+checksum is +obfuscation: the algorithm is in this repo, so anyone reverses it and reads the +`AKIA` prefix. FPE's indistinguishability holds *only* because of the key. This is +the single most important correctness point in the whole design. +==== + +== The vault + +[cols="1,3",options="header"] +|=== +| Platform | Backing store + +| Linux | kernel keyring (`keyctl padd` + `keyctl timeout`) for the live key — + non-swappable kernel memory, real TTL; `age`/`sops` for the at-rest entry. +| Windows | DPAPI (CurrentUser + entropy) or, for hardware binding, a CNG/TPM + key-encryption-key wrapping the data key. `SecretManagement`/`SecretStore` as + the managed option, with `-PasswordTimeout` for auto-lock. +| systemd unit consumers | `systemd-creds` (TPM2-bound, `host+tpm2`), delivered + as a `$CREDENTIALS_DIRECTORY` file, never in env or argv. +|=== + +Each vault entry is `{ uuid, ciphertext | keyring-id, clearance ℓ, provider-tag +(sealed), created, ttl }`. The `provider-tag` (which real service this is) is +stored *inside* the sealed entry, never in the handle — so the value-triage the +prefix used to give the attacker is available only after a successful, +clearance-checked resolve. + +== Leak detection without value disclosure + +Registering a single Gitleaks / secret-scanning rule for the envelope shape +`SILO-[0-9a-f-]{36}-[0-9a-f]{16}` restores the safety net the uniformity would +otherwise remove: + +* a leaked handle is *detected* — "a silo secret appeared in a commit / log"; +* its *value is not disclosed* — the finder cannot tell provider or clearance. + +This is strictly better than the prefix status quo: we keep leak alerting and +remove the attacker's triage gift. The rule is ours to publish; it does not depend +on a partner-pattern registration. + +== Crypto-shred RMO — making obliteration sound + +RMO on a handle does *not* overwrite disk blocks. It destroys the *key* the vault +entry needs: + +. `keyctl revoke` / `keyctl unlink` the live DEK (or `keyctl timeout` for the + self-destruct TTL); on Windows, delete the DPAPI/TPM-wrapped DEK. +. delete the vault row. +. emit the `januskey`-style `ObliterationProof` (commitment `H(uuid ‖ nonce ‖ t)`), + which records *that* a specific handle was obliterated, without storing its value. + +Now irrecoverability reduces to *"the 32-byte key is gone and AES holds"* — a claim +that is provable and hardware-independent — rather than the unprovable "we defeated +the SSD FTL". This is the construction that closes `valence-shell`'s open +`obliterate_overwrites_all_blocks` gap *by changing the mechanism*, not by trying +to prove the overwrite. Every copy of the handle, everywhere it was pasted, dies +the instant the key does — the self-destruct the low-effort user never has to trigger. + +== `Echo`-graded partial release (the open middle) + +Between RMR (`r=0`, reversible) and RMO (`r=∞`, obliterate) sits graded +declassification: resolve a handle to a *lossy view* at grade `r` — e.g. "reveal +that a card number ends `4242` but nothing more", a leak budget of a few bits. The +grade composes by the proved tropical algebra; a resolve that would exceed the +entry's declared floor is refused by the checker. This is where the silo does +something no existing secret manager does, and it is the natural alpha-stage +experiment. + +== Threat model (restated, sharp) + +[cols="1,2",options="header"] +|=== +| Adversary | Outcome + +| Finds a handle in a public repo / log / chat | *Nothing.* Inert reference. +| Runs secret scanning | Detects the leak; learns no value. (Our own rule.) +| Steals the vault file, not the key | Ciphertext only; useless (A) / needs the FPE key (B). +| Runs *as the user, on the box, at use time* | *Wins.* Can ask the vault. Out of scope — OS threat model. +| Wants provable erasure (GDPR Art. 17) | Crypto-shred + proof. Sound on SSD. +|=== + +== Build order (idea → alpha) + +. Handle format + HMAC envelope + the Gitleaks rule (pure, testable, no vault). +. `keyctl`-backed vault on Debian: mint → inert handle → resolve → crypto-shred, + demonstrated end to end. +. DPAPI/TPM vault on Windows, same interface. +. `Echo`-graded partial resolve, gated by the `tropecheck` verdict. +. Conformance suite → graduate to a typed repo.