The project focusses on the construction of secure mobile software. Our goal is to develop technologies to verify information flow security of Java and bytecode programs. Starting from existing formalisms, we plan to develop specification notations, type systems, and program logics which allow the code producer to statically certify information flow security properties of mobile software.
Motivated by mobile application scenarios, we plan to examine in particular those security policies that partly depend on the execution environment, or which are a result of consumer-based specialization of parametric policies. Parts of the verification infrastructure will be implemented as compiler extensions or verified formally in a theorem prover in order to integrate them later as components in proof-carrying code system.