CRII: SaTC: Repairing Code from Inferred Specifications of Information Flow Security

Carnegie Mellon University, Pittsburgh PA

Investigators

Abstract

As more software computes using sensitive user data, it increasingly important to ensure that data flows only where it is permitted. Protecting sensitive data often involves reasoning about how sensitive values and policies are interacting with functionality across the program. The need to reason across the code base makes it difficult not only for programmers to implement computations using sensitive data, but also to make existing code adhere to new policies. This project investigates an approach for (1) inferring information flow policies from potentially buggy code and (2) performing program repair to ensure programs adhere to the specified policies. Not only does this approach help identify potential misuses of sensitive information, but it also helps prevent leaks in code from well-intentioned programmers, and provides a mechanism for modifying arbitrary code to satisfy a given policy. Enabling this approach is a policy-agnostic semantic model, developed to disentangle information flow concerns from other functionality. Using policy-agnostic programming, the programmer may implement information flow policies by specifying them alongside sensitive data values, rather than implementing them as conditional access checks across the program. Prior work on Lifty supports policy-agnostic programming using type-driven repair, based on program synthesis for liquid types, which are value-dependent refinement types. Previously, programs could only benefit from policy-agnostic programming if the policies are known, but this is not always the case with existing code. We propose an approach for inferring liquid types from potentially buggy code. The inferred types now make it possible to perform sound repair. Representing the inferred policies as liquid types also facilitates modification of the policies. The proposal describes both a strategy for inferring a set of possible policies, and a solution for choosing which policies to use for repair.