diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 611b5a8..9257eac 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -2,13 +2,13 @@ # CODEOWNERS - Define code review assignments # See: https://docs.github.com/en/repositories/managing-your-repositorys-settings-and-features/customizing-your-repository/about-code-owners # -# Replace {{OWNER}} with your GitHub username or team +# Repository owner: hyperpolymath # Default owners for everything -* @{{OWNER}} +* @hyperpolymath # Security-sensitive files require explicit review -SECURITY.md @{{OWNER}} -.github/workflows/ @{{OWNER}} -Trustfile.a2ml @{{OWNER}} -.machine_readable/ @{{OWNER}} +SECURITY.md @hyperpolymath +.github/workflows/ @hyperpolymath +Trustfile.a2ml @hyperpolymath +.machine_readable/ @hyperpolymath diff --git a/.machine_readable/root-allow.txt b/.machine_readable/root-allow.txt index 196dbcf..f59dbf5 100644 --- a/.machine_readable/root-allow.txt +++ b/.machine_readable/root-allow.txt @@ -38,6 +38,10 @@ CLAUDE.md # generated arrival pack; the generator, pre-commit a Justfile # thin; delegates phases to build/just/*.just coordination.k9.ncl # repo-local session binding (template-mandated) +# ─── Project-specific root entries ─────────────────────────────────────────── +PROOF-STATUS.adoc # project theorem evidence and fragment limits, linked from README.adoc +secret-types.agda-lib # Agda discovers library descriptors at the project root + # ─── Conventional dotfiles (tool-required at root) ─────────────────────────── .editorconfig .envrc diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc new file mode 100644 index 0000000..bbb1da4 --- /dev/null +++ b/PROOF-STATUS.adoc @@ -0,0 +1,51 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += secret-types — Proof Status +:revdate: 2026-10-12 + +Statuses: PROVEN / TESTED / ASSUMED / DESIGNED / OPEN. Every PROVEN line +names its module; all modules are `--safe --without-K --no-libraries`, +checked with `--double-check`, no postulates. + +== Fragment (stated before the claims) + +One public and one secret variable; naturals; expressions `lit`, `var`, +`plus`; commands `skip`, assignment, sequence, `ifz`, `while`; fuel-indexed +big-step semantics (`nothing` when fuel runs out). Volpano–Smith typing with +a program-counter label over the two-point lattice. Not in the fragment: +n variables / arbitrary lattices, declassification, procedures, concurrency, +timing. Termination is the one channel the theorem names as open. + +== Claims + +[cols="1,3,1",options="header"] +|=== +| ID | Claim | Status +| N-1 | *TINI*: `pc ⊢ c → s ≈ s' → exec n c s ≡ just t → exec n' c s' ≡ just t' → t ≈ t'`, fuels independent | PROVEN (`Noninterference.tini`) +| N-2 | Public expressions read the same in low-equivalent stores | PROVEN (`eval-low`) +| N-3 | Confinement: under a secret program counter the public variable is unchanged, loops included | PROVEN (`confine`) +| N-4 | The typing side-condition is load-bearing: an explicit flow and an implicit flow are each refused (`L != H` at the `⊑` obligation) *and* each actually leaks from low-equivalent stores | TESTED (`tests/reject/ExplicitFlow`, `ImplicitFlow`; `Witness.explicit-leaks`, `implicit-leaks`) +| N-5 | Termination-insensitivity is real, not vacuous: a well-typed program spins on one secret and stops on another; TINI says nothing about that pair, by design | TESTED (`Witness.secret-loop-spins/stops`) +| N-6 | Laws census: the proof uses only the two-point order (`⊔-L₁`, `⊔-L₂`, `H ⊔ y = H`) and decidable zero-testing of naturals; no lattice law beyond that | ASSUMED by inspection (no parametric lattice to certify against yet) +|=== + +== Separation from siblings (criterion 2 of the family bar) + +* Noninterference is a property of *two* runs. Echo grades, tropical grades + and occupancy grades are accumulations over *one* run; none of them can + state N-1. That is the separation, and it is why this is a family and not + a view. The converse connection — that a well-typed program's low + observer has an Echo fibre that does not separate secret inputs — is a + CONJECTURE, recorded in the README, not claimed here. +* A label is not an epistemic standpoint (README). The Kripke frame built + for choreographic-types indexes knowledge by *views*; a label indexes + *permission to flow*. Nothing here imports epistemic-types, deliberately. + +== Open + +* Termination-sensitive noninterference (close the named channel): needs a + stronger typing rule for `while` on secret guards. Pre-registered: + the falsifier is `secret-loop` above, which TSNI must refuse. +* Arbitrary lattices (parametric in a `Lattice` record, with the census in + N-6 then certifiable the way resource-algebra's is). +* Declassification; multiple variables. +* CI (`proofs.yml`): DESIGNED until first green run on the 2.6.4.3 pin. diff --git a/README.adoc b/README.adoc index bae32a7..fcc6b56 100644 --- a/README.adoc +++ b/README.adoc @@ -10,7 +10,7 @@ image:https://img.shields.io/badge/Code-MPL--2.0-blue.svg?logo=mozilla[Code lice image:https://img.shields.io/badge/Docs-CC--BY--SA--4.0-blue.svg?logo=creativecommons[Docs licence: CC-BY-SA-4.0,link="https://creativecommons.org/licenses/by-sa/4.0/"] // ── Status ────────────────────────────────────────────────────────────────── -image:https://img.shields.io/badge/Stage-specification--only-orange[Specification only: no code, no proofs] +image:https://img.shields.io/badge/Proof-core_theorem_proven-brightgreen[Core theorem proven,link="PROOF-STATUS.adoc"] image:https://img.shields.io/badge/RSR-Rhodium_Standard-9C27B0[Rhodium Standard Repository,link="https://github.com/hyperpolymath/rhodium-standard-repositories"] Confidentiality labels that constrain value flow, with declassification only at @@ -38,17 +38,18 @@ 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 - link:https://github.com/hyperpolymath/secret-types/issues/2[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. +Core theorem PROVEN (2026-10-12): termination-insensitive noninterference +for the two-point lattice, `src/SecretTypes/Noninterference.agda` +(`tini`), with the explicit and implicit flows refused by the type system +and shown to leak by computation (`tests/reject/`, `Witness.agda`). The +fragment is one public and one secret variable with a `while` language and +fuel semantics; see link:PROOF-STATUS.adoc[]. Termination is the channel +the theorem leaves open, by name. + +Conjecture (not claimed): for a well-typed program, the public observer's +Echo fibre over its outputs does not separate secret inputs — the Echo +reading of noninterference, and the first candidate connection +Secret → Echo for `nextgen-typing/docs/TYPE-CONNECTIONS.adoc`. == Where things belong diff --git a/docs/MAINTAINERS.adoc b/docs/MAINTAINERS.adoc index 458fc55..3f1fad4 100644 --- a/docs/MAINTAINERS.adoc +++ b/docs/MAINTAINERS.adoc @@ -12,9 +12,9 @@ earlier duplicates at `.github/MAINTAINERS` and `docs/attribution/MAINTAINERS.ad |=== | Name | Role | Contact -| {{AUTHOR}} +| Jonathan D.A. Jewell | Lead Maintainer -| https://github.com/{{OWNER}}[@{{OWNER}}] +| https://github.com/hyperpolymath[@hyperpolymath] |=== == Responsibilities diff --git a/docs/README-section.adoc b/docs/README-section.adoc new file mode 100644 index 0000000..c25851e --- /dev/null +++ b/docs/README-section.adoc @@ -0,0 +1,15 @@ +// Splice into README.adoc, replacing "== Status" (specification only). +== Status + +Core theorem PROVEN (2026-10-12): termination-insensitive noninterference +for the two-point lattice, `src/SecretTypes/Noninterference.agda` +(`tini`), with the explicit and implicit flows refused by the type system +and shown to leak by computation (`tests/reject/`, `Witness.agda`). The +fragment is one public and one secret variable with a `while` language and +fuel semantics; see link:PROOF-STATUS.adoc[]. Termination is the channel +the theorem leaves open, by name. + +Conjecture (not claimed): for a well-typed program, the public observer's +Echo fibre over its outputs does not separate secret inputs — the Echo +reading of noninterference, and the first candidate connection +Secret → Echo for `nextgen-typing/docs/TYPE-CONNECTIONS.adoc`. diff --git a/docs/architecture/REPOSITORY-MAP.adoc b/docs/architecture/REPOSITORY-MAP.adoc index 8c77eea..d7848e2 100644 --- a/docs/architecture/REPOSITORY-MAP.adoc +++ b/docs/architecture/REPOSITORY-MAP.adoc @@ -113,6 +113,10 @@ predecessors did. | yes | REUSE licence texts, dual-licence model (code MPL-2.0 / docs CC-BY-SA-4.0) +| `PROOF-STATUS.adoc` +| yes +| project theorem evidence and fragment limits, linked from README.adoc + | `README.adoc` | yes | - @@ -161,6 +165,10 @@ predecessors did. | yes | repo helper scripts +| `secret-types.agda-lib` +| yes +| Agda discovers library descriptors at the project root + | `session/` | yes | dispatch.sh, custom-checks.k9.ncl, local-hooks.sh diff --git a/scripts/check.sh b/scripts/check.sh new file mode 100755 index 0000000..2d2ab69 --- /dev/null +++ b/scripts/check.sh @@ -0,0 +1,36 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Core proofs plus expected rejections. Pattern: residual-evidence-types. +set -euo pipefail +cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." +export LC_ALL="${LC_ALL:-C.UTF-8}" +prover="${AGDA:-agda}" +"$prover" --version +flags=(--safe --without-K --no-libraries --ignore-interfaces --double-check -i src) +"$prover" "${flags[@]}" src/SecretTypes/All.agda +mkdir -p _build/check-logs +shopt -s nullglob +rejects=(tests/reject/*.agda) +shopt -u nullglob +if (( ${#rejects[@]} == 0 )); then + echo 'ERROR: no expected-rejection modules found under tests/reject' >&2 + exit 1 +fi +for file in "${rejects[@]}"; do + name="$(basename -- "$file" .agda)" + log="_build/check-logs/$name.log" + if "$prover" "${flags[@]}" -i tests/reject "$file" >"$log" 2>&1; then + cat "$log" + echo "ERROR: invalid proof accepted: $name" >&2 + exit 1 + fi + if ! grep -Eq "/$name\.agda:[0-9]+,[0-9]+" "$log" || + ! grep -q 'when checking that' "$log" || + grep -Eq 'Not in scope|Failed to find|Unsolved|Parse error' "$log"; then + cat "$log" + echo "ERROR: unexpected failure while checking $name" >&2 + exit 1 + fi + echo "PASS: rejected $name at its invalid declaration" +done +echo "PASS: core proofs and all ${#rejects[@]} expected rejections" diff --git a/secret-types.agda-lib b/secret-types.agda-lib new file mode 100644 index 0000000..bef4bdc --- /dev/null +++ b/secret-types.agda-lib @@ -0,0 +1,3 @@ +name: secret-types +include: src +flags: --safe --without-K diff --git a/src/SecretTypes/All.agda b/src/SecretTypes/All.agda new file mode 100644 index 0000000..97676d1 --- /dev/null +++ b/src/SecretTypes/All.agda @@ -0,0 +1,9 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +module SecretTypes.All where +import SecretTypes.Prelude +import SecretTypes.Lattice +import SecretTypes.Lang +import SecretTypes.Typing +import SecretTypes.Noninterference +import SecretTypes.Witness diff --git a/src/SecretTypes/Lang.agda b/src/SecretTypes/Lang.agda new file mode 100644 index 0000000..a67d3b3 --- /dev/null +++ b/src/SecretTypes/Lang.agda @@ -0,0 +1,86 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- A small while-language with one public and one secret variable, and a +-- fuel-indexed big-step semantics. Fuel is what makes "termination- +-- insensitive" a real qualifier: a loop that does not finish within the +-- fuel returns `nothing`, and the theorem is stated only for runs that +-- return `just`. +module SecretTypes.Lang where + +open import SecretTypes.Prelude +open import SecretTypes.Lattice + +data Var : Set where + lo hi : Var + +-- Classify the public variable as L and the secret variable as H. +label : Var → Label +label lo = L +label hi = H + +record Store : Set where + constructor ⟨_,_⟩ + field + low : Nat + high : Nat +open Store public + +data Expr : Set where + lit : Nat → Expr + var : Var → Expr + plus : Expr → Expr → Expr + +infixr 5 _﹔_ +data Cmd : Set where + skip : Cmd + _≔_ : Var → Expr → Cmd + _﹔_ : Cmd → Cmd → Cmd + ifz : Expr → Cmd → Cmd → Cmd -- if e = 0 then c₁ else c₂ + while : Expr → Cmd → Cmd -- while e = 0 do c + +-- Evaluate an expression using the store's current variable values. +eval : Store → Expr → Nat +eval s (lit n) = n +eval s (var lo) = low s +eval s (var hi) = high s +eval s (plus a b) = eval s a + eval s b + +-- Return a store with the selected variable replaced, preserving the other. +update : Var → Nat → Store → Store +update lo n ⟨ l , h ⟩ = ⟨ n , h ⟩ +update hi n ⟨ l , h ⟩ = ⟨ l , n ⟩ + +-- exec fuel c s: `just t` if c runs to completion within fuel, else `nothing`. +-- Fuel bounds recursive loop evaluation: each while consumes one unit, +-- even when its guard is non-zero. At zero fuel, while returns `nothing`. +-- Other commands consume no fuel; sequence reuses it for both commands, +-- and a loop's body and continuation each receive the remaining fuel. +exec : Nat → Cmd → Store → Maybe Store +-- Run the first branch for guard value zero, otherwise the second, using +-- the supplied fuel unchanged; return the selected branch's result. +execIf : Nat → Nat → Cmd → Cmd → Store → Maybe Store -- guard value, branches +-- Continue a loop after its fuel decrement, using the supplied guard value. +-- Non-zero returns `just s`; zero runs the body then repeats the loop with +-- the same remaining fuel, re-evaluating e in the updated store. Return +-- `nothing` if either the body or the repeated loop exhausts its fuel. +execWhile : Nat → Nat → Expr → Cmd → Store → Maybe Store -- remaining fuel, guard value + +exec fuel skip s = just s +exec fuel (x ≔ e) s = just (update x (eval s e) s) +exec fuel (c₁ ﹔ c₂) s = bind (exec fuel c₁ s) (exec fuel c₂) +exec fuel (ifz e c₁ c₂) s = execIf fuel (eval s e) c₁ c₂ s +exec zero (while e c) s = nothing +exec (suc fuel) (while e c) s = execWhile fuel (eval s e) e c s + +execIf fuel zero c₁ c₂ s = exec fuel c₁ s +execIf fuel (suc _) c₁ c₂ s = exec fuel c₂ s + +execWhile fuel zero e c s = bind (exec fuel c s) (exec fuel (while e c)) +execWhile fuel (suc _) e c s = just s + +-- Low-equivalence: the public observer sees the same thing. +infix 4 _≈_ +_≈_ : Store → Store → Set +s ≈ s' = low s ≡ low s' diff --git a/src/SecretTypes/Lang.agdai b/src/SecretTypes/Lang.agdai new file mode 100644 index 0000000..bae9579 Binary files /dev/null and b/src/SecretTypes/Lang.agdai differ diff --git a/src/SecretTypes/Lattice.agda b/src/SecretTypes/Lattice.agda new file mode 100644 index 0000000..a804953 --- /dev/null +++ b/src/SecretTypes/Lattice.agda @@ -0,0 +1,33 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- The two-point lattice Public ⊑ Secret. A label is a flow constraint, not +-- an epistemic standpoint (README, "A label is not an epistemic standpoint"). +module SecretTypes.Lattice where + +open import SecretTypes.Prelude + +data Label : Set where + L H : Label -- L = Public, H = Secret + +infix 4 _⊑_ +data _⊑_ : Label → Label → Set where + L⊑L : L ⊑ L + L⊑H : L ⊑ H + H⊑H : H ⊑ H + +infixl 6 _⊔_ +-- Combine flow labels: the result is secret if either input is secret. +_⊔_ : Label → Label → Label +L ⊔ y = y +H ⊔ y = H + +-- A public join guarantees that its left input is public. +⊔-L₁ : ∀ {x y} → x ⊔ y ≡ L → x ≡ L +⊔-L₁ {L} _ = refl +⊔-L₁ {H} () + +-- A public join guarantees that its right input is public. +⊔-L₂ : ∀ {x y} → x ⊔ y ≡ L → y ≡ L +⊔-L₂ {L} e = e +⊔-L₂ {H} () diff --git a/src/SecretTypes/Lattice.agdai b/src/SecretTypes/Lattice.agdai new file mode 100644 index 0000000..8b6fa17 Binary files /dev/null and b/src/SecretTypes/Lattice.agdai differ diff --git a/src/SecretTypes/Noninterference.agda b/src/SecretTypes/Noninterference.agda new file mode 100644 index 0000000..47ea2b4 --- /dev/null +++ b/src/SecretTypes/Noninterference.agda @@ -0,0 +1,117 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- Termination-insensitive noninterference for the two-point lattice. +-- +-- tini : pc ⊢ c → s ≈ s' → exec n c s ≡ just t → exec n' c s' ≡ just t' → t ≈ t' +-- +-- Two runs of a well-typed command from low-equivalent stores, each of +-- which finishes, end low-equivalent. Fuel is universally quantified and +-- may differ between the runs; a run that does not finish is simply not a +-- case (that is the "termination-insensitive"). Structure: +-- eval-low a public expression reads the same in low-equivalent stores +-- confine a command typed under a secret pc leaves the public variable alone +-- tini by induction on fuel and the typing derivation +module SecretTypes.Noninterference where + +open import SecretTypes.Prelude +open import SecretTypes.Lattice +open import SecretTypes.Lang +open import SecretTypes.Typing + +---------------------------------------------------------------------- +-- A public expression has equal values in stores that agree on lo. +eval-low : ∀ e {s s'} → lab e ≡ L → s ≈ s' → eval s e ≡ eval s' e +eval-low (lit n) _ _ = refl +eval-low (var lo) _ eq = eq +eval-low (var hi) () +eval-low (plus a b) p eq = cong₂ _+_ (eval-low a (⊔-L₁ p) eq) (eval-low b (⊔-L₂ p) eq) + +---------------------------------------------------------------------- +-- Confinement: under a secret program counter the public variable is unchanged. +-- Requires evidence that execution finishes with the supplied fuel. +confine : ∀ {c} fuel {s t} → H ⊢ c → exec fuel c s ≡ just t → low t ≡ low s +-- Confinement for a finishing conditional with supplied guard value n; +-- both branches must be typed under a secret program counter. +confineIf : ∀ {c₁ c₂} fuel n {s t} → H ⊢ c₁ → H ⊢ c₂ → execIf fuel n c₁ c₂ s ≡ just t → low t ≡ low s +-- Confinement for a finishing loop continuation with remaining fuel and +-- supplied guard value n, when its body is typed under a secret counter. +confineW : ∀ {e c} fuel n {s t} → H ⊢ c → execWhile fuel n e c s ≡ just t → low t ≡ low s + +confine fuel skip e = cong low (sym (just-inj e)) +confine fuel (assign {x = lo} ()) +confine fuel (assign {x = hi} _) e = cong low (sym (just-inj e)) +confine fuel (seq t₁ t₂) e with bind-just _ _ e +... | s₁ , (e₁ , e₂) = trans (confine fuel t₂ e₂) (confine fuel t₁ e₁) +confine fuel (ifz {e = g} t₁ t₂) e = confineIf fuel (eval _ g) t₁ t₂ e +confine zero (while t) () +confine (suc fuel) (while {e = g} t) e = confineW fuel (eval _ g) t e + +confineIf fuel zero t₁ t₂ e = confine fuel t₁ e +confineIf fuel (suc _) t₁ t₂ e = confine fuel t₂ e + +confineW fuel zero t e with bind-just _ _ e +... | s₁ , (e₁ , e₂) = trans (confine fuel (while t) e₂) (confine fuel t e₁) +confineW fuel (suc _) t e = cong low (sym (just-inj e)) + +---------------------------------------------------------------------- +-- Finishing runs of a well-typed command preserve low-equivalence. +-- The fuel bounds may differ; runs returning nothing are not covered. +tini : ∀ {pc c} fuel fuel' {s s' t t'} → pc ⊢ c → s ≈ s' + → exec fuel c s ≡ just t → exec fuel' c s' ≡ just t' → t ≈ t' +-- Preserve low-equivalence across two finishing conditional evaluations. +-- ℓ is the program-counter label joined with the guard's label; when it +-- is secret, the runs may take different branches. Fuel bounds may differ. +tiniIf : ∀ {pc e c₁ c₂} fuel fuel' {s s' t t'} ℓ → pc ⊔ lab e ≡ ℓ + → pc ⊔ lab e ⊢ c₁ → pc ⊔ lab e ⊢ c₂ → s ≈ s' + → execIf fuel (eval s e) c₁ c₂ s ≡ just t → execIf fuel' (eval s' e) c₁ c₂ s' ≡ just t' → t ≈ t' +-- Preserve low-equivalence across two finishing loop continuations. +-- ℓ is the program-counter label joined with the guard's label; the fuel +-- bounds are those remaining after each loop's decrement and may differ. +tiniW : ∀ {pc e c} fuel fuel' {s s' t t'} ℓ → pc ⊔ lab e ≡ ℓ + → pc ⊔ lab e ⊢ c → s ≈ s' + → execWhile fuel (eval s e) e c s ≡ just t → execWhile fuel' (eval s' e) e c s' ≡ just t' → t ≈ t' + +tini fuel fuel' skip eq e e' = trans (cong low (sym (just-inj e))) (trans eq (cong low (just-inj e'))) +tini fuel fuel' (assign {pc} {lo} {g} ok) eq e e' = + trans (cong low (sym (just-inj e))) + (trans (eval-low g (⊔-L₂ (low-pc ok)) eq) + (cong low (just-inj e'))) + where + -- Any label allowed to flow to the public variable must itself be public. + low-pc : ∀ {x} → x ⊑ L → x ≡ L + low-pc L⊑L = refl +tini fuel fuel' (assign {x = hi} _) eq e e' = + trans (cong low (sym (just-inj e))) (trans eq (cong low (just-inj e'))) +tini fuel fuel' (seq t₁ t₂) eq e e' with bind-just _ _ e | bind-just _ _ e' +... | s₁ , (e₁ , e₂) | s₁' , (e₁' , e₂') = tini fuel fuel' t₂ (tini fuel fuel' t₁ eq e₁ e₁') e₂ e₂' +tini fuel fuel' (ifz {pc} {g} t₁ t₂) eq e e' = tiniIf {pc} {g} fuel fuel' (pc ⊔ lab g) refl t₁ t₂ eq e e' +tini zero fuel' (while t) eq () e' +tini (suc fuel) zero (while t) eq e () +tini (suc fuel) (suc fuel') (while {pc} {g} t) eq e e' = tiniW {pc} {g} fuel fuel' (pc ⊔ lab g) refl t eq e e' + +-- Public guard: both runs read the same guard, take the same branch. +tiniIf {pc} {g} {c₁} {c₂} fuel fuel' {s} {s'} {t} {t'} L p t₁ t₂ eq e e' = + go (eval s g) (eval-low g (⊔-L₂ p) eq) e e' + where + -- Equal guard values select the same branch in the two finishing runs. + go : ∀ n {m} → n ≡ m → execIf fuel n c₁ c₂ s ≡ just t → execIf fuel' m c₁ c₂ s' ≡ just t' → t ≈ t' + go zero refl e e' = tini fuel fuel' t₁ eq e e' + go (suc n) refl e e' = tini fuel fuel' t₂ eq e e' +-- Secret guard: whichever branches ran, neither touched the public variable. +tiniIf {pc} {g} {c₁} {c₂} fuel fuel' {s} {s'} H p t₁ t₂ eq e e' = + trans (confineIf fuel (eval s g) (subst (_⊢ c₁) p t₁) (subst (_⊢ c₂) p t₂) e) + (trans eq (sym (confineIf fuel' (eval s' g) (subst (_⊢ c₁) p t₁) (subst (_⊢ c₂) p t₂) e'))) + +tiniW {pc} {g} {c} fuel fuel' {s} {s'} {t} {t'} L p tc eq e e' = + go (eval s g) (eval-low g (⊔-L₂ p) eq) e e' + where + -- Equal guard values make both finishing runs continue the loop or stop. + go : ∀ n {m} → n ≡ m → execWhile fuel n g c s ≡ just t → execWhile fuel' m g c s' ≡ just t' → t ≈ t' + go zero refl e e' with bind-just _ _ e | bind-just _ _ e' + ... | s₁ , (e₁ , e₂) | s₁' , (e₁' , e₂') = tini fuel fuel' (while tc) (tini fuel fuel' tc eq e₁ e₁') e₂ e₂' + go (suc n) refl e e' = trans (cong low (sym (just-inj e))) (trans eq (cong low (just-inj e'))) +tiniW {pc} {g} {c} fuel fuel' {s} {s'} H p tc eq e e' = + trans (confineW fuel (eval s g) (subst (_⊢ c) p tc) e) + (trans eq (sym (confineW fuel' (eval s' g) (subst (_⊢ c) p tc) e'))) diff --git a/src/SecretTypes/Noninterference.agdai b/src/SecretTypes/Noninterference.agdai new file mode 100644 index 0000000..4369594 Binary files /dev/null and b/src/SecretTypes/Noninterference.agdai differ diff --git a/src/SecretTypes/Prelude.agda b/src/SecretTypes/Prelude.agda new file mode 100644 index 0000000..6e1834f --- /dev/null +++ b/src/SecretTypes/Prelude.agda @@ -0,0 +1,60 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- Minimal prelude over Agda builtins only (no stdlib): negation, equality +-- lemmas, Maybe with monadic bind, and pairs. Used by the TINI proof. +module SecretTypes.Prelude where + +open import Agda.Builtin.Nat public using (Nat; zero; suc; _+_) +open import Agda.Builtin.Equality public using (_≡_; refl) +open import Agda.Builtin.Sigma public using (Σ; _,_; fst; snd) + +data ⊥ : Set where +-- Negation is evidence that a proposition would imply a contradiction. +¬_ : Set → Set +¬ A = A → ⊥ +infix 4 _≢_ +-- Express inequality by ruling out evidence of equality. +_≢_ : {A : Set} → A → A → Set +a ≢ b = ¬ (a ≡ b) + +-- Reverse an equality proof. +sym : {A : Set} {a b : A} → a ≡ b → b ≡ a +sym refl = refl +-- Chain equality proofs through their shared intermediate value. +trans : {A : Set} {a b c : A} → a ≡ b → b ≡ c → a ≡ c +trans refl q = q +-- Carry equality through application of a function. +cong : {A B : Set} (f : A → B) {a b : A} → a ≡ b → f a ≡ f b +cong f refl = refl +-- Carry equalities in both arguments through a binary function. +cong₂ : {A B C : Set} (f : A → B → C) {a b : A} {c d : B} → a ≡ b → c ≡ d → f a c ≡ f b d +cong₂ f refl refl = refl +-- Transport evidence for the predicate P along an equality of its indices. +subst : {A : Set} (P : A → Set) {a b : A} → a ≡ b → P a → P b +subst P refl p = p + +data Maybe (A : Set) : Set where + nothing : Maybe A + just : A → Maybe A + +-- Recover equality of the values inside equal just results. +just-inj : {A : Set} {a b : A} → just a ≡ just b → a ≡ b +just-inj refl = refl + +-- Pass a present value to f and return its result; propagate nothing +-- without applying f when the input is absent. +bind : {A : Set} → Maybe A → (A → Maybe A) → Maybe A +bind nothing f = nothing +bind (just a) f = f a + +infixr 2 _×_ +-- Pair evidence for two propositions without a dependency between them. +_×_ : Set → Set → Set +P × Q = Σ P (λ _ → Q) + +-- From a successful bind, recover the intermediate value and proofs that +-- both the input and the continuation produced the required just results. +bind-just : {A : Set} (m : Maybe A) (f : A → Maybe A) {t : A} + → bind m f ≡ just t → Σ A (λ a → (m ≡ just a) × (f a ≡ just t)) +bind-just (just a) f e = a , (refl , e) diff --git a/src/SecretTypes/Prelude.agdai b/src/SecretTypes/Prelude.agdai new file mode 100644 index 0000000..b61bc08 Binary files /dev/null and b/src/SecretTypes/Prelude.agdai differ diff --git a/src/SecretTypes/Typing.agda b/src/SecretTypes/Typing.agda new file mode 100644 index 0000000..7defbf3 --- /dev/null +++ b/src/SecretTypes/Typing.agda @@ -0,0 +1,25 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- Volpano–Smith security typing: expressions get the join of their +-- variables' labels; commands are typed under a program-counter label. +module SecretTypes.Typing where + +open import SecretTypes.Prelude +open import SecretTypes.Lattice +open import SecretTypes.Lang + +-- Classify an expression as secret exactly when it mentions hi; +-- literals and expressions using only lo are public. +lab : Expr → Label +lab (lit _) = L +lab (var x) = label x +lab (plus a b) = lab a ⊔ lab b + +infix 3 _⊢_ +data _⊢_ : Label → Cmd → Set where + skip : ∀ {pc} → pc ⊢ skip + assign : ∀ {pc x e} → pc ⊔ lab e ⊑ label x → pc ⊢ (x ≔ e) + seq : ∀ {pc c₁ c₂} → pc ⊢ c₁ → pc ⊢ c₂ → pc ⊢ (c₁ ﹔ c₂) + ifz : ∀ {pc e c₁ c₂} → pc ⊔ lab e ⊢ c₁ → pc ⊔ lab e ⊢ c₂ → pc ⊢ ifz e c₁ c₂ + while : ∀ {pc e c} → pc ⊔ lab e ⊢ c → pc ⊢ while e c diff --git a/src/SecretTypes/Typing.agdai b/src/SecretTypes/Typing.agdai new file mode 100644 index 0000000..1ef26d0 Binary files /dev/null and b/src/SecretTypes/Typing.agdai differ diff --git a/src/SecretTypes/Witness.agda b/src/SecretTypes/Witness.agda new file mode 100644 index 0000000..cafb327 --- /dev/null +++ b/src/SecretTypes/Witness.agda @@ -0,0 +1,56 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- Computed witnesses (TESTED): the typing side-condition is load-bearing. +module SecretTypes.Witness where + +open import SecretTypes.Prelude +open import SecretTypes.Lattice +open import SecretTypes.Lang +open import SecretTypes.Typing +open import SecretTypes.Noninterference + +-- An explicit flow and an implicit flow. Both are refused by the type +-- system (tests/reject/), and both actually leak: from low-equivalent +-- stores they end low-inequivalent. +explicit implicit : Cmd +explicit = lo ≔ var hi +implicit = ifz (var hi) (lo ≔ lit 0) (lo ≔ lit 1) + +s₀ s₁ : Store +s₀ = ⟨ 0 , 0 ⟩ +s₁ = ⟨ 0 , 1 ⟩ + +low-equivalent : s₀ ≈ s₁ +low-equivalent = refl + +explicit-leaks : ¬ (∀ {t t'} → exec 1 explicit s₀ ≡ just t → exec 1 explicit s₁ ≡ just t' → t ≈ t') +explicit-leaks h = absurd (h refl refl) + where absurd : 0 ≡ 1 → ⊥ + absurd () + +implicit-leaks : ¬ (∀ {t t'} → exec 1 implicit s₀ ≡ just t → exec 1 implicit s₁ ≡ just t' → t ≈ t') +implicit-leaks h = absurd (h refl refl) + where absurd : 0 ≡ 1 → ⊥ + absurd () + +-- A well-typed program with a secret loop guard: it spins forever when the +-- secret is 0 and stops at once otherwise, touching nothing public. +secret-loop : Cmd +secret-loop = while (var hi) skip + +secret-loop-typed : L ⊢ secret-loop +secret-loop-typed = while skip + +-- From s₁ the loop does not run (guard 1): finishes. From s₀ it runs until +-- the fuel is spent: `nothing`, so TINI has nothing to say — and need not. +secret-loop-stops : exec 3 secret-loop s₁ ≡ just s₁ +secret-loop-stops = refl + +secret-loop-spins : exec 3 secret-loop s₀ ≡ nothing +secret-loop-spins = refl + +-- Termination-insensitivity, made explicit: the public observer cannot +-- tell s₀ from s₁ by any finishing run of a well-typed program, but CAN by +-- whether the program finishes. That is the channel this theorem leaves +-- open, by name. diff --git a/tests/reject/ExplicitFlow.agda b/tests/reject/ExplicitFlow.agda new file mode 100644 index 0000000..76541bf --- /dev/null +++ b/tests/reject/ExplicitFlow.agda @@ -0,0 +1,11 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +module ExplicitFlow where +open import SecretTypes.Lattice +open import SecretTypes.Lang +open import SecretTypes.Typing + +-- Must fail: assigning the secret variable to the public one needs H ⊑ L. +invalid : L ⊢ (lo ≔ var hi) +invalid = assign L⊑L diff --git a/tests/reject/ImplicitFlow.agda b/tests/reject/ImplicitFlow.agda new file mode 100644 index 0000000..1e8e65a --- /dev/null +++ b/tests/reject/ImplicitFlow.agda @@ -0,0 +1,12 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +module ImplicitFlow where +open import SecretTypes.Lattice +open import SecretTypes.Lang +open import SecretTypes.Typing + +-- Must fail: branching on the secret raises the program counter to H, so +-- the public assignment inside the branch needs H ⊑ L. +invalid : L ⊢ ifz (var hi) (lo ≔ lit 0) (lo ≔ lit 1) +invalid = ifz (assign L⊑L) (assign L⊑L)