The ubiquity of sensitive information in today’s computer systems combined with the increasing connectivity of these systems require security controls to ensure information is not leaked to unauthorized locations. To this end, information flow security mechanisms enforce application-level security by tracking and controlling the dissemination of information through programs. Though much foundational work has been done in this area, current systems are hampered by a high learning curve, many code annotations, poorly defined security policies, and imprecision in the analysis.
In this talk, I will describe a static information flow type inference system for Java. The focus of the system is on specifying security policies of IO channels only, making code annotations unnecessary, as the type system automatically infers all of the security labels throughout the code. The type system includes a high degree of polymorphism, necessary to allow classes to be used in multiple security contexts, and to properly distinguish the security policies of different IO channels. Top-level policy specifications allow the policy to be clearly defined and visible in the API. I will conclude by describing how the type system is proved correct with a noninterference result: that high security data is not visible to a low security observer.