Uncovering Information Flow Policy Violations in C Programs

TL;DR

This paper introduces a lightweight, type-system-based method for detecting information flow policy violations in C programs, especially cryptographic applications, ensuring security policies are adhered to efficiently.

Contribution

It presents a novel source-to-source translation approach embedding policies into C's type system, enabling scalable and precise violation detection with formal guarantees.

Findings

Successfully applied to cryptographic libraries and applications

Able to express detailed policies for large codebases

Detected subtle policy violations in real-world code

Abstract

Programmers of cryptographic applications written in C need to avoid common mistakes such as sending private data over public channels, modifying trusted data with untrusted functions, or improperly ordering protocol steps. 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 uncovering violations of these policies that allows for a much lighter-weight approach than previous tools. We embed the policy annotations in C's type system via a source-to-source translation and leverage existing C compilers to check for policy violations, achieving high performance and scalability. We show through case studies of recent cryptographic libraries and applications that our work is able to express detailed policies for large bodies of C code and can find subtle policy violations. To gain formal understanding of our policy annotations, we show formal connections between the policy annotations and an information flow type system and prove a noninterference guarantee.