DeepState: C/C++ symbolic execution unit test framework from Trail of Bits

DeepState is a framework that provides C and C++ developers with a common interface to various symbolic execution and fuzzing engines. Users can write one test harness using a Google Test-like API, then execute it using multiple backends without having to learn the complexities of the underlying engines. It supports writing unit tests and API sequence tests, as well as automatic test generation. DeepState currently targets Linux, with macOS support in progress.

https://github.com/trailofbits/deepstate

Click to access bar18.pdf

Trail of Bits releases McSema 2.0: Framework for lifting x86, amd64, and aarch64 program binaries to LLVM bitcode

Heavy lifting with McSema 2.0

Four years ago, we released McSema, our x86 to LLVM bitcode binary translator. Since then, it has stretched and flexed; we added x86-64 support, put it on a performance-focused diet, and improved its usability and documentation. McSema wasn’t the only thing improving these past years, though. At the same time, programs were increasingly adopting modern x86 features like the advanced vector extensions (AVX) instructions, which operate on 256-bit wide vector registers. Adjusting to these changes was back-breaking but achievable work. Then our lifting goals expanded to include AArch64, the architecture used by modern smartphones. That’s when we realized that we needed to step back and strengthen McSema’s core. This change in focus paid off; now McSema can transpile AArch64 binaries into x86-64! Keep reading for more details.[…]

Heavy lifting with McSema 2.0

https://github.com/trailofbits/mcsema

https://github.com/trailofbits/mcsema/blob/master/docs/McSemaWalkthrough.md

https://www.trailofbits.com/research-and-development/mcsema/

 

TrailOfBits releases osquery extenson repo, including EFI use

 

Announcing the Trail of Bits osquery extension repository

Manticore

Manticore is a prototyping tool for dynamic binary analysis, with support for symbolic execution, taint analysis, and binary instrumentation.
Features
* Input Generation: Manticore automatically generates inputs that trigger unique code paths
* Crash Discovery: Manticore discovers inputs that crash programs via memory safety violations
* Execution Tracing: Manticore records an instruction-level trace of execution for each generated input
* Programmatic Interface: Manticore exposes programmatic access to its analysis engine via a Python API

https://github.com/trailofbits/manticore

https://github.com/trailofbits/manticore/wiki

Binary Ninja

Ryan Stortz has a new post on the Trail of Bits Blog on the tool Binary Ninja:

Using Vector35’s Binary Ninja, a promising new interactive static analysis and reverse engineering platform, I wrote a script that generated “exploits” for 2,000 unique binaries in this year’s DEFCON CTF qualifying round. If you’re wondering how to remain competitive in a post-DARPA DEFCON CTF, I highly recommend you take a look at Binary Ninja. Before I share how I slashed through the three challenges — 334 cuts, 666 cuts, and 1,000 cuts — I have to acknowledge the tool that made my work possible. Compared to my experience with IDA, which is held together with duct tape and prayers, Binary Ninja’s workflow is a pleasure. It does analysis on its own intermediate language (IL), which is exposed through Python and C++ APIs. It’s comparatively simple to query blocks of code, functions, trace execution flow, query register states, and many other tasks that seem herculean within IDA.

Binary Ninja is a commercial product, not open source, US$$100-400, with an Enterprise level coming soon:

Binary Ninja currently comes in two different flavors. The personal edition is primarily for students and hobbyists to give them a powerful feature set at an extremely affordable price. The personal license’s primary restriction is that it only allows non-commercial use. The standard license includes more than just the freedom to profit with your work though. Some specific features targeting professional or power users are also included, while still keeping the personal edition featureful.

Well, it comes from an open source roots, and that is still available, but deprecated, see the Prototype page and the Github page:

http://binary.ninja/
http://binary.ninja/purchase.html
http://binary.ninja/prototype.html
https://github.com/Vector35/deprecated-binaryninja-python
2000 cuts with Binary Ninja