Repository navigation
Specify an in-repository security model for secret types #32
Description
Follow-up to #29 and docs/secret-types.adoc. The direction stays inside epistemic-types; do not spin up a new repository or add a Secret API before the semantics are specified.
First deliverable: the model and threat boundary
Agree and record:
- a concrete use case, attacker capabilities, and observable outputs;
- the label-order convention (including whether public is bottom and higher labels are more restrictive), clearances, and permitted flows;
- whether declassification is in scope and, if so, the authority/policy required;
- the security property to prove and the semantics of observations (for example, a specific noninterference statement);
- whether
Access.Preordercan be safely reused or a separateSecurityLatticeinterface is needed.
Acceptance criteria
- Update
docs/secret-types.adocwith the chosen definitions and non-claims. - Do not describe
BeliefModality's missingreflectorEchoBridge.Gradeas a confidentiality or leakage guarantee. - Keep any Agda module, rejecting fixtures, semantic theorem, and runtime integration as separately reviewed follow-on work after this specification is agreed.
The current note's staged route is the plan; this issue tracks its first actionable step.
Activity
docs(security): specify secret-type model boundary (#32) (#33)
hyperpolymath commentedon Sep 30, 2026
RULING D154 (2026-09-30T14:15Z) · scope: repo · basis: owner (direct answer, selector)
Reuse an existing lattice (two-point then general), prove noninterference, declassification only at explicit audited points
surface: hyperpolymath/standards#787 (comment)
The open question in this issue is answered by the ruling above; future agents should act on it rather than re-ask.
docs: record the epistemic-types transition review and correct its cr…
docs: cross-reference review of the Secret Types transition (refs #32) (
hyperpolymath commentedon Oct 5, 2026
Closing — delivered here; the model's acceptance now lives in
hyperpolymath/secret-typesThis issue asked for the first semantic boundary here, not for an Agda module.
That is delivered, and what remains is tracked where it belongs.
Delivered against the acceptance criteria
docs/secret-types.adoc: twolabels
Public ⊑ Secret(public is bottom; higher is more restrictive),dependency join, clearances as
ℓ ⊑ cwitnesses, a low-clearance observer,prohibited
Secret → Publicflows (implicit flow included), thetermination-insensitive noninterference target, and an explicit non-claims
list. The note also states why
Access.Preorderis not the securityinterface and why a distinct security-label definition is required.
interfaces:
BeliefModality's missingreflectandEchoBridge.Gradeareexplicit non-claims, and
--safe --without-Kis not presented as a securitycertification.
Secrettype, IFC calculus,declassification rule, theorem, rejection fixtures, or runtime integration —
all of it stays separately reviewed follow-on work.
(two-point first, then general), prove noninterference, declassify only at
explicit audited points. The 2026-10-04 owner confirmation places the
specification and all formal work in
hyperpolymath/secret-types(ADR0004-standalone-repo-and-scope.adoc, PR feat(read-consistency): version-monotone re-sync liveness as AccessibleModality instance #4d1122d8; adopted text = thisrepository's PR docs(security): specify secret-type model boundary (#32) #33 revision, blob
583017cfd5fab189ca17128d01c7eddb494d8476).Not claimed by this close: the standalone specification is not described as
accepted. Its item-by-item acceptance is its own "Review checklist before
implementation" (
secret-typesdocs/secret-types.adoc), with the mint andhand-off tracked in
secret-types#2. No transfer of this issue occurred or isrequired, and none should be attempted: this history and the boundary note
stay in
epistemic-types.What remains here is only a guard — keep the pointer accurate and keep
Secret/IFC claims out of this repository. Successor issue: #N.
For future readers: model changes, lattice choices, the noninterference theorem,
declassification policy, and any
Secretmodule belong inhyperpolymath/secret-types. Do not re-open this issue to re-litigate themodel.
#29remains closed. Evidence record: the 2026-10-05 transition reviewin this repository.