FlowNotation: An Annotation System for Statically Enforcing Information Flow Policies in C

Programmers often need to enforce high-level policies on their cryptographic applications written in C; for instance, that private data is not sent over public channels, trusted data is not modified by untrusted functions, and that the ordering of protocol steps is maintained. These secrecy, integrity, and sequencing policies can be cumbersome to check with existing general-purpose tools. We have developed a novel means of specifying and checking these policies that allows for a much lighter-weight approach than previous tools; requiring less work from programmers. Further, we have modeled our policy annotations as an information flow type system and proved a noninterference guarantee. We embed the policy annotations in C's type system via a source-to-source translation and leverage existing C type checkers to enforce our policies, achieving high performance and scalability. We show through case studies of cryptographic libraries from both industry and recent literature that our work expresses detailed policies for large bodies of C code with little annotation burden, and finds subtle implementation bugs.