Type-Based Verification of Noninterference for Dalvik-Programs with 
Exception Handling


Smartphones have access to private data of their user and are able to 
connect with multiple devices via different channels. Therefore the 
user has to be able to rely on the program to preserve his privacy. To 
check whether a program keeps the private information confidential, 
information flow analyses are suitable. For the source code is usually 
not available on a smartphone, the file format for the execution 
should be analyzed directly.

Programs on the most widely used mobile platform Android are usually 
executed in Dalvik bytecode. Dalvik bytecode allows handling 
exceptions separately from the normal execution. Exceptional behavior 
exhibited by a program can be treated together. By throwing and 
handling exceptions, a program may disclose confidential information. 
We present an extention of an existing information flow analysis for 
Dalvik bytecode to an analysis of exception handling.