Information flow analysis for mobile code in dynamic security environments

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