Thomas H. Austin, Cormac Flanagan
11/11/2009 09:00 AM
Computer Science
A key challenge in dynamic information flow analysis is handling implicit flows, where code conditional on a private variable updates a public variable x. The naive approach of upgrading x to private results in x being partially-leaked, where its value contains private data but its label may be either private (on this execution) or public (on an alternative execution where the conditional update was not performed). Prior work proposed the no-sensitive-upgrade check, which handles implicit flows by prohibiting partially-leaked data, but attempts to update a public variable from a private context causes execution to get stuck. To overcome this limitation, we develop a sound yet flexible permissive-upgrade strategy. To prevent information leaks, partially-leaked data is permitted but carefully tracked, and it must be upgraded to private before being used in a conditional test. We present an automatic dynamic analysis technique for inferring these upgrade annotations and inserting them into the program source code. The combination of these techniques allows more programs to run to completion, while still guaranteeing termination-insensitive non-interference in a purely-dynamic manner.
