Co-Inflow: Coarse-grained Information Flow Control for Java-like Languages

Abstract

Coarse-grained dynamic information-flow control (IFC) is a good match for imperative object-oriented programming languages such as Java. Java language abstractions align well with coarse-grained IFC concepts, and so Java can be cleanly extended with coarse-grained dynamic IFC without requiring significantly different design patterns or excessive security annotations, and without excessive performance overhead. We present Co-Inflow: an extension of Java with coarse-grained dynamic IFC. By careful design choices and defaults, a programmer typically needs to add very few annotations to a Java program to convert it to a Co-Inflow program with relatively good precision. Additional annotations can improve precision. We achieve this trade-off between precision and annotation burden by instantiating and specializing recent advances in coarse-grained IFC for a Java-like setting, and by using opaque labeled values: a restriction of labeled values that the Co-Inflow runtime automatically and securely creates and uses. We have captured the essence of Co-Inflow in a middle-weight imperative calculus, and proven that it provides a termination-insensitive non-interference security guarantee. We have a prototype implementation of Co-Inflow and use it to evaluate the precision, usability, and potential performance of Co-Inflow.