Automatic exploit generation
Communications of the ACMPublished 28 January 2014
Thanassis Avgerinos, Sang Kil, Alexandre Rebert, Edward J. Schwartz, Maverick Woo, David Brumley
Citations258
SJR quartileQ1
SJR score1.15
SNIP3.34
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
The idea is to identify security-critical software bugs so they can be fixed first rather than waiting for them to be fixed later.
Abstract
The idea is to identify security-critical software bugs so they can be fixed first.
Keywords
Computer Science
Communications of the ACMSymbolic execution and program testing
2,991 Citations1976James C. King
A particular system called EFFIGY which provides symbolic execution for program testing and debugging is described, which interpretively executes programs written in a simple PL/I style programming language.
KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs
2,681 Citations2008Cristian Cadar, Daniel Dunbar +1 more
A new symbolic execution tool, KLEE, capable of automatically generating tests that achieve high coverage on a diverse set of complex and environmentally-intensive programs, and significantly beat the coverage of the developers' own handwritten test suite is presented.
CUTE
1,653 Citations2005Koushik Sen, Darko Marinov +1 more
A method to represent and track constraints that capture the behavior of a symbolic execution of a unit with memory graphs as inputs is developed and an efficient constraint solver is proposed to facilitate incremental generation of such test inputs.
DART
1,501 Citations2005Patrice Godefroid, Nils Klarlund +1 more
DART is a new tool for automatically testing software that combines three main techniques, automated extraction of the interface of a program with its external environment using static source-code parsing, and dynamic analysis of how the program behaves under random testing and automatic generation of new test inputs to direct systematically the execution along alternative program paths.
The geometry of innocent flesh on the bone
1,262 Citations2007Hovav Shacham
A return-into-libc attack to be mounted on x86 executables that calls no functions at all is presented, and how to discover such instruction sequences by means of static analysis is shown.
On the effectiveness of address-space randomization
861 Citations2004Hovav Shacham, Matthew J. Page +4 more
Aderandomization attack is demonstrated that will convert any standard buffer-overflow exploit into an exploit that works against systems protected by address-space randomization, and it is concluded that, on 32-bit architectures, the only benefit of PaX-like address- space randomization is a small slowdown in worm propagation speed.
EXE
789 Citations2006Cristian Cadar, Vijay Ganesh +3 more
This paper presents EXE, an effective bug-finding tool that automatically generates inputs that crash real code instead of running code on manually or randomly constructed input, and solves the current path constraints to find concrete values using its own co-designed constraint solver, STP.
Communications of the ACMSymbolic execution for software testing
749 Citations2013Cristian Cadar, Koushik Sen
The challenges---and great promise---of modern symbolic execution techniques, and the tools to help implement them.
Communications of the ACMSatisfiability modulo theories
629 Citations2011Leonardo de Moura, Nikolaj Bjørner
IEEE Transactions on Software EngineeringAn Attack Surface Metric
608 Citations2010Pratyusa K. Manadhata, Jeannette M. Wing
The notion of a system's attack surface is formalized and an attack surface metric is introduced to measure the attack surface in a systematic manner and is useful in multiple phases of the software development lifecycle.
Before we knew it
608 Citations2012Leyla Bilge, Tudor Dumitraş
This paper describes a method for automatically identifying zero-day attacks from field-gathered data that records when benign and malicious binaries are downloaded on 11 million real hosts around the world and identifies 18 vulnerabilities exploited before disclosure.
Communications of the ACMSAGE
562 Citations2012Patrice Godefroid, Michael Y. Levin +1 more
SAGE has had a remarkable impact at Microsoft and will continue to have an important role in the company's strategy and operations for years to come.
Unleashing Mayhem on Binary Code
521 Citations2012Sang Kil, Thanassis Avgerinos +2 more
This paper proposes two novel techniques: 1) hybrid symbolic execution for combining online and offline (concolic) execution to maximize the benefits of both techniques, and 2) index-based memory modeling, a technique that allows Mayhem to efficiently reason about symbolic memory at the binary level.
Lecture notes in computer scienceBAP: A Binary Analysis Platform
425 Citations2011David Brumley, Ivan Jager +2 more
BAP explicitly represents all side effects of instructions in an intermediate language (IL), making syntaxdirected analysis possible and used to routinely generate and solve verification conditions that are hundreds of megabytes in size and encompass 100,000's of assembly instructions.
ACM SIGPLAN NoticesSELECT—a formal system for testing and debugging programs by symbolic execution
388 Citations1975Robert S. Boyer, B. Elspas +1 more
SELECT appears to be a useful tool for rapidly revealing program errors, but for the future there is a need to expand its expressive and deductive power.
Compositional dynamic test generation
308 Citations2007Patrice Godefroid
This paper introduces a new algorithm, dubbed SMART for Systematic Modular Automated Random Testing, that extends DART by testing functions in isolation, encoding test results as function summaries expressed using input preconditions and output postconditions, and then re-using those summaries when testing higher-level functions.
Proceedings - IEEE Symposium on Security and Privacy/Proceedings of the ... IEEE Symposium on Security and PrivacyAutomatic Patch-Based Exploit Generation is Possible: Techniques and Implications
283 Citations2008David Brumley, Pongsin Poosankam +2 more
Avoiding exponential explosion
220 Citations2001Cormac Flanagan, James B. Saxe
A two-stage VC generation algorithm that generates compact VCs whose size is worst-case quadratic in the size of the source fragment, and is close to linear in practice.
FigshareAEG: Automatic Exploit Generation
209 Citations2018Thanassis Avgerinos, Cha, Sang Kil +2 more
This paper presents AEG, the first end-to-end system for fully automatic exploit generation, which was used to analyze 14 open-source projects and successfully generated 16 control flow hijacking exploits.
ACM Transactions on Computer SystemsThe S2E Platform
198 Citations2012Vitaly Chipounov, Volodymyr Kuznetsov +1 more
This article presents S2E, a platform for analyzing the properties and behavior of software systems, along with its use in developing tools for comprehensive performance profiling, reverse engineering of proprietary software, and automated testing of kernel-mode and user-mode binaries.
IEEE Transactions on ComputersMethodology for the Generation of Program Test Data
195 Citations1975William E. Howden
The methodology is a model of the test data generation process and can be used to characterize the basic problems of testData generation and build an automatic test data Generation system.
Efficient state merging in symbolic execution
186 Citations2012Volodymyr Kuznetsov, Johannes Kinder +2 more
A way to automatically choose when and how to merge states such that the performance of symbolic execution is significantly increased and query count estimation, a method for statically estimating the impact that each symbolic variable has on solver queries that follow a potential merge point, is presented.
Research Showcase @ Carnegie Mellon University (Carnegie Mellon University)Q: Exploit Hardening Made Easy
186 Citations2018Edward J. Schwartz, Thanassis Avgerinos +1 more
Q, an end-to-end system that automatically generates ROP payloads for a given binary, is built and shown that Q can automatically perform exploit hardening, enabling an attacker to automatically bypass defenses as deployed by industry for those programs.
Loop-extended symbolic execution on binary programs
162 Citations2009Prateek Saxena, Pongsin Poosankam +2 more
SELECT---a formal system for testing and debugging programs by symbolic execution
162 Citations1975Robert S. Boyer, B. Elspas +1 more
SELECT appears to be a useful tool for rapidly revealing program errors, but for the future there is a need to expand its expressive and deductive power.
Bouncer
154 Citations2007Manuel Costa, Miguel Castro +3 more
Bouncer introduces a new form of program slicing that uses a combination of static and dynamic analysis to remove unnecessary conditions from the filter and symbolic summaries for common library functions that characterize their behavior succinctly as a set of conditions on the input.
Lecture notes in computer scienceMemory Errors: The Past, the Present, and the Future
145 Citations2012Victor van der Veen, Nitish dutt-Sharma +2 more
A historical overview provides insights in past trends and developments, while an investigation of real-world vulnerabilities and exploits allows us to answer on the significance of memory errors in the foreseeable future.
Billions and billions of constraints: whitebox fuzz testing in production
117 Citations2013Ella Bounimova, Patrice Godefroid +1 more
Improving integer security for systems with KINT
88 Citations2012Xi Wang, Haogang Chen +3 more
KINT, a tool that uses scalable static analysis to detect integer errors in C programs, is presented and a new integer family with NaN semantics is proposed to help developers avoid integer errorsIn C programs.
Under-constrained execution
65 Citations2007Dawson Engler, Daniel Dunbar
Software testing is well-recognized as a crucial part of the modern software development process, however, manual testing is labor intensive and often fails to produce impressive coverage results.
Computer and Communications SecurityEXE: A system for automatically generating inputs of death using symbolic execution
61 Citations2006Cristian Cadar, Vijay Ganesh +3 more
Bayesian modeling, Bayesian inference and the fast algorithm are presented to achieve the maximum-a-posterior (MAP) solution and the improved computational efficiency of using Laplace prior is validated in the localization-time experiment as well.
SMT solvers for software security
30 Citations2012Julien Vanegue, Sean Heelan +1 more
Three practical applications of SAT to software security in static vulnerability checking, exploit generation, and the study of copy protections are presented.
IEEE Transactions on Dependable and Secure ComputingTheory and Techniques for Automatic Generation of Vulnerability-Based Signatures
30 Citations2008David Brumley, J.P. Newsome +3 more
This paper creates vulnerability signatures which are guaranteed to have zero false positives, and shows how to automate signature creation for any vulnerability that can be detected by a runtime monitor.
Automatic discovery of API-level exploits
27 Citations2005Vinod Ganapathy, Sanjit A. Seshia +3 more
A framework to model low-level details of APIs is presented, and an automatic technique based on bounded, infinite-state model checking to discover API-level exploits is developed, which is demonstrated by finding exploits against vulnerabilities in widely-used software.
Efficient Directionless Weakest Preconditions
18 Citations2011David Brumley, Ivan Jager
This work reconcile the differences between FSE and WP by proposing a new directionless weakest precondition that can be run in both the forward and backward direction and provides the more attractive O(M 2 ) VC generation time and predicate size while allowing VC generation in execution order, which is what makes FSE attractive in practice.
Platform-independent programs
11 Citations2010Sang Kil, Brian Pak +2 more
This paper challenges the notion that programs run on a single architecture by developing techniques that automatically create a single program string that a) runs on different architectures, and b) potentially has different behaviors depending upon which architecture it runs on.