June 21, 2021


Dedicated Forum to help removing adware, malware, spyware, ransomware, trojans, viruses and more!

Phoenix: A Formally Verified Regenerating Vault. (arXiv:2106.01240v1 [cs.CR])

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.