Type systems are not just for types they can ensure that secret data does not leak explicitly, implicitly, and even through covert channels. This repository defines a simple language that does it and uses GADTs to make data leakage a compile time error.
All the source code is in src/VolpanoSmith.hs.
The type system is based on Chapter 9 of "Concrete Semantics" by Tobis Nipkow and Gerwin Klein. This in turn is based on the following papers:
- A sound type system for secure flow analysis by Volpano, Irvine, and Smith
- Eliminating covert flows with minimum typings by Volpano and Smith