Time: 11:00am - 12:00pm Venue: CS 414 4th Floor, Computer Science Bldg Queen Mary, University of London Mile End London E1 4NS
Automated Program Analysis for Trustworthy Software
Johannes Kinder (Royal Holloway)
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.