gdb demo 3

How I gave ManticoreUI a makeover

By Calvin Fong During my internship at Trail of Bits, I explored the effectiveness of symbolic execution for finding vulnerabilities in native applications ranging from CTF challenges to popular open source libraries ...
Manticore GUIs made easy

Manticore GUIs made easy

By Wong Kok Rui, National University of Singapore Trail of Bits maintains Manticore, a symbolic execution engine that can analyze smart contracts and native binaries. While symbolic execution is a powerful technique ...
Maat: Symbolic execution made easy

Maat: Symbolic execution made easy

By Boyan Milanov We have released Maat, a cross-architecture, multi-purpose, and user-friendly symbolic execution framework. It provides common symbolic execution capabilities such as dynamic symbolic execution (DSE), taint analysis, binary instrumentation, environment ...
MUI: Visualizing symbolic execution with Manticore and Binary Ninja

MUI: Visualizing symbolic execution with Manticore and Binary Ninja

By Alan Chang, University of Oxford During my summer internship, I had the wonderful opportunity to work on the Manticore User Interface (MUI). The MUI project aims to combine the strength of ...

Contract verification made easier

Smart contract authors can now express security properties in the same language they use to write their code (Solidity) and our new tool, manticore-verifier, will automatically verify those invariants. Even better, Echidna ...
Figure 1: Sam Sun (samczsun) discovered a critical vulnerability in ENS

Manticore discovers the ENS bug

The Ethereum Name Service (ENS) contract recently suffered from a critical bug that prompted a security advisory and a migration to a new contract (CVE-2020-5232). ENS allows users to associate online resources ...
image7

Symbolically Executing WebAssembly in Manticore

With the release of Manticore 0.3.3, we’re proud to announce support for symbolically executing WebAssembly (WASM) binaries. WASM is a newly standardized programming language that allows web developers to run code with ...
Anatomy of an Unsafe Smart Contract Programming Language

Watch Your Language: Our First Vyper Audit

A lot of companies are working on Ethereum smart contracts, yet writing secure contracts remains a difficult task. You still have to avoid common pitfalls, compiler issues, and constantly check your code ...
Screenshot from 2019-08-09 15-11-26

Binary symbolic execution with KLEE-Native

KLEE-Native, a fork of KLEE that operates on binary program snapshots by lifting machine code to LLVM bitcode ...

Fuzzing Unit Tests with DeepState and Eclipser

If unit tests are important to you, there’s now another reason to use DeepState, our Google-Test-like property-based testing tool for C and C++. It’s called Eclipser, a powerful new fuzzer very recently ...