智能合约的形式验证

以太坊是一个加密货币框架，利用区块链技术提供一个开放的全球计算平台，称为以太坊虚拟机（EVM）。EVM在一个简单的堆栈机器上执行字节码。程序员通常不会编写EVM代码；相反，他们可以用一种类似于JavaScript的语言进行编程，称为Solidity，该语言编译为字节码。由于EVM的主要目的是执行管理和转移数字资产（称为以太币）的智能合约，因此安全性至关重要。然而，编写安全的智能合约可能非常困难：由于以太坊的开放性，程序和假名用户都可以调用其他程序的公共方法，导致受信任和不受信任代码的潜在危险组合。最近，一次对TheDAO合约的攻击说明了这个风险，该攻击利用了EVM语义的微妙细节，将大约5000万美元的以太币转移到攻击者的控制之中。