Advancing Tool Support for the Detection of Side-Channel Vulnerabilities
in Java


The Assistant for Developing Leak-free Programs and the Side-Channel Finder 
are two tools developed in the MAIS group that implement static type-based 
information-flow analysis for Java programs. However, while the analysis of 
Adele is only concerned with direct and indirect flows, the SCF was developed 
for the detection of potential timing side channels. The SCF supports more 
Java constructs, in that number loops and array-related expressions and
statements.

One of the goals of my thesis is to implement a new tool, reusing the code 
base of Adele, which covers the Java subset of the SCF. This should be done 
by extending Adele's type system for verifying information-flow security. 
In this talk, I describe some of the typing rules that will be part of 
the security type system of the new tool.