The Carnegie Mellon University Binary Analysis Platform (CMU BAP) is a suite of utilities and libraries that enables analysis of programs that are represented as machine code (aka binaries). CMU BAP is written in OCaml and uses plugin-based architecture to enable extensibility. We also have a domain-specific language, called Primus Lisp, that we use to write analysis, specify verification conditions, interact with the built-in SMT solver, and model the semantics of machine instructions and functions.
The 2.1.0 Release is very rich in new features but the most prominent addition is the new symbolic executor mode for the Primus framework. We also significantly updated the Primus framework, integrated it with our new Knowledge Base, which was introduced in the BAP 2.0 release; we made our interpreter much faster; we added the systems and components facilities, inspired by Common Lisp; and we implemented a gradual type checker for Primus Lisp with type inference. We also added an ability to represent machine instructions as intrinsic functions so now it is possible to express their semantics using Primus Lisp since we added IEEE754 primitives to the Lisp interpreter.
As usual, we upgraded BAP to the newer versions of the Core library and OCaml (we now support OCaml versions from 4.07 to 4.09). We also significantly improved our build times and added an optional omake backend, which we are using in-house.
From the user perspective, one of the key features of BAP as an analysis platform is that you can run BAP on binaries that you can’t run otherwise, either because they need special hardware or software, or need to interact with the outside world. In the past couple of months, we have run BAP on various firmware and found numerous zero-day vulnerabilities, particular, we were able to find critical vulnerabilities in the VxWorks operating system that runs on, potentially, billions of devices including mission-critical and military appliances.
As always, questions, suggestions, and opinions are very welcome!