Information-Flow Type Systems and Noninterference

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

Preservation and progress cannot distinguish the following command from an ordinary well-typed conditional: $$\begin{array}{}\text{(}\mathsf{Leak}\text{)}& \mathbf{if}h=0\mathbf{then}l:=0\mathbf{else}l:=1.\end{array}$$ Both branches assign integers. Nevertheless, an observer who may read the public variable $l$ learns whether the secret $h$ was zero. The missing invariant relates two runs: changing only secret inputs must not change public outputs. For the imperative language below, that relation is the exact termination-insensitive noninterference property to establish.

Stores, observations, and the security lattice

Fix a finite lattice $(\mathcal{L},{⊑}_{\mathsf{sec}},\bigsqcup ,\mathrm{\perp })$. A security environment $\mathrm{\Gamma }:\mathsf{Var}\to \mathcal{L}$ assigns a fixed label to every mutable variable. Expressions and commands are Stores map variables to integers. The deterministic big-step relation is $⟨c,s⟩{\Downarrow }_{\mathsf{IF}}{s}^{\prime }$; its assignment, sequence, conditional, and terminating-loop rules appear in appendix A. The theorem will quantify only over pairs of terminating derivations.

An observer at level $o$ sees the variables labelled at most $o$.

On the two-point lattice $L{⊑}_{\mathsf{sec}}H$, stores agreeing on $l:L$ are low-equivalent at $L$, regardless of their values at $h:H$. Taking $s_0(h)=0$ and $s_1(h)=7$ in (Leak) yields outputs with $l=0$ and $l=1$, so the command fails the relation.

Expression labels and command typing

The expression judgment $\mathrm{\Gamma }⊢e:\ell$ assigns an upper bound to every variable read by $e$: constants have label $\mathrm{\perp }$, a variable has label $\mathrm{\Gamma }(x)$, and a compound expression joins the labels of its operands. Boolean guards use the same join.

Commands are checked under a program-counter label: $\mathrm{\Gamma }{⊢}_p^{\mathsf{IF}}c$. The label $p$ records the information already revealed by control flow. $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢e:\ell \\ p\bigsqcup \ell {⊑}_{\mathsf{sec}}\mathrm{\Gamma }(x)\end{array}}{\mathrm{\Gamma }{⊢}_p^{\mathsf{IF}}x:=e}\mathrm{IF}-\mathrm{Assign}\frac{\begin{array}{c}\mathrm{\Gamma }{⊢}_p^{\mathsf{IF}}{c}_1\\ \mathrm{\Gamma }{⊢}_p^{\mathsf{IF}}{c}_2\end{array}}{\mathrm{\Gamma }{⊢}_p^{\mathsf{IF}}{c}_1;c_2}\mathrm{IF}-\mathrm{Seq}$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢b:\ell \\ \mathrm{\Gamma }{⊢}_{p\bigsqcup \ell }^{\mathsf{IF}}{c}_1\\ \mathrm{\Gamma }{⊢}_{p\bigsqcup \ell }^{\mathsf{IF}}{c}_2\end{array}}{\mathrm{\Gamma }{⊢}_p^{\mathsf{IF}}\mathbf{if}b\mathbf{then}{c}_1\mathbf{else}{c}_2}\mathrm{IF}-\mathrm{If}\frac{\begin{array}{c}\mathrm{\Gamma }⊢b:\ell \\ \mathrm{\Gamma }{⊢}_{p\bigsqcup \ell }^{\mathsf{IF}}c\end{array}}{\mathrm{\Gamma }{⊢}_p^{\mathsf{IF}}\mathbf{while}b\mathbf{do}c}\mathrm{IF}-\mathrm{While}.$$ The skip rule has no premise. In $\mathsf{Leak}$, the branches are checked under $H$, but IF-Assign would require $H{⊑}_{\mathsf{sec}}L$. The rejected derivation pinpoints the implicit flow.

Proof of Lemma 70.2 — Program-counter monotonicity

Proof. Induct on the typing derivation. In IF-Assign, $p\bigsqcup \ell {⊑}_{\mathsf{sec}}{p}^{\prime }\bigsqcup \ell {⊑}_{\mathsf{sec}}\mathrm{\Gamma }(x)$. In IF-If and IF-While, monotonicity of join gives $p\bigsqcup \ell {⊑}_{\mathsf{sec}}{p}^{\prime }\bigsqcup \ell$; apply the induction hypothesis to the premises. Sequence and skip are immediate. ◻

Write $⟨c,s⟩{⟶}_{\mathsf{IF}}⟨c^{\prime },s^{\prime }⟩$ for the deterministic small-step rules in appendix A. A conditional step removes a guard and thereby lowers the dynamic program counter. The preceding lemma supplies exactly the needed weakening.

Proof of Proposition 70.3 — Subject reduction

