Name: Anonymous 2011-04-28 14:41
http://www.youtube.com/watch?v=VPe1W7SIdBE
http://security.ece.cmu.edu/aeg/
The automatic exploit generation challenge we address is given a program, automatically find security-critical bugs and generate exploits. Our approach uses a novel formal verification technique called preconditioned symbolic execution to make automatic exploit generation more scalable to real-world programs than without it. We implemented our techniques in a system called AEG, which we use to automatically generate 16 exploits for 14 open-source projects. Two of the generated exploits are against previously unknown vulnerabilities.
The hard part, in our experience, was exploring the state space efficiently to find bugs, determine the problem, and generate an initial input that triggers the bug. The core of our paper is a technique called preconditioned symbolic execution, which provides better scalability for finding exploitable bugs than when using previous symbolic execution techniques. The main idea is to guide symbolic execution to program paths that are more likely to be exploitable. Basic symbolic execution tends to try and explore all paths, which is more expensive. Our implementation is built on top of KLEE, a great symbolic execution engine from researchers at Stanford.
We are very excited about these results, and think they show a real step forward in state of the art. Don't take this to mean we believe it's a solved problem. Our future work focuses on scaling to larger and more programs, to more types of exploits, and to other relevant problem settings. There is plenty still to do.
Now, imagine using this as a backend rooting modality for an AI agent built with OpenCog to own systems 24/7.
http://security.ece.cmu.edu/aeg/
The automatic exploit generation challenge we address is given a program, automatically find security-critical bugs and generate exploits. Our approach uses a novel formal verification technique called preconditioned symbolic execution to make automatic exploit generation more scalable to real-world programs than without it. We implemented our techniques in a system called AEG, which we use to automatically generate 16 exploits for 14 open-source projects. Two of the generated exploits are against previously unknown vulnerabilities.
The hard part, in our experience, was exploring the state space efficiently to find bugs, determine the problem, and generate an initial input that triggers the bug. The core of our paper is a technique called preconditioned symbolic execution, which provides better scalability for finding exploitable bugs than when using previous symbolic execution techniques. The main idea is to guide symbolic execution to program paths that are more likely to be exploitable. Basic symbolic execution tends to try and explore all paths, which is more expensive. Our implementation is built on top of KLEE, a great symbolic execution engine from researchers at Stanford.
We are very excited about these results, and think they show a real step forward in state of the art. Don't take this to mean we believe it's a solved problem. Our future work focuses on scaling to larger and more programs, to more types of exploits, and to other relevant problem settings. There is plenty still to do.
Now, imagine using this as a backend rooting modality for an AI agent built with OpenCog to own systems 24/7.