Practical End-to-End Analysis of Information Flow Security Policies

C and JavaScript are widely-used languages for writing security-sensitive software, despite their inherent security issues. The widespread deployment of these languages makes them attractive targets for attackers; vulnerabilities in C programs remain common and recent years have seen a surge in attacks that target web page scripts and Node.js packages. Several types of vulnerabilities in these programs can be expressed as violations of information flow policies that specify the confidentiality and integrity of program data, or required sequences of declassification and endorsement. Prior work has proposed analysis techniques for C and JavaScript to check these policies, but a practical end-to-end analysis pipeline, applicable to real programs, requires additional solutions that enable precise, scalable analysis that minimizes manual effort. 

In this thesis, we develop a set of information flow policy-based modeling and analysis methodologies for checking security-sensitive software, including C cryptographic libraries, server-side Node.js applications, and website scripts. We build tools that help analysts specify and precisely check security policies on their software, without requiring manually-crafted test drivers, with reduced manual tuning to ensure analysis tractability, and with lowered effort for manual triage and confirmation of reported potential vulnerabilities. We first develop techniques to apply information flow policy checking scalably via type systems for C and via dynamic taint analysis for JavaScript. We then demonstrate how dynamic taint analysis can be used in combination with dynamic symbolic execution to improve analysis comprehensiveness. Finally, we show how information flow traces can be leveraged to synthesize concrete exploits that can then be used to automatically confirm potential vulnerabilities in real programs.