On November 26, 2013, Prof. Dr. Heiko Mantel will give a talk on "Towards more Reliable Software Security".
Formal methods and program analysis techniques can contribute to making software security more reliable. A formal specification of security requirements clarifies in which sense security shall be achieved, and analysis tools clarify whether it has been achieved. In this presentation, I will illustrate the use of formal methods and of program analysis at two practically relevant security requirements. I will show how to formalize such requirements, discuss which program analysis techniques are suitable for which properties, and present two novel security analysis tools. The CliSeAu tool enforces security in distributed Java programs at run-time and the RSCP security analyzer statically verifies security requirements in Android applications.