We compile
You can check proofs and explore examples by following the steps:
- Agda
2.6.4
- Standard library
v1.7.3 (0817da6)
- Abstract binding trees
- GNU Make
- GHC with working MAlonzo
-
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
.
To get a taste of bin/RunDemo
.
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
andCC2.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
andCommon.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 castsCC2.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.Console
: prints to console (tty). -
PrettyPrinter.GraphViz
: prints in GraphViz visualizer format.
-