Proof. By cases on the step. Assignment produces skip. A conditional selects a branch typed at $p\bigsqcup \ell$; since $p{⊑}_{\mathsf{sec}}p\bigsqcup \ell$, apply lemma 70.2. While unfolds to a conditional followed by the loop, whose premises follow from IF-While. Sequence uses the induction hypothesis for its left component and retains the right premise. ◻

Agreement and confinement

Two lemmas divide the proof according to whether observed data are read or written.

Proof of Lemma 70.4 — Expression agreement, or simple security

Proof. Induct on $e$. In the variable case, $\mathrm{\Gamma }(x){⊑}_{\mathsf{sec}}\ell {⊑}_{\mathsf{sec}}o$, so low equivalence gives the equality. Constants agree. For addition, each operand label flows to their join and therefore to $o$; apply both induction hypotheses. Guard evaluation follows from the two expression cases. ◻

Proof of Lemma 70.5 — High-context confinement

Proof. Induct on the evaluation derivation. For assignment to $x$, IF-Assign gives $p{⊑}_{\mathsf{sec}}p\bigsqcup \ell {⊑}_{\mathsf{sec}}\mathrm{\Gamma }(x)$. If $\mathrm{\Gamma }(x){⊑}_{\mathsf{sec}}o$, transitivity would contradict $p\text{⧸}{⊑}_{\mathsf{sec}}o$. Hence no observed variable changes. Sequence composes the two low-equivalences.

For a conditional, each selected branch is typed at $p\bigsqcup \ell$. Since $p{⊑}_{\mathsf{sec}}p\bigsqcup \ell$, that label also fails to flow to $o$; apply the induction hypothesis to the selected branch. The false-loop rule changes no store. In the true-loop rule, apply the induction hypothesis first to the body and then to the recursive loop derivation, and use transitivity of low equivalence. ◻

The original Volpano–Irvine–Smith calculus phrases these facts as simple security, confinement, and a two-store soundness theorem [VIS96]. Its printed syntax-directed system uses command security types rather than our explicit program-counter judgment. The proof above belongs to the book’s stated calculus; the historical theorem is comparison evidence, not an implementation transfer.

Two runs

The central argument is an unwinding proof over two terminating derivations. The low-guard case synchronizes their control choices; the high-guard case allows different choices but confines both.

Proof of Theorem 70.6 — Termination-insensitive noninterference

Proof. Prove the stronger statement for $\mathrm{\Gamma }{⊢}_p^{\mathsf{IF}}c$, by induction on the first evaluation and case analysis on the second.

For $x:=e$, consider an observed target $\mathrm{\Gamma }(x){⊑}_{\mathsf{sec}}o$. IF-Assign gives $p\bigsqcup \ell {⊑}_{\mathsf{sec}}\mathrm{\Gamma }(x)$, hence $\ell {⊑}_{\mathsf{sec}}o$. By lemma 70.4, both assignments store the same integer. Unobserved targets do not affect low equivalence. Sequence applies the induction hypothesis to the first commands and then to the second commands.

For a conditional with guard label $\ell$, there are two cases. If $\ell {⊑}_{\mathsf{sec}}o$, expression agreement makes both guards select the same branch. Apply the induction hypothesis to that branch, whose typing premise is at $p\bigsqcup \ell$. If $\ell \text{⧸}{⊑}_{\mathsf{sec}}o$, then $p\bigsqcup \ell \text{⧸}{⊑}_{\mathsf{sec}}o$. Each run may select a different branch, but lemma 70.5 shows that each selected branch preserves its own initial low store. Transitivity through $s_1{\approx }_{\mathrm{\Gamma }}^o{s}_2$ relates the results.

For while with a low guard, expression agreement synchronizes zero iterations or one iteration. In the latter case, apply the induction hypothesis to the body and then to the two residual loop derivations. For a high guard, the whole terminating loop is confined: every body is typed at $p\bigsqcup \ell \text{⧸}{⊑}_{\mathsf{sec}}o$, so each finite iteration preserves its run’s low projection. The runs may execute different numbers of iterations; their final low projections still equal their respective initial ones. Skip is immediate. Instantiate the stronger statement with $p=\mathrm{\perp }$. ◻

The theorem deliberately assumes that both evaluations terminate. A program may loop exactly when $h=0$; an observer who can detect termination learns a secret bit even though no low store cell changes. That is a termination-sensitive observation and is not covered by theorem 70.6.

A complete password calculation

