When: Monday, May 12, 01:30 a.m.- 03:00 a.m.

Where: 3305Newell-Simon Hall

Stephen McCamant, Massachusetts Institute of Technology

SCS Faculty Candidate Talk

Abstract:
I'll describe a new technique for determining how much information about a program's secret inputs is revealed by its public outputs. In contrast to previous techniques based on reachability from secret inputs (tainting), it achieves a more precise quantitative result by computing a maximum flow of information between the inputs and outputs. The technique uses static control-flow regions to soundly account for implicit flows via branches and pointer operations, but operates dynamically by observing one or more program executions and giving numeric flow bounds specific to them (e.g., "17 bits"). The results are a conservative estimate of channel capacity: the amount of information that could be transmitted by an adversary making an arbitrary choice of secret inputs. We've performed case studies on five real C, C++, and Objective C programs, 3 of which had more than 250K lines of code. The tool checked multiple security policies, including one that was violated by a previously unknown bug. (A paper describing this work will appear in PLDI 2008.) I'll also say a bit about how this work relates to themes in my previous research, and point out some future directions.

<< Back