BAP: A Binary Analysis Platform
Lecture notes in computer sciencePublished 1 January 2011
David Brumley, Ivan Jager, Thanassis Avgerinos, Edward J. Schwartz
Citations425
SJR quartileQ2
SJR score0.35
SNIP0.55
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
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.
Abstract
BAP is a publicly available infrastructure for performing program verification and analysis tasks on binary (i.e., executable) code. In this paper, we describe BAP as well as lessons learned from previous incarnations of binary analysis platforms. BAP explicitly represents all side effects of instructions in an intermediate language (IL), making syntaxdirected analysis possible. We have used BAP to routinely generate and solve verification conditions that are hundreds of megabytes in size and encompass 100,000's of assembly instructions.
Keywords
Computer Science
All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask)
702 Citations2010Edward J. Schwartz, Thanassis Avgerinos +1 more
The algorithms for dynamic taint analysis and forward symbolic execution are described as extensions to the run-time semantics of a general language to highlight important implementation choices, common pitfalls, and considerations when using these techniques in a security context.
Lecture notes in computer scienceA Decision Procedure for Bit-Vectors and Arrays
590 Citations2007Vijay Ganesh, David L. Dill
Experimental results indicate that the above mix of algorithms along with the overall architecture is far more effective, for a variety of applications, than a direct translation of the original formula to SAT or other comparable decision procedures.
Electronic Notes in Theoretical Computer ScienceValgrind
456 Citations2003Nicholas Nethercote, Julian Seward
Valgrind is a programmable framework for creating program supervision tools such as bug detectors and profilers that executes supervised programs using dynamic binary translation, giving it total control over their every part without requiring source code, and without the need for recompilation or relinking prior to execution.
Cambridge University Press eBooksModern Compiler Implementation in C
411 Citations1997Andrew W. Appel, Maia Ginsburg
ACM Transactions on Programming Languages and SystemsWYSINWYX
274 Citations2010Gogul Balakrishnan, Thomas Reps
The article presents the algorithms that were developed, explains how they are used to recover Intermediate Representations from executables that are similar to the IRs that would be available if one started from source code, and describes their application in the context of program understanding and automated bug hunting.
FigshareTIE: Principled Reverse Engineering of Types in Binary Programs
169 Citations2018JongHyup Lee, Thanassis Avgerinos +1 more
Novel techniques for reverse engineering data type abstractions from binary programs are developed and a novel type reconstruction system based upon binary code analysis is developed that is both more accurate and more precise at recovering high-level types than existing mechanisms.
Cambridge University Press eBooksModern Compiler Implementation in ML
168 Citations1997Andrew W. Appel
Lecture notes in computer scienceWYSINWYX: What You See Is Not What You eXecute
153 Citations2008Gogul Balakrishnan, Thomas Reps +2 more
Lecture notes in computer scienceCodeSurfer/x86—A Platform for Analyzing x86 Executables
140 Citations2005Gogul Balakrishnan, Radu Gruian +2 more
CodeSurfer/x86 is a prototype system for analyzing x86 executables that uses a static-analysis algorithm called value-set analysis (VSA) to recover intermediate representations that are similar to those that a compiler creates for a program written in a high-level language.
Lecture notes in computer scienceJakstab: A Static Analysis Platform for Binaries
135 Citations2008Johannes Kinder, Helmut Veith
This work presents their fully configurable binary analysis platform Jakstab, which resolves indirect branches by multiple rounds of disassembly interleaved with dataflow analysis, and demonstrates that this iterative disassembling strategy achieves better results than the state-of-the-art tool IDA Pro.
Lecture notes in computer scienceDirected Proof Generation for Machine Code
61 Citations2010Aditya Thakur, Junghee Lim +6 more
What distinguishes McVeto from other work on software model checking is that it shows how verification of machine-code can be performed, while avoiding conventional techniques that would be unsound if applied at the machine- code level.
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.