Let $\mathrm{\Gamma }(pwd)=\mathrm{\Gamma }(guess)=\mathrm{\Gamma }(audit)=H$ and $\mathrm{\Gamma }(status)=L$. Consider $$\begin{array}{}\text{(}\mathsf{PasswordAudit}\text{)}& \begin{array}{l}\mathbf{if}pwd=guess\mathbf{then}audit:=1\mathbf{else}audit:=0;\\ status:=1.\end{array}\end{array}$$ The guard has label $H$. Both branch assignments satisfy $H\bigsqcup L=H{⊑}_{\mathsf{sec}}H=\mathrm{\Gamma }(audit)$. The final assignment is checked after the conditional, at program counter $\mathrm{\perp }$, so $\mathrm{\perp }\bigsqcup \mathrm{\perp }{⊑}_{\mathsf{sec}}L$. For any two initial stores agreeing on $status$, the branches may disagree on $audit$, but confinement preserves the low projection; both final assignments then write $1$ to $status$. Thus the complete two-run result is $$s_1{\approx }_{\mathrm{\Gamma }}^L{s}_2⟹s_1^{\prime }[status\mapsto 1]{\approx }_{\mathrm{\Gamma }}^L{s}_2^{\prime }[status\mapsto 1].$$ Moving $status:=1$ into only the successful branch would make the program rejected and genuinely leaking when the initial status differs from $1$.

The checker as a finite abstract interpretation

Only after fixing the two-run semantics can we compare the type checker to an analysis. For a finite set of variables, abstract an expression to the join of labels of variables it reads. Abstract a command at program point $p$ to the predicate that every assignment $x:=e$ on a control path satisfies $p\bigsqcup {\ell }_e{⊑}_{\mathsf{sec}}\mathrm{\Gamma }(x)$, joining the guard label into $p$ below conditionals and loop bodies. Structural recursion computes this finite predicate; IF-Assign, IF-If, and IF-While are exactly its local transfer conditions.

Soundness of this analysis is theorem 70.6, not merely termination of the checker. It is incomplete: the constant-branch program $$\mathbf{if}h=0\mathbf{then}l:=0\mathbf{else}l:=0$$ is noninterfering but rejected because the abstraction retains the high control dependency and does not prove equality of branch results. The more flow- and path-sensitive analysis of Li and Zhang and the ownership-oriented Flowistry system refine different components of this abstraction [LZ17, CPAH22]. Neither paper’s theorem transfers to this fixed-variable calculus without an explicit translation.

A bounded DCC comparison

The Dependency Core Calculus protects a value at label $\ell$ with a type $T_{\ell }A$. This is a separate, functional theorem card. It does not replace the imperative two-run proof.

Algehed and Bernardy first prove a shallow relational-parametricity theorem. For their shallow DCC module $dcc$, a type $A$, observer $\hat{\ell }$, and protected label $\ell \text{⧸}{⊑}_{\mathsf{sec}}\hat{\ell }$, every $$f:(dcc:\mathsf{DCC})\to (Tdcc\ell A)\to (Tdcc\hat{\ell }\mathsf{Bool})$$ returns equal results on any two protected inputs. This is their Theorem 3.

Their Definition 4 interprets deep DCC types and terms in the shallow module. Theorem 5 says the translation preserves typing. Theorem 6 says one deep DCC step translates to definitional equality; its bind-return case assumes the right-unit law for the selected DCC module. Strong normalization and confluence then reflect equality at protected Boolean values.

Proof of Theorem 70.7 — Original-DCC noninterference

Proof. By translation type preservation, $[[e]]$ has the shallow type needed by Theorem 3. Apply that theorem to $[[a_0]]$ and $[[a_1]]$: $$[[e]]({\mathsf{return}}_{\ell }[[a_0]])\equiv [[e]]({\mathsf{return}}_{\ell }[[a_1]]).$$ Definition 4 identifies these terms with the translations of the two deep applications. Theorem 6 carries each deep reduction to definitional equality. Strong normalization and confluence put the closed protected Booleans in canonical return forms; the Boolean reflection corollary makes their deep normal forms equal. One beta expansion on each side yields the displayed equation. This is precisely the route through Theorems 3, 5, and 6 used to derive Algehed–Bernardy Theorem 8 [AB19]. ◻

The pinned Agda fixture exposes its assumptions rather than hiding them: lattice structure is postulated in Definitions.agda; function extensionality, strong normalization of deep DCC, a separating observer, and shallow noninterference appear as named postulates in Translation.agda. The artifact is hole-free at its pinned commit, but the local environment used for this edition has no Agda executable, so Appendix E records hashes and a static hole scan rather than claiming a fresh typecheck.

This comparison covers the original DCC Boolean-observation theorem only. It does not establish termination-sensitive security, declassification, term-sensitive relations, quantitative leakage, or results for other DCC variants. The Haskell adaptation in the paper explicitly remains termination-insensitive because partiality exposes a termination channel.

Chapter seminar

The Kappa companion at artifacts/ch70-tini-checker/ implements the two-point instance, the syntax-directed checker, a fuel-bounded evaluator, and finite two-run tests. The finite enumeration tests the implementation; the proof of theorem 70.6 quantifies over every terminating derivation.

The principal result is termination-insensitive two-run noninterference for a sequential, deterministic, fixed-label store language. Concurrency, declassification, probabilistic observations, quantitative leakage, and termination-sensitive security require different observations and proof relations; they are not variants silently covered by the theorem above.