Speaker: Johannes Kinder (Royal Holloway University of London, UK)
Johannes Kinder joined Royal Holloway's Computer Science Department in September 2013 after two years as a postdoctoral researcher in the Dependable Systems Lab at EPFL in Lausanne, Switzerland. He holds a doctorate in computer science from Technische Universität Darmstadt and a Master’s degree from Technische Universität München, Germany. His research interests revolve around automated program analysis, with particular focus on making formal methods applicable to assessing and improving the reliability and security of real world software.
Title: Automated Program Analysis for Trustworthy Software
The amount of software keeps growing steadily, but software quality assurance is not keeping pace. Users are faced with an increasingly complex choice of which applications to trust and install. In my talk, I propose to use automated program analysis both during development and during deployment to improve software quality assurance and protect users.
A particularly promising technique to help during development is symbolic execution, which can automatically generate test cases and find bugs by systematically exploring individual program paths. I explain tradeoffs in this generally expensive technique and introduce a heuristic for minimizing its cumulative cost by merging individual execution states, which allows experimental speed-ups of up to ten orders of magnitude.
To help users judge whether an application is trustworthy, I propose to use program analysis on deployed binaries. In this setting, one faces potentially malicious developers and cannot rely on their cooperation. Therefore, I suggest to apply static analysis directly to binaries and harden it against common obfuscation schemes by tightly integrating it with disassembly and control flow reconstruction. Based on this approach, I show how to statically defeat the infamous "virtualization obfuscation", which compiles programs into bytecode for randomized architectures.