Our research revolves around the automatic hardening and auditing of applications and systems using static and dynamic program analysis. We focus on the detection of software vulnerabilities and malware, and on instrumenting software to prevent exploitation. We emphasize theoretically well-founded concepts, but target concrete problems in systems security.

ExpoSE: Symbolic Execution for Real-World JavaScript

Sponsored by the UK Research Institute in Verified Trustworthy Software Systems and the Royal Holloway Centre for Doctoral Training in Cyber Security.

JavaScript has evolved into a versatile ecosystem for not just the web, but also a wide range of server-side and client-side applications. With this increased scope, the potential impact of bugs increases. With ExpoSE, we are developing a dynamic symbolic execution engine for Node.js JavaScript applications. ExpoSE automatically generates test cases to find bugs and cover as many paths in the target program as possible. In this project, we address the specific challenges for symbolic execution arising in real-world JavaScript code, from regular expressions to asynchronous execution. ExpoSE is available on GitHub.

MobSec: Malware and Security in the Mobile Age

Sponsored by EPSRC (EP/L022710/1) and a donation from Intel Security / McAfee Labs UK.

A main theme of the project are mobile applications analyses to extract behavioral information necessary for effective policy enforcement and mobile malware mitigation techniques. The CopperDroid system allows to perform dynamic behavioral analysis of Android malware and presents a unified analysis to characterize low-level OS-specific and high-level Android-specific behaviors. MobSec explores research questions around the automatic, comprehensive, and faithful reconstruction of Android app behaviors, the reliable identification of behaviors triggered by malware embedded in benign applications, event-behavior attributions, and the simulation of complex UI interactions.

We are also concerned with the detection of malicious mobile applications, a particularly challenging task in the mobile landscape that largely sees malware repackaged (and embedded) in benign apps.

Automated Security Testing of Webview Interfaces

Sponsored by a Google Faculty Research Award.

Many Android applications use an embedded webview, essentially a bare bones web browser, and expose an interface for JavaScript content in the webview to interact with the app. Since they typically control both the app and the JavaScript code, developers consider these interfaces to be private. However, malicious attackers may manipulate contents loaded through network connections and can thus interact with the interface almost arbitrarily. The goal of this project is to develop methods for assessing the impact of insecure interfaces: while many functions exposed through such interfaces are harmless, some can allow an attacker to obtain or manipulate sensitive information, or even to load additional privilege escalation exploits.

Automated Exploit Generation

Sponsored by L3-TRL.

Vulnerabilities in software are a major security concern; when they are reported, they usually require immediate and expensive action by the affected software vendor. However, many vulnerabilities are not disclosed to the vendor but instead collected and traded by government agencies and cyber criminals alike. Even where developers may have seen warnings or bug reports by testing or static analysis, they may lack the specialized knowledge to determine whether a suspicious line of code is an exploitable vulnerability. The idea of automated exploit generation (AEG) systems promises to democratize the art of exploit writing. An AEG system can demonstrate the severity of a bug by generating a working targeted exploit, which takes control of the program and executes a payload, such as spawning a shell.

Jakstab: Static Analysis of x86 Executables

Jakstab allows to statically analyze binaries directly, without relying on any preprocessing. It integrates disassembly, control flow graph reconstruction, and abstract interpretation in a single process. Jakstab was successfully used to verify Windows device driver binaries and generate control flow graphs for Windows and Linux binaries. Because it avoids making assumptions about well-behavedness of code, its particularly good at working with unconventional and hand-written machine code. In ongoing work, Jakstab is being extended to remove obfuscation layers from malware by static analysis. Jakstab is open source and designed to be extensible by custom analysis and binary frontends. Check it out on