simpl is a tiny security-typed imperative programming language close to the
one from Sabelfeld and Myers (2003) defined in Imp.agda. simplc is a
compiler from simpl to a little stack-based machine defined in Machine.agda.
The fact that all well-typed simpl programs have the noninterference
property is formalized in Noninterference.agda. In addition to this, we have
formulated a natural notion of noninterference for the machine and have
formalized the proof that the compilation of every well-typed simpl program
results in a noninterferent machine program; this theorem goes under the name
main-theorem and lives in Compiler.agda
- Sabelfeld, A., & Myers, A. C. (2003). Language-based information-flow security. IEEE Journal on selected areas in communications, 21(1), 5-19.
Authors are Ayberk Tosun (@ayberkt) and Alexander Fuhs (@haskell-user).
This development was carried out as the final project for the language-based
security course (TDA602) taught by Andrei Sabelfeld at Chalmers University of
Technology.
We are grateful to Marco Vassena and Andrei Sabelfeld for suggestions and guidance.