Person:

Chong, Stephen

We explore the inference of expressive human-readable declassification policies as a step towards providing practical tools and techniques for strong language-based information security. Security-type systems can enforce expressive information-security policies, but can require enormous programmer effort before any security benefit is realized. To reduce the burden on the programmer, we focus on inference of expressive yet intuitive information-security policies from programs with few programmer annotations. We define a novel security policy language that can express what information a program may release, under what conditions (or, when) such release may occur, and which procedures are involved with the release (or, where in the code the release occur). We describe a dataflow analysis for precisely inferring these policies, and build a tool that instantiates this analysis for the Java programming language. We validate the policies, analysis, and our implementation by applying the tool to a collection of simple Java programs.

Program progress (or termination) is a covert channel that may leak sensitive information. To control information leakage on this channel, semantic definitions of security should be progress sensitive and enforcement mechanisms should restrict the channel's capacity. However, most state-of-the-art language-based information-flow mechanisms are progress insensitive---allowing arbitrary information leakage through this channel---and current progress-sensitive enforcement techniques are overly restrictive. We propose a type system and instrumented semantics that together enforce progress-sensitive security more precisely than existing approaches. Our system is permissive in that it is able to accept programs in which the termination behavior depends only on low-security (e.g., public or trusted) information. Our system is parameterized on a termination oracle, and controls the progress channel precisely, modulo the ability of the oracle to determine the termination behavior of a program based on low-security information. We have instantiated the oracle for a simple imperative language with a logical abstract interpretation that uses an SMT solver to synthesize linear rank functions. In addition, we extend the system to permit controlled leakage through the progress channel, with the leakage bound by an explicit budget. We empirically analyze progress channels in existing Jif code. Our evaluation suggests that security-critical programs appear to satisfy progress-sensitive security.