Toward Automated Information-Flow Integrity Verification for Security-Critical Applications

We provide a largely automated system for verifying Clark-Wilson interprocess information-flow integrity. Information-flow integrity properties are essential to isolate trusted processes from untrusted ones, but system misconfiguration can easily create insecure dependences. For example, an untrusted user process may be able to write to sshd config via a cron script. A useful notion of integrity is the Clark-Wilson integrity model [7], which allows trusted processes to accept necessary untrusted inputs (e.g., network data or print jobs) via filtering interfaces that sanitize the data. However, Clark-Wilson has the requirement that programs undergo formal semantic verification; in practice, this kind of burden has meant that no information-flow integrity property is verified on most widely-used systems. We define a weaker version of Clark-Wilson integrity, called CW-Lite, which has the same interprocess information-flow guarantees, but which requires less filtering, only small changes to existing applications, and which we can check using automated tools. We modify the SELinux user library and kernel module in order to support CW-Lite integrity verification and develop new software tools to aid developers in finding and enabling filtering interfaces. Using our toolset, we found and fixed several integrity-violating configuration errors in the default SELinux policies for OpenSSH and vsftpd.