Formal Analysis of the CBC Casper Consensus Algorithm with TLA+

by Anne Ouyang, Piedmont Hills High School, San Jose, CA As a summer intern at Trail of Bits, I used the PlusCal and TLA+ formal specification languages to explore Ethereum’s CBC Casper consensus protocol and its Byzantine fault tolerance. This work was motivated by the article Peer Review: CBC ... Read More

DeepState Now Supports Ensemble Fuzzing

| | fuzzing, Internship Projects
by Alan Cao, Francis Lewis High School, Queens, NY We are proud to announce the integration of ensemble fuzzing into DeepState, our unit-testing framework powered by fuzzing and symbolic execution. Ensemble fuzzing allows testers to execute multiple fuzzers with varying heuristics in a single campaign, while maintaining an architecture for ... Read More

Rewriting Functions in Compiled Binaries

by Aditi Gupta, Carnegie Mellon University As a summer intern at Trail of Bits, I’ve been working on building Fennec, a tool to automatically replace function calls in compiled binaries that’s built on top of McSema, a binary lifter developed by Trail of Bits. The Problem Let’s say you have ... Read More
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 ... Read More

Reverse Taint Analysis Using Binary Ninja

by Henry Wildermuth, Horace Mann High School We open-sourced a set of static analysis tools, KRFAnalysis, that analyze and triage output from our system call (syscall) fault injection tool KRF. Now you can easily figure out where and why, KRF crashes your programs. During my summer internship at Trail of ... Read More

Wrapper’s Delight

During my summer at Trail of Bits, I took full advantage of the latest C++ language features to build a new SQLite wrapper from scratch that is easy to use, lightweight, high performant, and concurrency friendly—all in under 750 lines of code ... Read More
On Bounties and Boffins

On Bounties and Boffins

Trying to make a living as a programmer participating in bug bounties is the same as convincing yourself that you’re good enough at Texas Hold ‘Em to quit your job. There’s data to back this up in Fixing a Hole: The Labor Market for Bugs, a chapter in New Solutions ... Read More

How to Spot Good Fuzzing Research

| | fuzzing, Guides
Of the nearly 200 papers on software fuzzing that have been published in the last three years, most of them—even some from high-impact conferences—are academic clamor. Fuzzing research suffers from inconsistent and subjective benchmarks, which keeps this potent field in a state of arrested development. We’d like to help explain ... Read More