The Agda Development of LambdaIFCStar

• Agda 2.6.4
• Agda standard library v1.7.3 (0817da6)
• The Abstract Binding Trees library
• GNU Make

• GHC with MAlonzo

• XeLaTeX and latexmk
• GraphViz (specifically, dot)
• Dot2TeX
• Zsh (for running plotting scripts)

• Common.SecurityLabels: Definitions of security labels as well as predicates, relations and operators on security labels.
• Common.Types: Definitions of (security) types as well as predicates, relations and operators on types.
• Common.BlameLabels: This module defines blame labels, which are identifiers of casts. In case a cast fails, it raises a cast error, called blame, that contains its blame label. In this way, the programmer knows which cast is causing the problem.
• Common.TypeBasedCast: This module defines type-based casts between two security types. In particular, \(\lambda_{\mathtt{SEC}}^{c}\) uses type-based casts as its cast representation.
• Common.Coercions: This modules defines the coercion-based cast representation used by \(\lambda_{\mathtt{IFC}}^{c}\). In particular, it defines the security coercions on values of \(\lambda_{\mathtt{IFC}}^{c}\).

• Memory.Addr: Definition of memory addresses.
• Memory.Heap: Definition and helper methods of the split-heap model, where low and high addresses are indexed separately. For example, heap lookup has the form \(\mu(\ell, n) = V\), where \(\ell\) is the security level of the memory cell, \(n\) is the index of the part of the memory where all cells are labeled \(\ell\), and \(V\) is the value stored at \((\ell, n)\).
• Memory.HeapTyping: Definition of heap well-typedness. It is defined point-wise. The typing judgment has the form \(\Sigma \vdash \mu\), where \(\Sigma\) is the heap context and \(\mu\) is the (well-typed) heap.

• Surface.SurfaceSyntax: The syntax definition of \(\lambda_{\mathtt{SEC}}^\star\). It uses the Abstract Binding Tree (ABT) library. For example, the term of function application has the signature sig (op-app p) = ■ ∷ ■ ∷ [], because it contains two sub-terms and introduces no binder. On the other hand, the term for \(\lambda\) abstraction has the signature sig (op-lam pc A ℓ) = (ν ■) ∷ [], because there is one free variable in the body of a \(\lambda\) (indicated by (ν ■)).
• Surface.SurfaceTyping: The typing rules for \(\lambda_{\mathtt{SEC}}^\star\). The typing judgment takes the form \(\Gamma ; g \vdash M : A\), where \(\Gamma\) is the typing context, \(g\) is the static program counter (PC) label, \(M\) is a surface language program, and \(A\) is the security type that \(M\) is typed at.

• CC.CCSyntax: The syntax definition of \(\lambda_{\mathtt{SEC}}^{c}\). Again, the module uses the ABT library. There are a few terms that arise during runtime, including memory addresses, casts, PC casts (cast-pc), protection terms (prot), and runtime errors (error). The opaque term (●) is used in the erasure-based noninterference proof.
• CC.CCTyping: The typing judgment is of form \(\Gamma ; \Sigma ; g ; \ell \vdash M : A\). It contains 6 field: \(\Gamma\) is the typing context; \(\Sigma\) is the heap context; \(g\) is the static PC, which can be viewed as the compile-time approximation of the runtime PC; \(\ell\) is the dynamic (runtime) PC; \(M\) is a \(\lambda_{\mathtt{SEC}}^{c}\) term; \(A\) is the type of \(M\).
• CC.HeapTyping: Lemmas about heap well-typedness for \(\lambda_{\mathtt{SEC}}^{c}\). These lemmas are used in the type safety proof.
• CC.Values: The definition of values in \(\lambda_{\mathtt{SEC}}^{c}\). A value can be (1) a constant (2) an address (3) a \(\lambda\) abstraction or (4) a value wrapped with an irreducible (Inert) cast. The opaque term is also a value in the semantics of erased \(\lambda_{\mathtt{SEC}}^{c}\). In this module, there are canonical-form lemmas for constants, functions, and memory addresses. For example, a value of function type must be either a \(\lambda\) or a function proxy (a \(\lambda\) wrapped with at least one inert function cast).
• CC.Reduction: The operational semantics for \(\lambda_{\mathtt{SEC}}^{c}\). The relation \(M \mid \mu \mid \ell \longrightarrow N \mid \mu'\) says that \(\lambda_{\mathtt{SEC}}^{c}\) term \(M\) reduces with heap \(\mu\) under PC label \(\ell\) (by one step) to term \(N\) and heap \(\mu'\).
  • The rule cast turns to the ApplyCast relation defined in the following module:
    • CC.ApplyCast: The cast-application relation has the form \(\mathtt{ApplyCast}\;V , c \leadsto M\), where \(V\) is a value and \(c\) is the cast to apply; \(M\) can be either a value, or a cast error (blame) if the cast application fails.
  • The rule fun-cast, assign?-cast, and assign-cast turn to the proxy-elimination helpers that are defined in the following module:
    • CC.ProxyElimination: The module defines two helper functions: elim-fun-proxy works on a function proxy and elim-ref-proxy works on a reference proxy. The helpers check the well-formedness of the outermost inert cast, generate proper casts that preserve types if well-formed and signal errors if ill-formed.
