Exploring and enforcing security guarantees via program dependence graphs
Authors:
Open Access
- 3 June 2015
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in ACM SIGPLAN Notices
- Vol. 50 (6) , 291-302
Abstract
We present PIDGIN, a program analysis and understanding tool that enables the specification and enforcement of precise application-specific information security guarantees. PIDGIN also allows developers to interactively explore the information flows in their applications to develop policies and investigate counter-examples. PIDGIN combines program dependence graphs (PDGs), which precisely capture the information flows in a whole application, with a custom PDG query language. Queries express properties about the paths in the PDG; because paths in the PDG correspond to information flows in the application, queries can be used to specify global security policies. PIDGIN is scalable. Generating a PDG for a 330k line Java application takes 90 seconds, and checking a policy on that PDG takes under 14 seconds. The query language is expressive, supporting a large class of precise, application-specific security guarantees. Policies are separate from the code and do not interfere with testing or development, and can be used for security regression testing. We describe the design and implementation of PIDGIN and report on using it: (1) to explore information security guarantees in legacy programs; (2) to develop and modify security policies concurrently with application development; and (3) to develop policies based on known vulnerabilities.Keywords
Funding Information
- National Science Foundation (1054172,1421770)
- U.S. Air Force (FA8721-05-C-0002)
This publication has 49 references indexed in Scilit:
- Dependent Type Theory for Verification of Information Flow and Access Control PoliciesACM Transactions on Programming Languages and Systems, 2013
- Modelling declassification policies using abstract domain completenessMathematical Structures in Computer Science, 2011
- TaintEraserACM SIGOPS Operating Systems Review, 2011
- Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphsInternational Journal of Information Security, 2009
- Language-based information-flow securityIEEE Journal on Selected Areas in Communications, 2003
- Efficiently computing static single assignment form and the control dependence graphACM Transactions on Programming Languages and Systems, 1991
- Interprocedural slicing using dependence graphsACM SIGPLAN Notices, 1988
- The program dependence graph and its use in optimizationACM Transactions on Programming Languages and Systems, 1987
- Information-flow and data-flow analysis of while-programsACM Transactions on Programming Languages and Systems, 1985
- A lattice model of secure information flowCommunications of the ACM, 1976