From 88d0f50d599cab01db97b0898e6393639230a3d9 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 27 Sep 2026 04:53:16 +0000 Subject: [PATCH] docs(security): integrate secret-types research note Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- CHANGELOG.adoc | 6 ++ README.adoc | 4 + docs/README.adoc | 5 ++ docs/secret-types.adoc | 177 +++++++++++++++++++++++++++++++++++++++++ 4 files changed, 192 insertions(+) create mode 100644 docs/secret-types.adoc diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index ff12341..c9f7970 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -34,6 +34,12 @@ the changelog records what is actually proved, not what is aspired to. A fixity declaration only; no definition changed. * New documentation: `docs/applications/rapidnj-q-criterion.adoc`, plus README, documentation-index, proof-status and machine-readable state updates. +* Added `docs/secret-types.adoc` as an in-repository research note for the + security-polarity direction (issue #29). It corrects the preserved draft's + scope against the current APIs, makes no security-implementation claim, and + sets out staged proof and runtime obligations. README and documentation + index link to the note; no Agda API changed and the retired `AUDIT.adoc` was + not restored. [[fixed--2026-09-07]] ==== Fixed — 2026-09-07 diff --git a/README.adoc b/README.adoc index da789a5..c7b1a36 100644 --- a/README.adoc +++ b/README.adoc @@ -202,6 +202,9 @@ This is a prototype, not a complete epistemic logic. The following are **intenti transport that would lift the integer certificate to rational input * Cross-iteration reuse of a skip bound, and the row-insertion update that maintains the scan invariants (`Applications.RapidNJSkip.WeakeningObligation`) +* Confidentiality labels, secret types, declassification, and noninterference; + see link:docs/secret-types.adoc[the security-polarity research note] for the + current scope and proposed route == Build @@ -223,6 +226,7 @@ agda --no-libraries -i src src/EpistemicTypes/All.agda * link:docs/continuity-foundations.adoc[Continuity foundations] — store coherence, retained information, bounds, and next obligations * link:docs/proof-transport.adoc[Proof transport] — semantic verification across boundaries * link:docs/applications/rapidnj-q-criterion.adoc[Applications: the RapidNJ Q-criterion] — the bound, the skip warrant, the exact-arithmetic obligation +* link:docs/secret-types.adoc[Secret types] — a scoped research direction and staged route to a future security model == License diff --git a/docs/README.adoc b/docs/README.adoc index e8a5f34..2da73d5 100644 --- a/docs/README.adoc +++ b/docs/README.adoc @@ -34,6 +34,11 @@ authority. downgrades a sender's `Proof` to a receiver's `Receipt`, how `verify` upgrades `Data` to `Proof` only with the receiver's own checker plus evidence, and the public / designated / receipt distinctions. + +| `docs/secret-types.adoc` +| A scoped research direction for security-polarity / secret types: what the + current epistemic, warrant, and Echo interfaces do and do not establish, plus + a staged route to an in-repository security model. |=== == Continuity foundations diff --git a/docs/secret-types.adoc b/docs/secret-types.adoc new file mode 100644 index 0000000..cf0a152 --- /dev/null +++ b/docs/secret-types.adoc @@ -0,0 +1,177 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += Secret Types: a security-polarity research direction +:toc: macro +:toclevels: 3 +:icons: font +:revdate: 2026-09-27 + +[abstract] +This note keeps the secret-types direction inside `epistemic-types` and sets out +a cautious route from the current epistemic interfaces to a possible formal +information-flow model. It is a design note, not an implemented security API: +there is no `Secret` type, security-label lattice, declassification mechanism, or +noninterference result in this repository today. + +toc::[] + +== Decision and scope + +The land-or-retire decision recorded in issue #29 is to **land this research +direction in this repository**, rather than create a new repository. The +preserved note is reworked here against the current source and proof boundaries. +It is a research connection to the existing epistemic core, not evidence that a +security model is already implemented or proved. + +This file is therefore a roadmap and an explicitly unformalized research note. +It does not change the public Agda API, promise a particular design, or make a +security guarantee about a program or runtime. The retired `AUDIT.adoc` is not +part of this decision and is not restored. + +== What the repository currently provides + +The current code offers concepts that may be useful when designing a security +model, but their present meanings are narrower: + +* `Modality` in `src/EpistemicTypes/Base.agda` is an indexed family `E κ A` + with a mapping operation. It does not assign confidentiality labels or + restrict who can observe a value. +* `Access.Preorder` and `AccessibleModality.increase` in + `src/EpistemicTypes/Access.agda` let an instance interpret an order and + transport `E κ A` along it. The example reading is epistemic access from a + less-informed to a more-informed standpoint. The generic preorder does not + specify a security policy or a clearance lattice. +* `BeliefModality` omits a `reflect` field. This says that the generic record + interface does not provide a factivity operation. It does **not** hide a + concrete representation, prevent pattern matching, stop a client from + exposing data through another operation, or establish confidentiality. +* `FactiveModality.reflect : E κ A -> A` is an epistemic factivity interface. + It is not a declassification policy. Conversely, omitting `reflect` is not, + by itself, an information-flow proof. +* `Warrant` separates evidence tokens from an explicit soundness map, and + `ProofTransport` proves claims relative to a caller-supplied meaning and + checker. Neither module models secrecy, identity, cryptography, or a physical + access-control system. +* `Echo` certificates relate a residue to an observation under a supplied + contract. `BoundedEcho` bounds a supplied residue measure. Its grade is not + inherently a number of leaked bits, entropy, or a declassification budget; + such a meaning would need its own measure and theorem. See + link:continuity-foundations.adoc[continuity foundations]. + +At this revision, the proof gate recursively checks the Agda modules under +`src/EpistemicTypes/` (17 source modules) using `--safe --without-K`, with no +standard-library dependency. These proofs establish only the propositions +encoded in those modules. Safe type-checking is not a general security +certification, and it does not supply missing security semantics. + +== A possible security interpretation + +A future model could reuse the idea of indexing a value by a standpoint, but it +must state a security policy rather than silently identify it with the existing +epistemic preorder. One possible convention is: + +* labels form an ordered set with `ℓ ⊑ ℓ'` meaning that `ℓ'` is at least as + restrictive as `ℓ`; +* `⊥` is public and higher labels require greater clearance; +* a value classified at `ℓ` can be read at clearance `c` only when there is an + explicit witness of `ℓ ⊑ c`; +* raising a label from `ℓ` to `ℓ'` when `ℓ ⊑ ℓ'` is safe classification (taint + moves upward); combining values uses a join so the result is no less + restrictive than either input. + +Under that convention, schematic signatures (not compile-ready Agda) might +resemble: + +[source,text] +---- +Secret : Label -> Set -> Set +raise : ℓ ⊑ ℓ' -> Secret ℓ A -> Secret ℓ' A +combine : Secret ℓ A -> Secret m B -> Secret (ℓ ⊔ m) (A × B) +readAt : ℓ ⊑ clearance -> Secret ℓ A -> A +---- + +This is only a sketch. It leaves open how values are represented, how the +constructor is hidden, what a clearance witness means, how a runtime enforces +it, and which observations an attacker can make. In particular, a proof of +`ℓ ⊑ clearance` is meaningful only relative to a correctly specified label +model and trusted construction of its witnesses. The order direction is a +design choice that must be documented consistently in code and examples. + +Declassification would need a separate, explicit policy boundary. It should +not be modelled as an unrestricted `reflect` or as an ordinary safe label raise: +a release rule needs to say who may release what, under which evidence or +capability, and what property is preserved by that release. The initial model +could instead omit declassification entirely. + +== What is not claimed + +This note does not claim that the following exist or have been proved here: + +* a `SecurityLattice`, `Secret`, `classify`, `declassify`, or clearance API; +* a confidentiality or information-flow policy, or a proof that forbidden + flows cannot occur; +* noninterference, quantitative leakage, secure erasure, zeroization, or + resistance to timing, cache, storage, network, or other side channels; +* linear or single-use handling of secret values; +* a connection from `EchoBridge.Grade` to bits, entropy, or a security budget; +* a transfer of proof from another repository's algebra, type checker, or + runtime into this Agda development. + +The preserved draft proposed links to neighbouring formal and runtime projects. +Those may be useful inputs, but they are not dependencies of this repository and +their results are not reproduced by its current CI. Any future integration must +name exact source revisions, state the compatibility claim, and add a +reproducible check before the project relies on it. + +== Route forward + +The route below is staged so that prose, a type-level discipline, and a runtime +security claim are not conflated. Later stages depend on earlier decisions; this +list is a proposal, not a commitment to implement every stage. + +. **Specify the model and threat boundary.** Choose a concrete use case, label + order and its direction, principals and clearances, observable outputs, + attacker capabilities, permitted flows, and whether declassification is in + scope. State the security property to prove (for example, a clearly defined + noninterference relation) before choosing type constructors. +. **Add the smallest in-repository Agda interface.** If the specification + warrants it, introduce a `SecurityLattice` and an abstract secret wrapper in + a focused module (a possible location is + `src/EpistemicTypes/Secret.agda`). Decide explicitly whether the existing + `Preorder` is reusable or whether security needs a distinct interface. Define + only the operations justified by the model: safe label raising, combination + at a join, and reading under a proved clearance. Keep declassification out + until its policy is specified. +. **Add positive and negative proof controls.** Prove the permitted operations + under `--safe --without-K --no-libraries`; add regression fixtures showing + that a lower-clearance read, an implicit downgrade, and an unauthorized + release are rejected. The recursive proof gate must include every new module + and the expected-rejection gate must distinguish a real policy failure from + a broken import or tool invocation. +. **Prove the semantic security property.** Give the labels and program + observations an explicit semantics. Prove a policy-appropriate theorem such + as noninterference, with any permitted declassification reflected in the + theorem's assumptions and conclusion. Type-level encapsulation alone is not + that theorem. +. **Treat runtime guarantees as a separate integration.** Only after the model + and theorem are clear should a concrete runtime, linearity discipline, + resource/leakage measure, or external grade algebra be connected. State and + check the representation and runtime correspondence; keep erasure and + side-channel claims outside the formal result unless they are separately + modelled and verified. + +The next actionable step is the first one: agree the use case, order convention, +and threat boundary. That specification determines whether the useful first +implementation is an access-controlled wrapper, a lattice-indexed information- +flow API, or a different abstraction altogether. + +== Related documentation + +* link:../README.adoc[Project overview] — current interfaces and deliberately + unformalized commitments. +* link:what-epistemic-is.adoc[What epistemic-types is] — the project's + mathematical scope and contribution boundary. +* link:continuity-foundations.adoc[Continuity foundations] — certified + residues and the distinct resource-bound axis. +* link:proof-transport.adoc[Proof transport] — verification relative to an + explicit meaning, with its own trust boundary.