For a given piece of software, it is in general hard to assess if it satisfies the properties that the manufacturer promises. If these properties are defined formally, then formal methods can be used to verify whether the software satisfies the properties. This verification can be done in two ways: statically, i.e., by analyzing the code of an application at installation time, or dynamically, i.e., by monitoring execution steps of an application during its run-time. In this lab course we will consider security properties (e.g., information flow properties) and implement selected verification methods on real mobile devices like Android smartphones or tablets.
Last modified on 22 October 2012.