Information flow analysis for mobile code in dynamic security environments

摘要: With the growing amount of data handled by Internet-enabled mobile devices, task preventing software from leaking confidential information is becoming increasingly important. At the same time, mobile applications are typically executed on different devices whose users have varying requirements for the privacy their data. Users should be able to define their personal security settings, and they get a reliable assurance that installed respects these settings. Language-based flow focuses on the analysis programs determine flows among accessed resources different levels, to verify formally certify these follow a given policy. In code scenario, however, both dynamic aspect environment fact mobile software distributed as bytecode pose challenge existing static approaches. This thesis presents a language-based mechanism in the presence dynamic environments. An object-oriented high-level language well equipped with facilities inspect user-defined security settings at runtime. way, developer can create privacy-aware adapt behaviour to arbitrary environments, property formalized as "universal noninterference". statically verified an type system uses restrictive forms dependent types judge abstractly on concrete security policy effective To verify compiled bytecode programs, low-level version is presented works intermediate representation in which original program structure partially restored. Rigorous soundness proofs type-preserving compilation enable generation certified in style of proof-carrying code. show practical feasibility the approach, implemented demonstrated a concrete application where personal sent from a device server Internet.