2022

Amarna: Static analysis for Cairo programs

We are open-sourcing Amarna, our new static analyzer and linter for the Cairo programming language. Cairo is a programming language powering several trading exchanges with millions of dollars in assets (such as dYdX, driven by StarkWare) and is the programming language for StarkNet contracts. But, not unlike other languages, it has its […]

The Frozen Heart vulnerability in PlonK

In part 1 of this blog post, we disclosed critical vulnerabilities that break the soundness of multiple implementations of zero-knowledge proof systems. This class of vulnerability, which we dubbed Frozen Heart, is caused by insecure implementations of the Fiat-Shamir transformation that allow malicious users to forge proofs for random statements. In part […]

The Frozen Heart vulnerability in Bulletproofs

In part 1 of this series, we disclosed critical vulnerabilities that break the soundness of multiple implementations of zero-knowledge proof systems. This class of vulnerability, which we dubbed Frozen Heart, is caused by insecure implementations of the Fiat-Shamir transformation that allow malicious users to forge proofs for random statements. In part 2, […]

Coordinated disclosure of vulnerabilities affecting Girault, Bulletproofs, and PlonK

Trail of Bits is publicly disclosing critical vulnerabilities that break the soundness of multiple implementations of zero-knowledge proof systems, including PlonK and Bulletproofs. These vulnerabilities are caused by insecure implementations of the Fiat-Shamir transformation that allow malicious users to forge proofs for random statements. We’ve dubbed this class of vulnerabilities Frozen Heart. […]

Optimizing a smart contract fuzzer

During my winternship, I applied code analysis tools, such as GHC’s Haskell profiler, to improve the efficiency of the Echidna smart contract fuzzer. As a result, Echidna is now over six times faster! Echidna overview To use Echidna, users provide smart contracts and a list of conditions that should be satisfied no […]

Maat: Symbolic execution made easy

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 simulation, and constraint solving. Maat is easy-to-use, is based on the popular Ghidra intermediate representation (IR) language p-code, prioritizes runtime performance, and has […]

Part 2: Improving crypto code in Rust using LLVM’s optnone

Let’s implement crypto! Welcome to the second part of our posts on the challenges of implementing constant-time Rust code. Part 1 discussed challenges with constant-time implementations in Rust and WebAssembly and how optimization barriers can mitigate risk. The Rust crypto community has responded with several approaches, and in this post, we will […]

Part 1: The life of an optimization barrier

Many engineers choose Rust as their language of choice for implementing cryptographic protocols because of its robust security guarantees. Although Rust makes safe cryptographic engineering easier, there are still some challenges to be aware of. Among them is the need to preserve constant-time properties, which ensure that, regardless of the input, code […]

Finding unhandled errors using CodeQL

One of your developers finds a bug in your codebase—an unhandled error code—and wonders whether there could be more. He combs through the code and finds unhandled error after unhandled error. One lone developer playing whack-a-mole. It’s not enough. And your undisciplined team of first-year Stanford grads never learned software engineering. You’re […]