Skip to content

Mechanise Theorem 4 (delimited release for declassify) in Agda #8

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
nelsonduarte merged 1 commit into from
Jun 9, 2026
Merged

Mechanise Theorem 4 (delimited release for declassify) in Agda #8

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
87 changes: 63 additions & 24 deletions docs/semantics.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -363,23 +363,29 @@ mechanisation they would cite is already in tree.

## 9. Noninterference (information-flow soundness)

> **Status: pen-and-paper, NOT machine-checked.** Everything in
> Section 9 is a hand proof. Sections 1 to 8 above describe the
> capability calculus λ_cap, whose soundness *is* mechanised in
> [`proofs/`](../proofs/). Section 9 is a *different* property
> about a *different* calculus: termination-insensitive
> noninterference for a store-based imperative core λ_if that
> models Capa's information-flow control (the analyser in
> **Status: machine-checked.** Section 9 is now mechanised in Agda
> ([`proofs/CapaIF.agda`](../proofs/CapaIF.agda) and
> [`proofs/CapaNoninterference.agda`](../proofs/CapaNoninterference.agda),
> under `--safe`, no postulates): Lemma 1, Lemma 2, Theorem 3 (the
> declassify-free fragment) AND Theorem 4 (delimited release, with
> `declassify`) are all proved and typechecked in CI. Sections 1
> to 8 above describe the capability calculus λ_cap, whose
> soundness is mechanised in the same directory. Section 9 is a
> *different* property about a *different* calculus:
> termination-insensitive noninterference for a store-based
> imperative core λ_if that models Capa's information-flow control
> (the analyser in
> [`capa/analyzer/_ifc.py`](../capa/analyzer/_ifc.py) over the
> two-point lattice in [`capa/_labels.py`](../capa/_labels.py)).
> No Agda exists for λ_if yet. This section is written as the
> blueprint for that mechanisation: explicit syntax, explicit
> rules, explicit lemmas, proofs structured for transcription.
> It uses the same honesty conventions as
> [`proofs/README.md`](../proofs/README.md): the *calculus* is
> what is proved sound; fidelity between λ_if and the Python
> analyser is argued informally (Section 9.8), and we do **not**
> claim the Python analyser is verified.
> The prose below states the rules and proofs; the Agda is the
> artefact a referee re-checks. It uses the same honesty
> conventions as [`proofs/README.md`](../proofs/README.md): the
> *calculus* is what is proved sound; fidelity between λ_if and the
> Python analyser is argued informally (Section 9.8), and we do
> **not** claim the Python analyser is verified. Three encoding
> deviations (D1 total stores, D2 inductive big-step semantics, D3
> the release-log form of the Theorem 4 agreement hypothesis) are
> documented in `proofs/README.md` and inline in the Agda.

The result is the standard Volpano-Smith / Sabelfeld-Myers
noninterference theorem for a flow-sensitive type system,
Expand Down Expand Up @@ -932,6 +938,37 @@ SECRET value can become PUBLIC only by passing through a
`declassify`, and the theorem then relates only those runs that
already agree on what was released. ∎

