Modular and Constraint-Based Information Flow Inference for an Object-Oriented Language

Abstract. This paper addresses the problem of checking programs written in an object-oriented language to ensure that they satisfy the information flow policies, confidentiality and integrity. Policy is specified using security types. An algorithm that infers such security types in a modular manner is presented. The specification of the algorithm involves inference for libraries. Library classes and methods maybe parameterized by security levels. It is shown how modular inference is achieved in the presence of method inheritance and override. Soundness and completeness theorems for the inference algorithm are given.

• Type: Conference
• Year: 2004
• Where: SAS
• Authors: Qi Sun, Anindya Banerjee, David A. Naumann
• Keywords: Algorithm Involves Inference, Formal Methods, Information flow Policies, SAS 2004, Security Types