Abstract

Information Flow Analysis (IFA) is an indispensable tool in ascertaining whether programs obey a pre-defined security policy. The policy is typically described as a lattice of privilege levels and the first step towards to IFA is to use annotated types that hold these privilege levels for expressions. For unannotated expressions, the type system represents privilege levels as variables, derives a set of constraints on these variables and checks the satisfiability of these constraints against the policy lattice. In this talk, we discuss bottlenecks for generating and resolving these constraints for the polymorphic lambda calculus and present solutions for mitigating these bottlenecks. We first discuss how the introduction of universal quantification creates a need for constraint simplification – a computationally expensive operation. Then, we discuss how operations on the policy lattice like meet and join operators contribute significantly to computational costs of the resolution process. We highlight the innate relationship between both these issues and the transitive closure of Directed Acyclic Graphs (DAGs). Finally, we present an adaptive approach for both constraint simplification and answering lattice queries. The adaptive nature of our approach ties the computational costs to the incidence of non-tree edges in the flow-constraint-graph / security-lattice. Therefore, our approach seamlessly scales the performance graph between the best reported algorithms for trees and those for DAGs thereby achieving near-linear time complexity for sparse flow-constraint-graphs / security-lattices as opposed to traditional approaches which have cubic time complexity.