Tue 16 Jun 2015 14:25 - 14:50 at PLDI Main BLUE (Portland 254-255) - Analysis Chair(s): Yannis Smaragdakis

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 335k line Java application takes two minutes, and checking each of our policies on that PDG takes under 15 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.

Tue 16 Jun

Displayed time zone: Tijuana, Baja California change

14:00 - 15:40
AnalysisResearch Papers at PLDI Main BLUE (Portland 254-255)
Chair(s): Yannis Smaragdakis University of Athens
14:00
25m
Talk
DAG Inlining: A Decision Procedure for Reachability-Modulo-Theories in Hierarchical Programs
Research Papers
Akash Lal Microsoft Research India, Shaz Qadeer Microsoft Research
Media Attached File Attached
14:25
25m
Talk
Exploring and Enforcing Security Guarantees via Program Dependence Graphs
Research Papers
Andrew Johnson Harvard University, Lucas Waye Harvard University, Scott Moore Harvard University, Stephen Chong Harvard University
Media Attached
14:50
25m
Talk
Making Numerical Program Analysis Fast
Research Papers
Gagandeep Singh ETH Zurich, Switzerland, Markus Püschel ETH Zurich, Martin Vechev ETH Zurich
Media Attached
15:15
25m
Talk
Tree Dependence Analysis
Research Papers
Yusheng Weijiang Purdue University, Shruthi Balakrishna Purdue University, Jianqiao Liu Purdue University, Milind Kulkarni Purdue University
Media Attached