A Formal Model, a Noninterference Condition, and a Sound Type System 
for a Certifying Application Store


A certifying app store for Android applications has been designed and 
implemented recently by Bähr, Keller, Schneider, Starostin and Weber 
with the intention of guaranteeing the absence of undesired 
information flow in applications. Its underlying analysis technique is 
an information-flow-sensitive security type system which can be used 
to check whether an application leaks confidential information.

The thesis that is presented in this talk provides a soundness result 
for this type system. The soundness result with respect to a timing- 
and termination-insensitive information flow condition is based on an 
operational semantics for an abstract instruction set of Dalvik 
bytecode, excluding concurrency and exceptions. The semantics and the 
security condition have been formalized in this thesis.

During the process of proving soundness, mistakes in the 
implementation of the certifying app store were detected and the type 
system was adapted accordingly. Consequently, this thesis provides 
feedback on the implementation of the certifying app store and 
increases confidence in the modified version.

The presentation gives an overview of the work that has been done and 
focusses on the relevance for the certifying app store.