Fine: A Type-Preserving Compiler for End-to-End Security Verification

This is a source release of the Fine compiler and several example programs. The Fine compiler implements a type system that enables the enforcement of rich, stateful authorization and information-flow policies to be verified. Our compilation technique produces verifiable target code in a language called DCIL, an extension of CIL, the language of the .NET runtime. Code consumers can check DCIL target programs using a syntactic byte-code verifier to establish the security of the code.