Composing Polymorphic Information Flow Systems with Reference Immutability

Information flow type systems, such as EnerJ (a type system for energy efficiency), and integrity and confidentiality, are unsound if subtyping for references is allowed because of the presence of mutable references. The standard approach is to disallow subtyping for references, or in other words, replace subtyping constraints with equality constraints. Unfortunately, this often leads to imprecision, causing the type system to reject valid programs. We observe that subtyping is safe when the left-hand-side of the assignment is immutable. Therefore, we compose information flow systems with reference immutability, which allows for limited subtyping for references. We infer types with the standard approach (i.e., no subtyping for references), and with the composition approach on 13 Java web applications. The composition approach achieves at least 20% precision improvement over the standard approach.