• CC.Interp: A stepper that replies on the progress proof to generate a reduction sequence of \(k\) steps for a well-typed \(\lambda_{\mathtt{SEC}}^{c}\) term.
• CC.Compile: Compilation from \(\lambda_{\mathtt{SEC}}^\star\) to \(\lambda_{\mathtt{SEC}}^{c}\). The module also contains a proof that this compilation function preserves types (compilation-preserves-type).

The noninterference proof of \(\lambda_{\mathtt{SEC}}^{c}\) is erasure-based. It uses the following auxiliary definitions:

• CC.BigStep: The big-step semantics for \(\lambda_{\mathtt{SEC}}^{c}\). It is a direct mechanical translation from the semantics in CC.Reduction.
• CC.Erasure: Definition of the erasure functions for terms (erase) and heaps (erase-μ) in \(\lambda_{\mathtt{SEC}}^{c}\). Note that the memory cells of high security are completely erased, because the values read from those cells are always of high security and thus appear to be opaque from a low-observer's point of view.
• CC.BigStepErased: The big-step semantics for erased \(\lambda_{\mathtt{SEC}}^{c}\).

• Surface2.Syntax: The syntax of \(\lambda_{\mathtt{IFC}}^\star\). The most noteworthy difference from \(\lambda_{\mathtt{SEC}}^\star\) is that in \(\lambda_{\mathtt{IFC}}^\star\), the PC annotation on a \(\lambda\) is treated as a type annotation instead of a value annotation, which means that it is allowed to be \(\star\) in \(\lambda_{\mathtt{IFC}}^\star\) (but not in \(\lambda_{\mathtt{SEC}}^\star\)).
• Surface2.Typing: The typing rules for \(\lambda_{\mathtt{IFC}}^\star\).
• Surface2.Precision: The precision rules for \(\lambda_{\mathtt{IFC}}^\star\). The precision relation is used in the definition and the proof of the gradual guarantee.

This directory contains the definition of and the lemmas about the coercion calculus on security labels.

• CoercionExpr.Coercions: A single coercion on security labels can either be identity (\(\mathbf{id}\)), subtype (\(\uparrow\)), injection from \(\ell\) (\(\ell!\)), or projection to \(\ell\) with blame label \(p\) (\(\ell?^p\)).
• CoercionExpr.CoercionExpr: The syntax, typing, reduction, and normal forms of coercion sequences (formed by sequencing single coercions). We only care about well-typed coercion sequences, so the coercion sequences are intrinsically typed. Coercion sequences strongly normalize (cexpr-sn) and the normalization is deterministic (det-mult), so coercion sequences can be used to model information-flow checks.
• CoercionExpr.SyntacComp: Syntactical composition of coercion sequences. Sequencing and composing coercions model explicit information flow.
• CoercionExpr.Stamping: The stamping operation for coercion sequences. Stamping label \(\ell\) on a coercion sequence in normal form \(\bar{c}\) results in a new coercion sequence in normal form whose security level is promoted by \(\ell\). Stamping models implicit information flow.
• CoercionExpr.SecurityLevel: The \(|\bar{c}|\) operator retrieves the security level from the coercion sequence in normal form \(\bar{c}\).
• CoercionExpr.Precision: The precision relation between two coercion sequences takes the form \(\vdash \bar{c} \sqsubseteq \bar{d}\). The gradual guarantee states that replacing type annotations with \(\star\) (decreasing type precision) should result in the same value for a correctly running program while adding annotations (increasing type precision) may trigger more runtime errors. The precision relation is a syntactical characterization of the runtime behaviors of programs of different type precision.

