Problem
Abstract The last several years have seen a proliferation of static and run- time analysis tools for finding security violations that are caused by explicit information flow in programs. Much of this interest has been caused by the increase in the number of vulnerabilities such as cross-site scripting and SQL injection. In fact, these explicit infor- mation flow vulnerabilities commonly found in Web applications now outnumber vulnerabilities such as buffer overruns common in type-unsafe languages such as C and C++. Tools checking for these vulnerabilities require a specification to operate. In most cases the task of providing such a specification is delegated to the user. More- over, the efficacy of these tools is only as good as the specifica- tion. Unfortunately, writing a comprehensive specification presents a major challenge: parts of the specification are easy to miss, lead- ing to missed vulnerabilities; similarly, incorrect specifications may lead to false positives. This paper proposes MERLIN, a new approach for automati- cally inferring explicit information flow specifications from pro- gram code.
Approach
Such specifications greatly reduce manual labor, and enhance the quality of results, while using tools that check for secu- rity violations caused by explicit information flow. Beginning with a data propagation graph, which represents interprocedural flow of information in the program, MERLIN aims to automatically in- fer an information flow specification. MERLIN models information flow paths in the propagation graph using probabilistic constraints. A na¨ıve modeling requires an exponential number of constraints, one per path in the propagation graph. For scalability, we approx- imate these path constraints using constraints on chosen triples of nodes, resulting in a cubic number of constraints. We characterize this approximation as a probabilistic abstraction, using the theory of probabilistic refinement developed by McIver and Morgan. We solve the resulting system of probabilistic constraints using factor graphs, which are a well-known structure for performing proba- bilistic inference. We experimentally validate the MERLIN approach by applying it to 10 large business-critical Web applications that have been Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page.
Results
To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. PLDI’09, June 15–20, 2009, Dublin, Ireland. Copyright c⃝2009 ACM 978-1-60558-392-1/09/06...$5.00 ∗Partially supported at Kansas State University by NSF grants ITR- 0326577 and CNS-0627748 and by Microsoft Research, Redmond, by way of a sabbatical visit. analyzed with CAT.NET, a state-of-the-art static analysis tool for .NET. We find a total of 167 new confirmed specifications, which result in a total of 322 additional vulnerabilities across the 10 benchmarks. More accurate specifications also reduce the false positive rate: in our experiments, MERLIN-inferred specifications result in 13 false positives being removed; this constitutes a 15% reduction in the CAT.NET false positive rate on these 10 programs. The final false positive rate for CAT.NET after applying MERLIN in our experiments drops to under 1%. Categories and Subject Descriptors D.3.4 [Processors]: Com- pilers; D.4.6 [Operating Systems]: Security and Protection— Information flow controls; D.2.4 [Software/Program Verification]: Statistical methods General Terms Languages, Security, Verification