Writings

Technology and Research Articles

[Medium post]
We received bug bounties for disclosing smart contract vulnerabilities to Vesper Finance and BT Finance, via immunefi.com. We document the common pattern and analyze the preconditions for the attack.

R-Bounty / Primitive Finance Analysis

[Online articles]
Three articles on the Primitive Finance vulnerability disclosure and rescue:

[Medium post]
A vulnerable bot was allowing anyone to steal its owner's funds. We neutralized it, and the technical elements showcase an interesting Solidity anti-pattern.

[Medium post]
This story describes a cool hack, for over $300K (even nearly $600K, if done at the right time). It is a white-hat hack. We performed it off-chain, demonstrated to Dinngo, the authors of the vulnerable service, and they reproduced it and applied it to rescue the funds of exposed accounts, securing them.

[Medium post]
Saving DeFi Saver with Static Contract Analysis: a Vulnerability Report

[Research article, at OOPSLA'20 conference]
Static analysis of smart contracts as-deployed on the Ethereum blockchain has received much recent attention. However, high-precision analyses currently face significant challenges when dealing with the Ethereum VM (EVM) execution model. A major such challenge is the modeling of low-level, transient “memory” (as opposed to persistent, on-blockchain “storage”) that smart contracts employ. We offer an analysis that models EVM memory, recovering high-level concepts (e.g., arrays, buffers, call arguments) via deep modeling of the flow of values. Our analysis opens the door to Ethereum static analyses with drastically increased precision. One such analysis detects the extraction of ERC20 tokens by unauthorized users. For another practical vulnerability (redundant calls, possibly used as an attack vector), our memory modeling yields analysis precision of 89%, compared to 16% for a state-of-the-art tool without precise memory modeling. Additionally, precise memory modeling enables the static computation of a contract’s gas cost. This gas-cost analysis has recently been instrumental in the evaluation of the impact of the EIP-1884 repricing (in terms of gas costs) of EVM operations, leading to a reward and significant publicity from the Ethereum Foundation.

[Research article, at PLDI'20 conference]
Smart contracts on permissionless blockchains are exposedto inherent security risks due to interactions with untrusted entities. Static analyzers are essential for identifying security risks and avoiding millions of dollars worth of damage.
We introduce Ethainter, a security analyzer checking information flow with data sanitization in smart contracts. Ethainter identifies composite attacks that involve an escalation of tainted information, through multiple transactions, leading to severe violations. The analysis scales to the entire blockchain, consisting of hundreds of thousands of unique smart contracts, deployed over millions of accounts. Ethainter is more precise than previous approaches, as we confirm by automatic exploit generation (e.g., destroying over 800 contracts on the Ropsten network) and by manual inspection, showing a very high precision of 82.5% valid warnings for end-to-end vulnerabilities. Ethainter’s balance of precision and completeness offers significant advantages over other tools such as Securify, Securify2, and teEther.

[Medium post]
Although repricing opcodes can always break contracts, the EVM should be able to evolve too. Clearly, a decent number of contracts will be broken due to [EIP-1884], so care must be taken to lessen the impact on the overall ecosystem.

[Medium post]
In a few hours, an attacker will claim the prize for the first Consensys Diligence Ethereum hacking challenge. Here’s how they’ll do it, why nobody else can perform the same attack (any longer), and why the attacker has to wait…

[Medium Post]
Trivial Exploits of Bad Randomness In Ethereum, and How To Do On-Chain Randomness (Reasonably) Well.

Ethereum has been used as a platform for a variety of applications of financial interest. Several of these have a need for randomness — e.g., to implement a lottery, a competitive game, or crypto-collectibles. Unfortunately, writing a random number generator on a public blockchain is hard: computation needs to be deterministic, so that it can be replayed in a decentralized way, and all data that can serve as sources of randomness are also available to an attacker. Several exploits of bad randomness have been discussed exhaustively in the past. Next, we discuss near-trivial exploits of bad randomness, as well as ways to obtain true randomness in Ethereum.

[Research article, at ICSE'19 conference]
The rise of smart contract—autonomous applications running on blockchains—has led to a growing number of threats, necessitating sophisticated program analysis. However, smart contracts, which transact valuable tokens and cryptocurrencies, are compiled to very low-level bytecode. This bytecode is the ultimate semantics and means of enforcement of the contract.


We present the Gigahorse toolchain. At its core is a reverse compiler (i.e., a decompiler) that decompiles smart contracts from Ethereum Virtual Machine (EVM) bytecode into a high- level 3-address code representation.

[Research Article, distinguished paper award at OOPSLA'18 conference]
Ethereum is a distributed blockchain platform, serving as an ecosystem for smart contracts: full-fledged inter- communicating programs that capture the transaction logic of an account. Unlike programs in mainstream languages, a gas limit restricts the execution of an Ethereum smart contract: execution proceeds as long as gas is available. Thus, gas is a valuable resource that can be manipulated by an attacker to provoke unwanted behavior in a victim’s smart contract (e.g., wasting or blocking funds of said victim). Gas-focused vulnerabilities exploit undesired behavior when a contract (directly or through other interacting contracts) runs out of gas. Such vulnerabilities are among the hardest for programmers to protect against, as out-of-gas behavior may be uncommon in non-attack scenarios and reasoning about it is far from trivial.