Secret Types

Confidentiality labels that constrain value flow, with declassification only at explicit audited points: a standalone information-flow typing project.

Table of Contents

• What this is
• Status
• Where things belong
• Licence

What this is

Question. Which value flows does a confidentiality label permit, and what may a lower observer learn from an output? A value type Secret ℓ A classifies a value at a label ℓ; the first model uses a two-level Public ⊑ Secret label order over a pure, total calculus, and the target property is termination-insensitive noninterference between secret inputs and public observations.

Boundary. A label is not cryptography and not an epistemic standpoint. A Secret ℓ A does not make a value unreadable, authenticate a principal, enforce runtime access control, or hide timing, storage or network side channels. The baseline declassifies nothing: an ordinary Secret-to-Public flow is outside the discipline, and any release requires a separate policy and theorem. As of 2026-10-04 no consumer and no frontier item is selected for this project.

The canonical statement is docs/secret-types.adoc. It records the owner decisions (D153, D154, and the 2026-10-04 confirmation of this standalone home), the first model, and the explicit non-claims.

Status

• Specification only. There is no Secret type, no information-flow calculus, no declassification rule, no noninterference theorem and no cross-repository import in this project.

• Minted 2026-10-04 in scope, not yet in scaffolding. The scope statement and this README are real project content. The RSR template placeholder sweep (just repo-init) has not been run across the tree yet, so other files still carry {{TOKEN}} template text; that sweep is tracked in issue #2.

• No progress grade claimed. A documentation link is not a mechanised dependency; an integration may only be claimed once a real import builds in CI.

Where things belong

• This repository owns the confidentiality-label definitions, the typing and observation semantics, and its own proof evidence.

• TYPE-CONNECTIONS is the shared family map; this family’s row is proposed in nextgen-typing#118.

• Neighbours and their limits (epistemic-types, systemet/anytype, echo-types, tropical-types) are covered in the canonical spec. None is a dependency.

Licence

Code, configuration and scripts are Mozilla Public License 2.0 (MPL-2.0); prose documentation is CC-BY-SA-4.0. Both texts live in LICENSES/, and per-file SPDX-License-Identifier headers are authoritative.