> **Mechanisation note (encoding of the agreement hypothesis,
> deviation D3).** Theorems 3 and 4 are now machine-checked in
> Agda ([`proofs/CapaNoninterference.agda`](../proofs/CapaNoninterference.agda),
> `noninterference` and `theorem4`, under `--safe`, no postulates).
> The Agda development encodes the agreement hypothesis
> `⟦D(s)⟧_{σ_1}^{κ_1} = ⟦D(s)⟧_{σ_2}^{κ_2}` not as one flat
> multiset equality but in two structural forms (in
> [`proofs/CapaIF.agda`](../proofs/CapaIF.agda)): `EAgree` on
> expressions ("the two runs agree on every declassified value
> inside `e`") and `Agree` on the two big-step derivations
> ("...along the actual execution paths"). A concrete per-
> expression *release log* `releases κ σ e` is also defined (the
> sequence of declassified values an expression produces, the
> `declassify` analogue of the `sink` output trace `o`), and
> `EAgree` is proved EQUIVALENT to release-log equality
> `releases κ_1 σ_1 e = releases κ_2 σ_2 e` (`eagree->releq` /
> `releq->eagree`). So the Agda hypothesis IS the release-set
> agreement above, only phrased per declassify position so the
> `L-Op` and `L-Declassify` cases decompose without list-append
> reasoning. The derivation-indexed `Agree` is the faithful
> operational reading of `⟦D(s)⟧` evaluated at the store each
> declassify is actually reached in; where the two runs diverge
> under a SECRET guard it demands agreement only on the guard's
> releases, since the divergent declassifies are confined by
> Lemma 2 exactly as in the proof above. This keeps the hypothesis
> non-vacuous: a worked example in the Agda file
> (`sink(declassify(env_get))`) is covered by Theorem 4 but
> excluded from Theorem 3, and its agreement hypothesis reduces to
> secret equality `κ_1 = κ_2`, so Theorem 4 does not collapse into
> Theorem 3.

This matches the analyser's `declassify(value, reason: "...")`:
the label drops to PUBLIC (`_compute_label`), the value is
unchanged (`_check_declassify`), and the `reason` string is the
Expand Down Expand Up @@ -1015,16 +1052,18 @@ analyser is verified.** What λ_if deliberately abstracts away:
`@strict_ifc` code specifically, not of every program the
compiler accepts.

**Next step.** Section 9 is pen-and-paper. The planned
mechanisation is an Agda development for λ_if paralleling
**Mechanisation status.** Section 9 is now mechanised. The Agda
development for λ_if parallels
[`proofs/CapaSoundness.agda`](../proofs/CapaSoundness.agda):
syntax, the labelling and statement-typing relations, the
big-step semantics, Lemmas 1 and 2, and Theorems 3 and 4. The
two-point lattice, finite loop-fixpoint, and lock-step induction
make it a PLFA-scale development comparable to the existing
capability proof. Until that lands, the noninterference claim
should be cited as a *hand* proof, exactly as the capability
claim was before its Stage 1 to 4 mechanisation.
[`proofs/CapaIF.agda`](../proofs/CapaIF.agda) has the syntax, the
labelling and statement-typing relations, the big-step semantics,
and the release-log machinery; and
[`proofs/CapaNoninterference.agda`](../proofs/CapaNoninterference.agda)
has Lemmas 1 and 2 and Theorems 3 and 4. The two-point lattice,
finite loop-fixpoint, and lock-step induction made it a PLFA-scale
development comparable to the existing capability proof. The
noninterference claim is therefore now a *machine-checked* result
(under `--safe`, no postulates), not a hand proof.

---

Expand Down
132 changes: 130 additions & 2 deletions proofs/CapaIF.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,9 @@
-- flow-sensitive statement typing, and big-step operational
-- semantics for the lambda_if information-flow calculus described
-- in docs/semantics.md Section 9. This is the syntax/semantics
-- layer; the noninterference theorems are in
-- layer; it also defines the release-log machinery (`releases`,
-- `EAgree`, `Agree`) that the delimited-release Theorem 4 needs.
-- The noninterference theorems (3 and 4) are in
-- CapaNoninterference.agda.
--
-- STATUS: Typechecks on Agda >= 2.6.4 (developed and checked
Expand Down Expand Up @@ -427,7 +429,133 @@ data _,_,_=>_,_ (kappa : Nat) : Stmt -> Store -> Store -> Trace -> Set where

infix 4 _,_,_=>_,_

------------------------------------------------------------------
-- The unit type (a trivial agreement obligation).
------------------------------------------------------------------

record Unit : Set where
constructor tt

------------------------------------------------------------------
-- Non-dependent product (used to conjoin agreement obligations
-- here, and the theorem conclusions in CapaNoninterference.agda,
-- which re-uses this same record).
------------------------------------------------------------------

record _×_ (A B : Set) : Set where
constructor _,_
field
fst : A
snd : B

open _×_ public

infixr 2 _×_

------------------------------------------------------------------
-- Release log of an expression (Section 9.7.1 machinery).
--
-- `releases k s e` is the sequence of values that the declassify
-- nodes inside `e` produce when `e` is evaluated under ambient
-- secret `k` and store `s`, in left-to-right evaluation order,
-- innermost-first. This is the concrete "release log" the
-- delimited-release statement is about: it is to `declassify` what
-- the public output trace `o` is to `sink`. A declassify-free
-- expression releases nothing.
------------------------------------------------------------------

releases : Nat -> Store -> Expr -> Trace
releases k s (lit n) = []
releases k s (evar x) = []
releases k s (op a b) = releases k s a ++ releases k s b
releases k s env-get = []
releases k s (declassify e) = releases k s e ++ (eval k s e :: [])

------------------------------------------------------------------
-- Expression-level release agreement (Section 9.7.1).
--
-- `EAgree k1 s1 k2 s2 e` says the two runs (ambient secret k1 over
-- store s1, and k2 over s2) AGREE ON EVERY DECLASSIFIED VALUE
-- inside `e`. This is the structural, per-declassify-position form
-- of the paper's hypothesis `[| D(e) |]_{s1}^{k1} ==
-- [| D(e) |]_{s2}^{k2}`. It is provably equivalent to equality of
-- the release logs (`eagree<->releq` in CapaNoninterference.agda),
-- so it is exactly "the two release logs are equal" phrased so the
-- L-Op case decomposes without any list-append cancellation.
------------------------------------------------------------------

data EAgree (k1 : Nat) (s1 : Store) (k2 : Nat) (s2 : Store) : Expr -> Set where
ea-lit : forall {n} -> EAgree k1 s1 k2 s2 (lit n)
ea-var : forall {x} -> EAgree k1 s1 k2 s2 (evar x)
ea-op : forall {a b}
-> EAgree k1 s1 k2 s2 a
-> EAgree k1 s1 k2 s2 b
-> EAgree k1 s1 k2 s2 (op a b)
ea-env : EAgree k1 s1 k2 s2 env-get
-- the declassified value itself agrees, AND its sub-releases agree
ea-decl : forall {e}
-> EAgree k1 s1 k2 s2 e
-> eval k1 s1 e == eval k2 s2 e
-> EAgree k1 s1 k2 s2 (declassify e)

------------------------------------------------------------------
-- Statement-level release agreement, indexed by the TWO big-step
-- derivations (Section 9.7.1).
--
-- `Agree d1 d2` says the two runs agree on every declassified
-- value PRODUCED ALONG THE ACTUAL EXECUTION PATHS d1 and d2 -- the
-- faithful operational reading of the paper's ` [| D(s) |] == ...`
-- with `[| . |]` evaluated at the stores each declassify is
-- actually reached in. It is defined by recursion on the paired
-- derivations, so it composes exactly with the lock-step induction
-- of Theorem 4 and never needs list-append cancellation.
--
-- When the two runs take different control-flow paths (a SECRET
-- guard), only the guard's release agreement is recorded; the
-- divergent branches' declassifies are confined by Lemma 2 and
-- need no cross-run agreement, so no constraint is imposed there.
------------------------------------------------------------------

Agree : forall {k1 k2 s sigma1 sigma1' sigma2 sigma2' o1 o2}
-> k1 , s , sigma1 => sigma1' , o1
-> k2 , s , sigma2 => sigma2' , o2
-> Set
-- skip
Agree E-Skip E-Skip = Unit
-- assignment: agree on the released values of the RHS
Agree {k1 = k1} {k2 = k2} {sigma1 = s1} {sigma2 = s2}
(E-Assign {e = e}) E-Assign = EAgree k1 s1 k2 s2 e
-- sequencing: agree on both halves
Agree (E-Seq d1a d1b) (E-Seq d2a d2b) = Agree d1a d2a × Agree d1b d2b
-- conditional, same branch: guard releases agree, and the branch
Agree {k1 = k1} {k2 = k2} {sigma1 = s1} {sigma2 = s2}
(E-IfT {e = e} _ d1) (E-IfT _ d2) = EAgree k1 s1 k2 s2 e × Agree d1 d2
Agree {k1 = k1} {k2 = k2} {sigma1 = s1} {sigma2 = s2}
(E-IfF {e = e} _ d1) (E-IfF _ d2) = EAgree k1 s1 k2 s2 e × Agree d1 d2
-- conditional, divergent branches (only possible under a SECRET
-- guard): only the guard releases must agree
Agree {k1 = k1} {k2 = k2} {sigma1 = s1} {sigma2 = s2}
(E-IfT {e = e} _ _) (E-IfF _ _) = EAgree k1 s1 k2 s2 e
Agree {k1 = k1} {k2 = k2} {sigma1 = s1} {sigma2 = s2}
(E-IfF {e = e} _ _) (E-IfT _ _) = EAgree k1 s1 k2 s2 e
-- while, both stop: guard releases agree
Agree {k1 = k1} {k2 = k2} {sigma1 = s1} {sigma2 = s2}
(E-WhileF {e = e} _) (E-WhileF _) = EAgree k1 s1 k2 s2 e
-- while, both iterate: guard, body, and the rest all agree
Agree {k1 = k1} {k2 = k2} {sigma1 = s1} {sigma2 = s2}
(E-WhileT {e = e} _ b1 r1) (E-WhileT _ b2 r2)
= EAgree k1 s1 k2 s2 e × (Agree b1 b2 × Agree r1 r2)
-- while, divergent iteration counts (only under a SECRET guard):
-- only the guard releases must agree
Agree {k1 = k1} {k2 = k2} {sigma1 = s1} {sigma2 = s2}
(E-WhileF {e = e} _) (E-WhileT _ _ _) = EAgree k1 s1 k2 s2 e
Agree {k1 = k1} {k2 = k2} {sigma1 = s1} {sigma2 = s2}
(E-WhileT {e = e} _ _ _) (E-WhileF _) = EAgree k1 s1 k2 s2 e
-- sink: agree on the released values of the sunk expression
Agree {k1 = k1} {k2 = k2} {sigma1 = s1} {sigma2 = s2}
(E-Sink {e = e}) E-Sink = EAgree k1 s1 k2 s2 e

------------------------------------------------------------------
-- That is the syntax + semantics. Lemma 1, Lemma 2, Theorem 3,
-- and the Theorem 4 status are in CapaNoninterference.agda.
-- and Theorem 4 are in CapaNoninterference.agda.
------------------------------------------------------------------
Loading
Loading