Phoenix：一种形式化验证的可恢复金库

攻击者一旦获取加密货币用户的私钥，便可冒用其身份执行任意操作。由于大多数加密货币的去中心化特性，任何实体都无法撤销这些操作。这是去中心化系统面临的一个核心挑战，众多备受瞩目的盗窃事件即为例证。金库合约（vault contract）通过对操作引入人为延迟来降低此风险，使合约所有者在延迟期间能够中止操作。然而，密钥被盗仍会导致金库无法使用并使资金面临风险。我们提出 Phoenix，一种新颖的合约架构，允许用户在密钥丢失后恢复其安全属性。Phoenix 利用用户将密钥存储于易获取但安全性较低的存储（二级存储）以及更难访问但更安全的存储（一级存储）的能力。与以往方案不同，用户在二级密钥被盗后可恢复 Phoenix 的安全性，且无论哪一级密钥丢失都不会损失资金。Phoenix 还引入了一种机制，以降低一级密钥泄露时攻击者所能造成的损害。我们形式化地规定了 Phoenix 所需的行为，并提供了 Phoenix 作为以太坊合约的原型实现。由于此类实现高度敏感且易受细微漏洞影响，我们应用形式化验证工具来证明特定的代码属性并识别故障。我们重点指出了该工具发现的一个可被攻击者利用以攻破 Phoenix 的漏洞。修复该漏洞后，工具证明了底层可执行代码的正确性。