Security Type Inference for the Type-Based Information Flow Analysis of Java Programs


Verifying computer programs to operate on data according to the specification of a 
security policy is a non-trivial yet important problem. To check a program’s 
satisfaction of a security policy (e.g., expressing confidentiality goals), static 
analysis mechanisms in the form of security type systems have successfully been 
applied. A sound static security analysis deciding the security of Java programs with 
respect to user supplied security policies is proposed by Banerjee and Naumann. To 
apply the analysis, a detailed specification of the security policy is required. This 
makes the analysis intractable for realistically sized applications.

In this thesis, we develop an inference algorithm to automate the security analysis 
suggested by Banerjee and Naumann. We allow policy to be specified in terms of a 
programs end-to-end behavior. The inference algorithm then infers the end-to-end 
policy to a refined policy as required for Banerjee and Naumann’s security analysis. 
We test the applicability of our inference algorithm in detail on two example programs 
and give intuitive arguments regarding the algorithm’s correctness.