About

$\lambda_{\mathtt{SEC}}^\star$ is an experimental gradual security-typed programming language. It provides programmers with the freedom of choice between runtime versus compile-time information-flow (IFC) enforcement. The Agda development of $\lambda_{\mathtt{SEC}}^\star$ comes with machine-checked proofs of various meta-theoretical results.

Building and Testing

We compile $\lambda_{\mathtt{SEC}}^\star$ into an intermediate representation ("cast calculus"), namely, $\lambda_{\mathtt{SEC}}^\Rightarrow$. We define an operational semantics for $\lambda_{\mathtt{SEC}}^\star$ that includes blame tracking.

You can check proofs and explore examples by following the steps:

Prerequisites

Software dependencies for checking proofs:

• Agda 2.6.4
• Standard library v1.7.3 (0817da6)
• Abstract binding trees
• GNU Make

Additional dependencies for running demo:

• GHC with working MAlonzo

[Optional] Additional dependencies for drawing simulation diagrams:

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

Building

• To build everything, simply run make at the top level of this repository.

  • This will build the proofs, the runnable demo, and a simulation explorer.

• [Optional] To check the proofs only, run make proofs. The type-checker of Agda makes sure everything is correct.

• [Optional] To build the simulator only, run make sim.

Running Demo

To get a taste of $\lambda_{\mathtt{SEC}}^\star$ running in action, build everything first and then run bin/RunDemo.

Project Code Structure (selected)

All Agda source files are located in the src directory and end with .agda.

There are three top-level modules: one contains all type-check-able proofs; the other two compile to executable binaries:

• Proofs: sources the proofs of important meta-theoretical results in the following modules:

  • CC.TypeSafety: $\lambda_{\mathtt{SEC}}^\Rightarrow$ is type safe by satisfying progress and preservation.
    • CC2.Progress and CC2.Preservation: the CC2 version
  • CC.BigStepPreservation: Big-step evaluation to value is type safe.
  • CC.BigStepErasedDeterministic: Big-step evaluation of erased $\lambda_{\mathtt{SEC}}^\Rightarrow$ is deterministic.
  • CC.Noninterference: Termination-insensitive noninterference (TINI), the main security guarantee.
  • CC.Compile: Compilation from $\lambda_{\mathtt{SEC}}^\star$ to $\lambda_{\mathtt{SEC}}^\Rightarrow$ preserves types.
  • Simulation.Simulation the main simulation lemma for DGG, driven by more precise side
    • Simulation.CatchUp the catch-up lemma, where less precise is catching up to a more precise value

• RunDemo: runs the stepper on $\lambda_{\mathtt{SEC}}^\star$ programs in the following modules and pretty-prints their reduction sequences to console:

  • ExamplePrograms.Demo.Example1: shows that $\lambda_{\mathtt{SEC}}^\star$ indeed facilitates both compile-time (static) and runtime (dynamic) information-flow control. If a $\lambda_{\mathtt{SEC}}^\star$ program is fully statically-typed, our type system alone guarantees security. Transition between static and dynamic is controlled by the precision of type annotations given by the programmer.
  • ExamplePrograms.Demo.Example2: establishes the intuition that even if the programmer opts for runtime enforcement, $\lambda_{\mathtt{SEC}}^\star$ still guards against any possible information leakage.
  • ExamplePrograms.Demo.Example3: shows that moving type annotations to be less precise (or more dynamic) does not change the runtime behavior of a program.

• RunSimulation: simulates between $\lambda_{\mathtt{SEC}}^\Rightarrow$ terms of different precision.

Important technical definitions:

• Common.SecurityLabels and Common.Types: defines security labels and security types.

• Common.TypeBasedCast: defines type-based casts between security types.

• Surface: contains the statics of the surface language.

  • Surface.SurfaceSyntax: defines the syntax of $\lambda_{\mathtt{SEC}}^\star$.
  • Surface.SurfaceTyping: defines the typing rules of $\lambda_{\mathtt{SEC}}^\star$.

• Memory: the memory model of $\lambda_{\mathtt{SEC}}^\star$.

• CC: contains one variant of the cast calculus (CC) which has vigilant (sticky) but non-coercive casts

  • CC.CCSyntax: presents the syntax of $\lambda_{\mathtt{SEC}}^\Rightarrow$.
  • CC.CCTyping: the typing rules of $\lambda_{\mathtt{SEC}}^\Rightarrow$.
  • CC.HeapTyping: defines well-typed heap.
  • CC.Values: definition of values.
  • CC.Compile: defines type-preserving compilation from $\lambda_{\mathtt{SEC}}^\star$ to $\lambda_{\mathtt{SEC}}^\Rightarrow$.
  • CC.Reduction: small-step reduction semantics of $\lambda_{\mathtt{SEC}}^\Rightarrow$.
    • CC.ApplyCast: application rules for active casts.
    • CC.ProxyElimination: elimination rules for function and reference proxies.
  • CC.Bigstep: big-step semantics to values.
  • CC.Erasure: defines the erasure function.
  • CC.BigStepErased: big-step evaluation of erased $\lambda_{\mathtt{SEC}}^\Rightarrow$.
  • CC.Interp: a stepper that produces reduction sequences.

• CC2: contains the second variant of the cast calculus (CC2) which has vigilant (sticky) and coercive casts

  • CC2.Syntax
  • CC2.Typing
  • CC2.HeapTyping
  • CC2.Values
  • CC2.Reduction: small-step reduction semantics of $\lambda_{\mathtt{SEC}}^\Rightarrow$ variant 2
    • CC2.CastReduction: cast reduction rules
    • CC2.Stamping: value stamping (stamp-val) and value injective stamping (stamp-val!)
    • CC2.MultiStep: multi-step reduction, reflexive transitive closure of single-step reductions
  • CC2.Precision the precision relation between CC2 terms

• PrettyPrinter

  • PrettyPrinter.Console: prints to console (tty).
  • PrettyPrinter.GraphViz: prints in GraphViz visualizer format.