A Tested Formal Semantics of Dalvik Bytecode: Progress and Challenges


At the MAIS group, a formal semantics of Dalvik bytecode has been
developed in order to prove the soundness of the type-based
information-flow analysis underlying the Certifying App Store
Cassandra. More recently, this semantics has been formalized in
the proof assistant Isabelle/HOL.

Apart from the benefit of being checked for consistency, developing
formal semantics in a proof assistant like Isabelle/HOL has the
additional benefit that an executable version of the model can be
generated automatically. This allows us to validate our semantics
by testing: We can compare the execution of code according to the
formal semantics with the actual behavior of the Dalvik Virtual
Machine, which we use as the reference semantics. In this manner,
we can establish the faithfulness of our formal semantics.

In this talk, I present the current status of the research project
as well as remaining open problems.