Secure Flow Typing

Abstract

Some of the most promising work in the area of enforcing secure information flow in programs is based on static analyses of source code. However, as yet, these efforts have not had much impact in practice. We present a new approach to analyzing programs statically for secrecy and integrity flow violations. The analysis is characterized as a form of type inference in a secure flow type system. The type system provides a uniform frame work for traditional type checking of programs and information flow control Type correct programs have principal types that characterize how they can be called securely. Applications of the type system include flow analysis of legacy code as well as code written in newly emerging Web languages like Java (tm).