One key to the proof of the gradual guarantee is that "security is monotonic with respect to precision", which states that if \(\vdash \bar{c} \sqsubseteq \bar{d}\) then \(|\bar{c}| \preccurlyeq |\bar{d}|\).

• LabelExpr.LabelExpr: The syntax, typing, reduction, normal forms, precision, and security of label expressions.
• LabelExpr.Stamping: The stamping operation for label expressions.
• LabelExpr.Security: Lemmas about security level for label expressions.

• CC2.Syntax: As usual, the cast calculus \(\lambda_{\mathtt{IFC}}^{c}\) is a statically-typed language that includes an explicit term for casts. Many of the operators in \(\lambda_{\mathtt{IFC}}^{c}\) have two variants, a "static" one for when the pertinent security label is statically known (such as ref) and the "dynamic" one for when the security label is statically unknown (such as ref?). The operational semantics of the "dynamic" variants involve runtime checking.
• CC2.Typing: The typing judgment is of form \(\Gamma ; \Sigma ; g ; \ell \vdash M \Leftarrow A\). The six fields are of the same meanings as those of \(\lambda_{\mathtt{SEC}}^{c}\). The main difference is that the typing of \(\lambda_{\mathtt{IFC}}^{c}\) stays in checking mode, so the type \(A\) is considered an input of the judgment.
• CC2.HeapTyping: Lemmas about heap well-typedness for \(\lambda_{\mathtt{IFC}}^{c}\). They are similar to those of \(\lambda_{\mathtt{SEC}}^{c}\) because \(\lambda_{\mathtt{IFC}}^{c}\) shares the same heap model as \(\lambda_{\mathtt{SEC}}^{c}\).
• CC2.Values: The definition of values in \(\lambda_{\mathtt{IFC}}^{c}\). A raw value can be (1) a constant (2) an address or (3) a \(\lambda\) abstraction. A value can be either a raw value, or a raw value wrapped with an irreducible cast. A cast is irreducible if its top-level security label coercion is in normal form and the cast is not identity.
• CC2.Reduction: The operational semantics for \(\lambda_{\mathtt{IFC}}^{c}\). Similar to the one of \(\lambda_{\mathtt{SEC}}^{c}\), the relation \(M \mid \mu \mid \ell \longrightarrow N \mid \mu'\) says that \(\lambda_{\mathtt{IFC}}^{c}\) term \(M\) reduces with heap \(\mu\) under PC label \(\ell\) to term \(N\) and heap \(\mu'\).
  • The reduction of PC depends on the operational semantics of label expressions.
  • CC2.CastReduction: The rules for cast are grouped in the relation \(V \langle c \rangle \longrightarrow M\). The relation states that applying the coercion on values \(c\) on value \(V\) results in \(M\). We use this relation in rule cast of \(\lambda_{\mathtt{IFC}}^{c}\).
  • CC2.Stamping: The stamp-val function defines the stamping operation on \(\lambda_{\mathtt{IFC}}^{c}\) values. The lemma stamp-val-value states that stamping a value results in another value and the lemma stamp-val-wt states that stamping preserves types, so the value after stamping is well-typed.
• CC2.Precison: The precision relation of \(\lambda_{\mathtt{IFC}}^{c}\).
• CC2.HeapContextPrecision: The precision between two heap typing contexts has the form \(\Sigma \sqsubseteq_m \Sigma'\) and is defined point-wise.
• CC2.HeapPrecision: The precision relation between two heaps takes the form \(\Sigma ; \Sigma' \vdash \mu \sqsubseteq \mu'\). It is defined point-wise, similar to the definition of heap well-typedness.
• Compile.Compile: The compilation function from \(\lambda_{\mathtt{IFC}}^\star\) to \(\lambda_{\mathtt{IFC}}^{c}\).

This directory contains the formalization of the dynamic extreme for \(\lambda_{\mathtt{SEC}}^\star\) and \(\lambda_{\mathtt{IFC}}^\star\). We call this dynamic IFC language with labeled heap (that is, each memory cell is associated with a security label) \(\lambda_{\mathtt{SEC}}\). \(\lambda_{\mathtt{SEC}}\) is used in Section 11 of the Appendix of Chen and Siek [2024], where noninterference of \(\lambda_{\mathtt{IFC}}^\star\) is proved by simulation between \(\lambda_{\mathtt{IFC}}^{c}\) and \(\lambda_{\mathtt{SEC}}\).

• Dyn.Noninterference: Noninterference (TINI) for \(\lambda_{\mathtt{SEC}}\).