From 3b609a2a9d719f8927f2bc69d4a5be12b16683b7 Mon Sep 17 00:00:00 2001 From: nelsoduarte Date: Tue, 9 Jun 2026 11:03:05 +0100 Subject: [PATCH] proofs: mechanise Theorem 4 (delimited release for declassify) in Agda Machine-checks lambda_if Theorem 4 (relaxed noninterference / delimited release, docs/semantics.md Section 9.7.1) under --safe, with no postulates and no holes. Theorem 3 is unchanged. CapaIF.agda: - releases: the per-expression release log (declassified values, the declassify analogue of the sink output trace). - EAgree / Agree: structural agreement predicates on expressions and on the two big-step derivations. Agree is the faithful operational reading of the paper's released-value agreement, evaluated at the store each declassify is actually reached in. CapaNoninterference.agda: - eagree->releq / releq->eagree: EAgree is equivalent to release log equality, so the agreement hypothesis IS release-log equality, phrased per position so L-Op / L-Declassify decompose without list-append surgery (helpers len, dcount, releases-length, ++-cancel). - lemma1-decl: Lemma 1 re-admitting declassify; the L-Declassify case is discharged by the agreement witness. - theorem4: Theorem 3 clause for clause with declassify allowed; low cases use lemma1-decl, SECRET cases use confinement and never consult the agreement. - worked example sink(declassify(env-get)): covered by Theorem 4, excluded from Theorem 3, agreement reduces to secret equality, so Theorem 4 does not collapse into Theorem 3. Documents deviation D3 (release-log encoding of the agreement hypothesis) in proofs/README.md and docs/semantics.md Section 9.7.1; moves Theorem 4 from "future" to shipped. Checked locally on Agda 2.7.0.1. --- docs/semantics.md | 87 +++++-- proofs/CapaIF.agda | 132 +++++++++- proofs/CapaNoninterference.agda | 421 ++++++++++++++++++++++++++++---- proofs/README.md | 103 +++++--- 4 files changed, 630 insertions(+), 113 deletions(-) diff --git a/docs/semantics.md b/docs/semantics.md index be2bf3b..024498e 100644 --- a/docs/semantics.md +++ b/docs/semantics.md @@ -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, @@ -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 @@ -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. --- diff --git a/proofs/CapaIF.agda b/proofs/CapaIF.agda index 81a681c..c6f9d07 100644 --- a/proofs/CapaIF.agda +++ b/proofs/CapaIF.agda @@ -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 @@ -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. ------------------------------------------------------------------ diff --git a/proofs/CapaNoninterference.agda b/proofs/CapaNoninterference.agda index aa7fe1e..d90727a 100644 --- a/proofs/CapaNoninterference.agda +++ b/proofs/CapaNoninterference.agda @@ -11,11 +11,16 @@ -- * Lemma 1 (expression label soundness) : lemma1 -- * Lemma 2 (confinement / high-pc) : confinement -- * Theorem 3 (declassify-free noninterference) : noninterference +-- * Lemma 1 with declassify : lemma1-decl +-- * Theorem 4 (delimited release / relaxed : theorem4 +-- noninterference for declassify) -- --- Theorem 4 (delimited release for declassify) is NOT mechanised --- in this pass. It is left as a clearly-marked future item with a --- precise statement below; it is NOT postulated. See the closing --- comment and proofs/README.md for the honest status. +-- Theorem 4 is the delimited-release statement of Section 9.7.1: +-- declassify is re-admitted (no declassify-free restriction), and +-- the conclusion holds modulo an agreement hypothesis on the +-- declassified values (see `Agree` / `EAgree` in CapaIF.agda and +-- the encoding note at the foot of this file). It is a real proof, +-- not a postulate; the module is checked under --safe. -- -- STATUS: Typechecks on Agda >= 2.6.4 (developed and checked -- locally on Agda 2.7.0.1; CI pins 2.6.4.3). Verified in CI (see @@ -41,19 +46,10 @@ module CapaNoninterference where open import CapaIF ------------------------------------------------------------------ --- Products and sums (self-contained, no agda-stdlib). +-- The non-dependent product `_×_` (with fst / snd) is defined in +-- CapaIF.agda and re-exported here via `open import CapaIF`. ------------------------------------------------------------------ -record _×_ (A B : Set) : Set where - constructor _,_ - field - fst : A - snd : B - -open _×_ public - -infixr 2 _×_ - ------------------------------------------------------------------ -- Low-equivalence of stores at a label environment (Section 9.6). -- Two stores agree on every PUBLIC-labelled variable. With total @@ -442,47 +438,368 @@ noninterference {k1 = k1} {k2 = k2} {sigma1 = s1} {sigma2 = s2} ------------------------------------------------------------------ -- Theorem 4 (Relaxed noninterference / delimited release, --- Section 9.7.1): STATUS = NOT MECHANISED in this pass. +-- Section 9.7.1): MECHANISED below, with NO postulates and NO +-- holes, checked under --safe. +-- +-- Encoding of the agreement hypothesis (deviation D3, documented +-- in proofs/README.md and docs/semantics.md Section 9.7.1). The +-- paper writes the hypothesis as `[| D(s) |]_{s1}^{k1} == +-- [| D(s) |]_{s2}^{k2}`, equality of the multiset/tuple of +-- declassified values. We use the per-position structural form +-- `EAgree` on expressions and `Agree` on the two big-step +-- derivations (both in CapaIF.agda): -- --- This is an HONEST gap, NOT a postulate. There is deliberately no --- Agda term for Theorem 4 below: faking it with a `postulate` --- would defeat the purpose of a machine-checked artefact, and the --- module is checked under --safe precisely so that no such cheat --- can sneak in. +-- * `EAgree k1 s1 k2 s2 e` -- the two runs agree on every +-- declassified value inside expression `e`. We prove it is +-- EQUIVALENT to equality of the expression release logs +-- `releases k1 s1 e == releases k2 s2 e` (`eagree->releq` and +-- `releq->eagree` below), so adopting it does not weaken the +-- hypothesis: it IS release-log equality, phrased so the +-- L-Op / L-Declassify cases decompose without list-append +-- surgery. -- --- The precise statement it WOULD have, transcribing Section 9.7.1, --- is recorded here as a comment so a future contributor has the --- exact obligation: +-- * `Agree d1 d2` -- the run-level form, threaded along the two +-- ACTUAL execution paths. This is the faithful operational +-- reading of `[| D(s) |]` evaluated at the stores each +-- declassify is really reached in. Where the two runs diverge +-- (a SECRET guard) only the guard releases must agree; the +-- divergent declassifies are confined by Lemma 2, exactly as +-- in the paper proof, so demanding cross-run agreement on them +-- would be spurious. This is why Theorem 4 does NOT collapse +-- into Theorem 3: the hypothesis is a real, non-vacuous +-- condition on the low-context declassifies. +-- +-- The proof is "Theorem 3 plus one Lemma-1 case for L-Declassify, +-- discharged by the agreement hypothesis" (Section 9.7.1), with +-- the run-level agreement supplying the per-site witnesses. +------------------------------------------------------------------ + +------------------------------------------------------------------ +-- Release-log machinery: `EAgree` is equivalent to equality of +-- the expression release logs. This justifies calling `EAgree` +-- "the two release logs agree". +------------------------------------------------------------------ + +-- length of a trace, and the syntactic declassify-node count of an +-- expression. The release-log length is store-independent: it is +-- exactly the number of declassify nodes (`releases-length`), +-- which is what lets equal release logs be split at op nodes. + +len : Trace -> Nat +len [] = zero +len (_ :: xs) = suc (len xs) + +dcount : Expr -> Nat +dcount (lit n) = zero +dcount (evar x) = zero +dcount (op a b) = dcount a +N dcount b +dcount env-get = zero +dcount (declassify e) = suc (dcount e) + +len-++ : forall (xs ys : Trace) -> len (xs ++ ys) == (len xs +N len ys) +len-++ [] ys = refl +len-++ (x :: xs) ys = cong suc (len-++ xs ys) + +releases-length : forall (k : Nat) (s : Store) (e : Expr) + -> len (releases k s e) == dcount e +releases-length k s (lit n) = refl +releases-length k s (evar x) = refl +releases-length k s (op a b) + = trans (len-++ (releases k s a) (releases k s b)) + (cong2 _+N_ (releases-length k s a) (releases-length k s b)) +releases-length k s env-get = refl +releases-length k s (declassify e) + = trans (len-++ (releases k s e) (eval k s e :: [])) + (trans (cong (\ n -> n +N suc zero) (releases-length k s e)) + (n+1 (dcount e))) + where + n+1 : forall (n : Nat) -> (n +N suc zero) == suc n + n+1 zero = refl + n+1 (suc m) = cong suc (n+1 m) + +-- cons injectivity for traces. +cons-head : forall {a b : Nat} {as bs} -> (a :: as) == (b :: bs) -> a == b +cons-head refl = refl + +cons-tail : forall {a b : Nat} {as bs} -> (a :: as) == (b :: bs) -> as == bs +cons-tail refl = refl + +-- append cancellation when the two prefixes have equal length. +++-cancel : forall (xs1 xs2 ys1 ys2 : Trace) + -> len xs1 == len xs2 + -> (xs1 ++ ys1) == (xs2 ++ ys2) + -> (xs1 == xs2) × (ys1 == ys2) +++-cancel [] [] ys1 ys2 _ eq = refl , eq +++-cancel [] (x2 :: xs2) ys1 ys2 () _ +++-cancel (x1 :: xs1) [] ys1 ys2 () _ +++-cancel (x1 :: xs1) (x2 :: xs2) ys1 ys2 leq eq + with ++-cancel xs1 xs2 ys1 ys2 (suc-inj leq) (cons-tail eq) +... | (ts , us) = cong2 _::_ (cons-head eq) ts , us + +-- forward: EAgree implies the release logs are equal. +eagree->releq : forall {k1 s1 k2 s2 e} + -> EAgree k1 s1 k2 s2 e + -> releases k1 s1 e == releases k2 s2 e +eagree->releq ea-lit = refl +eagree->releq ea-var = refl +eagree->releq (ea-op a b) = cong2 _++_ (eagree->releq a) (eagree->releq b) +eagree->releq ea-env = refl +eagree->releq {k1 = k1} {s1 = s1} {k2 = k2} {s2 = s2} (ea-decl {e = e} a veq) + = cong2 _++_ (eagree->releq a) (cong (\ v -> v :: []) veq) + +-- backward: equal release logs imply EAgree. Uses releases-length +-- to split the op case and the declassify case. This closes the +-- equivalence, so EAgree IS release-log equality. +releq->eagree : forall {k1 s1 k2 s2} (e : Expr) + -> releases k1 s1 e == releases k2 s2 e + -> EAgree k1 s1 k2 s2 e +releq->eagree (lit n) eq = ea-lit +releq->eagree (evar x) eq = ea-var +releq->eagree {k1 = k1} {s1 = s1} {k2 = k2} {s2 = s2} (op a b) eq + with ++-cancel (releases k1 s1 a) (releases k2 s2 a) + (releases k1 s1 b) (releases k2 s2 b) + (trans (releases-length k1 s1 a) (sym (releases-length k2 s2 a))) + eq +... | aeq , beq = ea-op (releq->eagree a aeq) (releq->eagree b beq) +releq->eagree env-get eq = ea-env +releq->eagree {k1 = k1} {s1 = s1} {k2 = k2} {s2 = s2} (declassify e) eq + with ++-cancel (releases k1 s1 e) (releases k2 s2 e) + (eval k1 s1 e :: []) (eval k2 s2 e :: []) + (trans (releases-length k1 s1 e) (sym (releases-length k2 s2 e))) + eq +... | eeq , veq = ea-decl (releq->eagree e eeq) (cons-head veq) + +------------------------------------------------------------------ +-- Lemma 1 with declassify (Section 9.7.1). -- --- Let D(s) be the multiset of sub-expressions sitting directly --- inside declassify(.) positions of s, and let [| D(s) |]_sigma^k --- be the tuple of values they evaluate to in a given run. Then --- for s well-typed with PUBLIC , Gamma_0 |-s s ~> Gamma', for --- low-equivalent sigma1 ~[Gamma_0] sigma2 with ambient secrets --- k1, k2, IF both runs converge AND the two runs agree on every --- declassified value, i.e. [| D(s) |]_{sigma1}^{k1} == --- [| D(s) |]_{sigma2}^{k2}, then sigma1' ~[Gamma'] sigma2' and --- o1 == o2. +-- Like `lemma1`, but admitting `declassify`: a PUBLIC-labelled +-- expression evaluates equally in two low-equivalent runs PROVIDED +-- the two runs agree on its declassified values (`EAgree`). The +-- only new case beyond `lemma1` is L-Declassify, discharged +-- directly by the `ea-decl` agreement witness -- exactly the +-- paper's one-line extra case. No DFExpr restriction. No holes. +------------------------------------------------------------------ + +lemma1-decl : forall {g e l k1 k2 s1 s2} + -> g |-e e ~> l + -> l == PUBLIC + -> LowEq g s1 s2 + -> EAgree k1 s1 k2 s2 e + -> eval k1 s1 e == eval k2 s2 e +lemma1-decl L-Lit p leq ea-lit = refl +lemma1-decl (L-Var {x = x}) p leq ea-var = leq x p +lemma1-decl (L-Op d1 d2) p leq (ea-op a1 a2) + = cong2 _+N_ + (lemma1-decl d1 (join-public-l p) leq a1) + (lemma1-decl d2 (join-public-r p) leq a2) +lemma1-decl L-Env () leq ea-env +-- declassify: eval (declassify e0) = eval e0, and the agreement +-- witness IS the equality of those two values across runs. +lemma1-decl (L-Declassify _) p leq (ea-decl _ veq) = veq + +------------------------------------------------------------------ +-- Theorem 4 (Relaxed noninterference / delimited release, +-- Section 9.7.1). -- --- The paper proof (Section 9.7.1) is "identical to Theorem 3 with --- one extra Lemma-1 case for L-Declassify, discharged directly by --- the agreement hypothesis". The mechanisation work it needs that --- this pass does not do: --- 1. drop the DFExpr / DFStmt restriction from the inputs of --- lemma1 and noninterference (re-admitting declassify); --- 2. define the released-values tuple [| D(s) |] as a function --- of (s, k, sigma) and thread the run-agreement hypothesis --- through the L-Declassify case of lemma1 and the assign / --- sink cases of noninterference; --- 3. handle that, under declassify, a sub-expression's run-to-run --- agreement is an ASSUMPTION rather than a consequence, so the --- generalised induction's invariant must carry the agreement --- witness for the declassified positions reached so far. +-- For a well-typed statement s (NO declassify-free restriction: +-- DFStmt is gone), two runs from low-equivalent stores that +-- additionally AGREE on every declassified value reached along +-- their execution paths (`Agree ev1 ev2`), the final stores are +-- low-equivalent at the final environment and the public output +-- traces are identical. -- --- Step 2's bookkeeping (a faithful [| D(s) |] over the big-step --- relation, aligned across two runs that may take different --- control-flow paths) is the bulk of the work and is left for a --- follow-up. Theorem 3 above is fully mechanised and checked under --- --safe; Theorem 4 is future work, tracked in proofs/README.md. +-- The proof mirrors `noninterference` (Theorem 3) clause for +-- clause; the only changes are: +-- * the DFStmt argument and the DFExpr arguments are dropped; +-- * every appeal to `lemma1` becomes an appeal to `lemma1-decl`, +-- fed the per-site `EAgree` witness pulled out of `Agree`; +-- * the SECRET (high) cases are byte-for-byte the Theorem 3 +-- argument: they use confinement only and never touch the +-- agreement, since declassifies under SECRET pc are confined. +-- No holes, no postulates on this result. ------------------------------------------------------------------ +theorem4 + : forall {pc g g' s k1 k2 sigma1 sigma2 sigma1' sigma2' o1 o2} + -> pc , g |-s s ~> g' + -> (ev1 : k1 , s , sigma1 => sigma1' , o1) + -> (ev2 : k2 , s , sigma2 => sigma2' , o2) + -> LowEq g sigma1 sigma2 + -> Agree ev1 ev2 + -> LowEq g' sigma1' sigma2' × (o1 == o2) + +-- skip +theorem4 T-Skip E-Skip E-Skip leq ag = leq , refl + +-- assignment +theorem4 {pc = pc} {k1 = k1} {k2 = k2} {sigma1 = s1} {sigma2 = s2} + (T-Assign {x = a} {e = e} {l = l} de) E-Assign E-Assign leq ag + = leqOut , refl + where + leqOut : LowEq _ _ _ + leqOut y py with var-eq a y + ... | yes refl = + let lpub : l == PUBLIC + lpub = join-public-l (trans (sym (env-hit _ a (l join pc))) py) + in trans (update-hit s1 a (eval k1 s1 e)) + (trans (lemma1-decl de lpub leq ag) + (sym (update-hit s2 a (eval k2 s2 e)))) + ... | no q = + let gy : _ == PUBLIC + gy = trans (sym (env-miss _ a y (l join pc) q)) py + in trans (update-miss s1 a y (eval k1 s1 e) q) + (trans (leq y gy) (sym (update-miss s2 a y (eval k2 s2 e) q))) + +-- sequencing +theorem4 (T-Seq d1 d2) (E-Seq e1a e1b) (E-Seq e2a e2b) leq ag + with theorem4 d1 e1a e2a leq (fst ag) +... | (leq1 , oeq1) with theorem4 d2 e1b e2b leq1 (snd ag) +... | (leq2 , oeq2) = leq2 , cong2 _++_ oeq1 oeq2 + +-- conditional, low guard (l = PUBLIC): same branch in both runs +theorem4 (T-If {l = PUBLIC} de d1 d2) (E-IfT ev1 b1) (E-IfT ev2 b2) leq ag + with theorem4 d1 b1 b2 leq (snd ag) +... | (leqB , oeqB) = (\ y py -> leqB y (join-public-l py)) , oeqB +theorem4 (T-If {l = PUBLIC} de d1 d2) (E-IfF ev1 b1) (E-IfF ev2 b2) leq ag + with theorem4 d2 b1 b2 leq (snd ag) +... | (leqB , oeqB) = (\ y py -> leqB y (join-public-r py)) , oeqB +-- cross cases ruled out: Lemma 1 (with declassify) forces equal +-- guard evaluation, using the guard's release agreement +theorem4 (T-If {l = PUBLIC} de d1 d2) (E-IfT ev1 b1) (E-IfF ev2 b2) leq ag + = absurd (zero-not-suc (trans (sym ev2) (trans (sym (lemma1-decl de refl leq ag)) ev1))) +theorem4 (T-If {l = PUBLIC} de d1 d2) (E-IfF ev1 b1) (E-IfT ev2 b2) leq ag + = absurd (zero-not-suc (trans (sym ev1) (trans (lemma1-decl de refl leq ag) ev2))) + +-- conditional, high guard (l = SECRET): confinement, identical to +-- Theorem 3; the agreement is not consulted (declassifies under +-- SECRET pc are confined). +theorem4 (T-If {pc = pc} {l = SECRET} de d1 d2) (E-IfT _ b1) (E-IfT _ b2) leq ag + = (\ y py -> let g1p = join-public-l py + in trans (snd c1 y g1p) (trans (leq y (mono-secret dd1 y g1p)) (sym (snd c2 y g1p)))) + , trans (fst c1) (sym (fst c2)) + where dd1 = retype-pc (join-secret-r pc) d1 + c1 = confinement dd1 b1 + c2 = confinement dd1 b2 +theorem4 (T-If {pc = pc} {l = SECRET} de d1 d2) (E-IfT _ b1) (E-IfF _ b2) leq ag + = (\ y py -> let g1p = join-public-l py ; g2p = join-public-r py + in trans (snd c1 y g1p) (trans (leq y (mono-secret dd1 y g1p)) (sym (snd c2 y g2p)))) + , trans (fst c1) (sym (fst c2)) + where dd1 = retype-pc (join-secret-r pc) d1 + dd2 = retype-pc (join-secret-r pc) d2 + c1 = confinement dd1 b1 + c2 = confinement dd2 b2 +theorem4 (T-If {pc = pc} {l = SECRET} de d1 d2) (E-IfF _ b1) (E-IfT _ b2) leq ag + = (\ y py -> let g1p = join-public-l py ; g2p = join-public-r py + in trans (snd c1 y g2p) (trans (leq y (mono-secret dd2 y g2p)) (sym (snd c2 y g1p)))) + , trans (fst c1) (sym (fst c2)) + where dd1 = retype-pc (join-secret-r pc) d1 + dd2 = retype-pc (join-secret-r pc) d2 + c1 = confinement dd2 b1 + c2 = confinement dd1 b2 +theorem4 (T-If {pc = pc} {l = SECRET} de d1 d2) (E-IfF _ b1) (E-IfF _ b2) leq ag + = (\ y py -> let g2p = join-public-r py + in trans (snd c1 y g2p) (trans (leq y (mono-secret dd2 y g2p)) (sym (snd c2 y g2p)))) + , trans (fst c1) (sym (fst c2)) + where dd2 = retype-pc (join-secret-r pc) d2 + c1 = confinement dd2 b1 + c2 = confinement dd2 b2 + +-- while, low guard (l = PUBLIC): lock-step iteration +theorem4 (T-While {l = PUBLIC} de db) (E-WhileF ev1) (E-WhileF ev2) leq ag + = leq , refl +theorem4 (T-While {l = PUBLIC} de db) + (E-WhileT ev1 body1 rest1) (E-WhileT ev2 body2 rest2) leq ag + with theorem4 db body1 body2 leq (fst (snd ag)) +... | (leqBody , oeqBody) + with theorem4 (T-While de db) rest1 rest2 leqBody (snd (snd ag)) +... | (leqRest , oeqRest) = leqRest , cong2 _++_ oeqBody oeqRest +-- mismatched iteration counts ruled out by Lemma 1 (with declassify) +theorem4 (T-While {l = PUBLIC} de db) (E-WhileF ev1) (E-WhileT ev2 _ _) leq ag + = absurd (zero-not-suc (trans (sym ev1) (trans (lemma1-decl de refl leq ag) ev2))) +theorem4 (T-While {l = PUBLIC} de db) (E-WhileT ev1 _ _) (E-WhileF ev2) leq ag + = absurd (zero-not-suc (trans (sym ev2) (trans (sym (lemma1-decl de refl leq ag)) ev1))) + +-- while, high guard (l = SECRET): confine both loops (Theorem 3 +-- argument verbatim; agreement not consulted) +theorem4 (T-While {pc = pc} {l = SECRET} de db) ev1 ev2 leq ag + = leqOut , trans (fst conf1) (sym (fst conf2)) + where + dbS : SECRET , _ |-s _ ~> _ + dbS = retype-pc (join-secret-r pc) db + conf1 = while-high-conf dbS ev1 + conf2 = while-high-conf dbS ev2 + leqOut : LowEq _ _ _ + leqOut y py = + trans (snd conf1 y py) (trans (leq y py) (sym (snd conf2 y py))) + +-- sink +theorem4 {k1 = k1} {k2 = k2} {sigma1 = s1} {sigma2 = s2} + (T-Sink {e = e} {l = l} de fl) E-Sink E-Sink leq ag + = leq , cong (\ v -> v :: []) valeq + where + lpub : l == PUBLIC + lpub = join-public-l (flows-public-is-public fl) + valeq : eval k1 s1 e == eval k2 s2 e + valeq = lemma1-decl de lpub leq ag + +------------------------------------------------------------------ +-- Non-vacuity witness (Section 9.7.1). +-- +-- A concrete declassify-and-sink program that is (a) well-typed, +-- (b) evaluable, (c) covered by Theorem 4, and (d) EXCLUDED from +-- Theorem 3 (it contains declassify, so no DFStmt holds for it). +-- +-- The program is sink(declassify(env-get)) under PUBLIC pc and +-- the all-PUBLIC environment. It declassifies the secret and sinks +-- it -- exactly the pattern Theorem 3 forbids. Theorem 4 covers it +-- and, crucially, its conclusion DEPENDS on the agreement +-- hypothesis: the sunk value is the declassified secret, so two +-- runs with DIFFERENT secrets produce DIFFERENT public output +-- unless they agree on the declassified value. The agreement +-- `EAgree k1 s1 k2 s2 (declassify env-get)` for this program is +-- precisely `k1 == k2` (the released value is the secret itself), +-- a genuinely non-trivial condition. Hence Theorem 4 does not +-- collapse into Theorem 3. +------------------------------------------------------------------ + +-- the program is well-typed under PUBLIC pc in the all-PUBLIC env +example-prog : Stmt +example-prog = sink (declassify env-get) + +example-env : Env +example-env _ = PUBLIC + +example-typed : PUBLIC , example-env |-s example-prog ~> example-env +example-typed = T-Sink (L-Declassify L-Env) pub-flows + +-- it evaluates from any store, emitting the secret as public output +example-eval : forall (k : Nat) (s : Store) + -> k , example-prog , s => s , (k :: []) +example-eval k s = E-Sink + +-- the agreement hypothesis for this program is exactly k1 == k2: +-- the released value is the secret, so agreement IS secret-equality +example-agree-is-keq : forall {k1 k2 s1 s2} + -> k1 == k2 + -> Agree (example-eval k1 s1) (example-eval k2 s2) +example-agree-is-keq keq = ea-decl ea-env keq + +-- WITHOUT agreement the public outputs differ: two runs with +-- distinct secrets emit distinct traces. This shows the hypothesis +-- is NECESSARY (the conclusion o1 == o2 fails when k1 /= k2), +-- so Theorem 4 genuinely depends on it. +example-needs-agreement : forall {k1 k2 : Nat} + -> (k1 :: []) == (k2 :: []) + -> k1 == k2 +example-needs-agreement refl = refl + +-- Theorem 4 applied to the example: low-equivalent stores plus the +-- agreement (here k1 == k2) give equal public output. +example-theorem4 : forall {k1 k2 s1 s2} + -> LowEq example-env s1 s2 + -> k1 == k2 + -> ((k1 :: []) == (k2 :: [])) +example-theorem4 {s1 = s1} {s2 = s2} leq keq + = snd (theorem4 example-typed (example-eval _ s1) (example-eval _ s2) + leq (example-agree-is-keq keq)) + diff --git a/proofs/README.md b/proofs/README.md index ee87ff5..b46b2f9 100644 --- a/proofs/README.md +++ b/proofs/README.md @@ -3,26 +3,25 @@ [![agda](https://github.com/nelsonduarte/capa-language/actions/workflows/agda.yml/badge.svg)](https://github.com/nelsonduarte/capa-language/actions/workflows/agda.yml) > **Status (2026-06-09): all four capability soundness theorems -> proved, PLUS Lemma 1, Lemma 2, and the declassify-free -> noninterference theorem for λ_if; mechanically typechecked in -> CI; no postulates remain.** This directory holds two -> formalisations in Agda. (1) The λ_cap capability calculus: -> syntax, typing, reduction, PLFA-style parallel substitution, the -> inductive `_∈caps_` relation, and the reflexive-transitive -> closure `_==>*_`; Progress, Preservation, Capability Soundness, -> and Manifest Completeness ([`docs/semantics.md`](../docs/semantics.md) +> proved, PLUS Lemma 1, Lemma 2, the declassify-free +> noninterference theorem (Theorem 3) AND the delimited-release +> theorem (Theorem 4) for λ_if; mechanically typechecked in CI; no +> postulates remain.** This directory holds two formalisations in +> Agda. (1) The λ_cap capability calculus: syntax, typing, +> reduction, PLFA-style parallel substitution, the inductive +> `_∈caps_` relation, and the reflexive-transitive closure +> `_==>*_`; Progress, Preservation, Capability Soundness, and +> Manifest Completeness ([`docs/semantics.md`](../docs/semantics.md) > Theorems 1 and 2) are proved. (2) The λ_if information-flow > calculus ([`docs/semantics.md`](../docs/semantics.md) Section 9): > the two-point security lattice, expression labelling, > flow-sensitive statement typing, an inductive big-step -> semantics, low-equivalence, and the noninterference theorem -> (Theorem 3) with its two supporting lemmas. The -> noninterference modules typecheck under Agda's `--safe` flag, -> which mechanically forbids postulates, `trustMe`, and unsafe -> pragmas. **Theorem 4 (delimited release for `declassify`) is -> NOT yet mechanised**; it is recorded as an honest future item -> (a documented obligation, not a postulate) at the foot of -> `CapaNoninterference.agda`. +> semantics, low-equivalence, the noninterference theorem +> (Theorem 3) with its two supporting lemmas, AND the +> delimited-release / relaxed-noninterference theorem (Theorem 4) +> for the full calculus WITH `declassify`. The noninterference +> modules typecheck under Agda's `--safe` flag, which mechanically +> forbids postulates, `trustMe`, and unsafe pragmas. ## What this directory is for @@ -87,16 +86,25 @@ tactics differ. - `CapaNoninterference.agda`: the noninterference development. Lemma 1 (expression label soundness, `lemma1`), Lemma 2 - (confinement / high-pc, `confinement`), and Theorem 3 + (confinement / high-pc, `confinement`), Theorem 3 (termination-insensitive noninterference for the - declassify-free fragment, `noninterference`). Two supporting - lemmas the paper proof uses implicitly are made explicit and - proved: `mono-secret` (a SECRET-pc statement never lowers a - label to PUBLIC) and `while-high-conf` (a SECRET-guarded loop - emits nothing and touches no PUBLIC variable). Theorem 4 - (delimited release) is left as a clearly-marked future item - (a precise commented obligation, NOT a postulate). The whole - module is checked under `--safe`. + declassify-free fragment, `noninterference`), and Theorem 4 + (delimited release / relaxed noninterference for the full + calculus with `declassify`, `theorem4`). Two supporting lemmas + the paper proof uses implicitly are made explicit and proved: + `mono-secret` (a SECRET-pc statement never lowers a label to + PUBLIC) and `while-high-conf` (a SECRET-guarded loop emits + nothing and touches no PUBLIC variable). Theorem 4 reuses + `lemma1-decl` (Lemma 1 re-admitting `declassify`, discharged in + the L-Declassify case by the agreement hypothesis) and the + release-log machinery from `CapaIF.agda`. The whole module is + checked under `--safe`. A small worked example at the foot of + the module (`example-prog = sink(declassify(env-get))`) shows a + declassify-and-sink program that is covered by Theorem 4 but + EXCLUDED from Theorem 3 (it has no `DFStmt` derivation), and + proves the agreement hypothesis for it is exactly secret + equality `k1 == k2`, so Theorem 4 does not collapse into + Theorem 3. ## How to typecheck @@ -203,22 +211,23 @@ Honest tracking: | λ_if Lemma 1: expression label soundness | landed | | λ_if Lemma 2: confinement / high-pc | landed | | λ_if Theorem 3: declassify-free noninterference | landed | -| λ_if Theorem 4: delimited release | future (honest gap, not a postulate) | +| λ_if Theorem 4: delimited release | landed (machine-checked, `--safe`) | -The four capability soundness theorems and the λ_if -noninterference theorem (Theorem 3, with Lemmas 1 and 2) are -machine-verified; the noninterference modules pass under -`--safe`. The paper can cite them as such; the Agda source in -this directory is the artefact a referee opens. Theorem 4 -(delimited release) is the one remaining future item, recorded -as a precise obligation at the foot of `CapaNoninterference.agda`. +The four capability soundness theorems and BOTH λ_if +noninterference theorems (Theorem 3 for the declassify-free +fragment and Theorem 4, delimited release, for the full calculus +with `declassify`, with Lemmas 1 and 2) are machine-verified; the +noninterference modules pass under `--safe`. The paper can cite +them as such; the Agda source in this directory is the artefact a +referee opens. No future-item gap remains in the λ_if +development. ## λ_if: deviations from the Section 9 paper proof The mechanisation is faithful to [`docs/semantics.md`](../docs/semantics.md) Section 9 rule for -rule. Two encoding choices differ from the prose, both documented -inline in `CapaIF.agda` and neither weakening the theorem: +rule. Three encoding choices differ from the prose, all documented +inline in `CapaIF.agda` and none weakening the theorem: - **D1 (total stores).** Stores and label environments are total functions `Var -> Nat` / `Var -> L` rather than finite partial @@ -236,6 +245,30 @@ inline in `CapaIF.agda` and neither weakening the theorem: relates only runs for which both derivations exist (both converge), matching the theorem's hypothesis. +- **D3 (release-log agreement for Theorem 4).** Section 9.7.1 + writes the delimited-release hypothesis as equality of the + multiset/tuple of declassified values, + `[| D(s) |]_{σ1}^{κ1} == [| D(s) |]_{σ2}^{κ2}`. The Agda + encoding uses two structural forms (in `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"). `EAgree` is + proved EQUIVALENT to equality of the expression release logs + `releases k1 s1 e == releases k2 s2 e` (`eagree<->releq`: + `eagree->releq` and `releq->eagree` in + `CapaNoninterference.agda`), where `releases` is the concrete + per-expression release log -- declassify's analogue of the `sink` + output trace. So the hypothesis IS release-log equality, phrased + per-position so the L-Op / L-Declassify cases decompose without + list-append surgery. 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 releases (the divergent declassifies are confined by + Lemma 2, exactly as the paper proof handles them), so the + hypothesis is a real, non-vacuous condition on the low-context + declassifies and Theorem 4 does NOT collapse into Theorem 3. + The proof also makes explicit two facts the paper proof uses silently: `mono-secret` (under SECRET pc, no rule manufactures a fresh PUBLIC label) and `while-high-conf` (a SECRET-guarded loop