Phoenix: A Formally Verified Regenerating Vault

TL;DR

Phoenix is a new Ethereum contract architecture that enhances security by allowing recovery after key loss and reducing damage from key compromise, with formal verification ensuring correctness.

Contribution

It introduces a novel vault design enabling key recovery and damage mitigation, supported by formal specification and verification of the implementation.

Findings

Formal specification of Phoenix's behavior

Identification and fixing of a security bug

Verified correctness of the final implementation

Abstract

An attacker that gains access to a cryptocurrency user's private keys can perform any operation in her stead. Due to the decentralized nature of most cryptocurrencies, no entity can revert those operations. This is a central challenge for decentralized systems, illustrated by numerous high-profile heists. Vault contracts reduce this risk by introducing artificial delay on operations, allowing abortion by the contract owner during the delay. However, the theft of a key still renders the vault unusable and puts funds at risk. We introduce Phoenix, a novel contract architecture that allows the user to restore its security properties after key loss. Phoenix takes advantage of users' ability to store keys in easily-available but less secure storage (tier-two) as well as more secure storage that is harder to access (tier-one). Unlike previous solutions, the user can restore Phoenix security after the theft of tier-two keys and does not lose funds despite losing keys in either tier. Phoenix also introduces a mechanism to reduce the damage an attacker can cause in case of a tier-one compromise. We formally specify Phoenix's required behavior and provide a prototype implementation of Phoenix as an Ethereum contract. Since such an implementation is highly sensitive and vulnerable to subtle bugs, we apply a formal verification tool to prove specific code properties and identify faults. We highlight a bug identified by the tool that could be exploited by an attacker to compromise Phoenix. After fixing the bug, the tool proved the low-level executable code's correctness.