Exploring and Enforcing Application Security Guarantees vis Program Dependence

Abstract

We present Pidgin, a program analysis and understanding tool that allows developers to explore the information flows that exist in programs and specify and enforce security policies that restrict these information flows. Pidgin uses program-dependence graphs (PDGs) to precisely capture the information flows within a program. PDGs can be queried using a custom query language to explore and describe information flows in programs. A developer can specify strong information security policies by asserting that specific queries return no results (i.e., asserting the absence of certain information flows in the program). To check whether a program satisfies a security policy, a developer can simply evaluate the query against a program’s dependence graph. The query language is expressive, supporting a large class of precise, application-specific security guarantees. Pidgin can be used to explore information security guarantees in legacy programs, or to support the specification, enforcement, and modification of information security requirements during program development. We describe the design and implementation of Pidgin and report on using Pidgin both to explore security guarantees in existing open-source applications, and to specify and enforce security guarantees during application development.