Sponsored by L3-TRL and the Royal Holloway Centre for Doctoral Training in Cyber Security.

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.

Existing AEG approaches are based on test generation and formal verification methods such as symbolic execution or bounded model checking. To verify exploitability, the system requires a test case exhibiting the target bug; this test case is either provided by the developer or generated through another automated test generation tool. The exploit generation system then checks whether exploitability conditions can be met: it searches for a way to take control of the target program, e.g., by specially crafting the input such that the program overwrites return addresses on the stack or the values of function pointers. By symbolically executing the program code along specific paths, it builds a propositional formula encoding the exploitability condition. An external theorem prover then checks the satisfiability of the condition and generates an input assignment that can be converted into the actual exploit.

 The basic AEG concept has been proven to work with stack overflows on command-line based binaries compiled from C code . However, modern operating systems come with a wide range of defences that make such attacks largely impossible (stack canaries, ASLR, DEP, …). Practical attacks nowadays use different attack vectors, including heap overflows and combinations of different vulnerabilities. This project focuses on developing prototypes for such advanced forms of automated exploit generation.

Outputs

  • Dusan Repel, Johannes Kinder, and Lorenzo Cavallaro. Modular Synthesis of Heap Exploits. In Proc. ACM SIGSAC Workshop on Programming Languages and Analysis for Security (PLAS), 2017 [ PDF ]
  • James Patrick-Evans, Lorenzo Cavallaro, and Johannes Kinder. POTUS: Probing Off-The-Shelf USB Drivers with Symbolic Fault Injection. In 11th USENIX Workshop on Offensive Technologies (WOOT), 2017. Best Paper Award. [ PDF ]