NSF-BSF: SHF: Small: Efficient, Automatic, and Trustworthy Smart Contract Verification

基于区块链的加密货币，如比特币和以太坊，正在变得越来越普遍，并且带来了巨大的希望：区块链提供了一个分散的分类账，而不是作为资金转移中间人的中心化金融机构，其中交易直接发生在其参与者之间。此类交易的范围从同行之间的简单转移到具有各种条件的复杂合同。这些被编写为被称为“智能合约”的计算机程序。“智能合约和区块链对世界经济的潜力是巨大的;然而，它们也带来了许多风险。智能合约对实际资产的直接影响需要高水平的保证，才能使这项技术得到广泛接受和信任。传统软件的验证方法无法验证智能合约，因此迫切需要调整这些方法并开发新技术，以便能够验证智能合约的正确性和安全性。本项目通过开发能够对智能合约进行推理的算法，并将其作为最先进的自动推理工具的一部分来实现，从而解决了这一挑战。该项目有三个主要目标：第一，开发用于推理嵌套数据库和序列的算法，这对于在区块链中建模智能合约的执行以及它们与更传统的数据结构的结合非常有用;第二，使用这些算法来推理真实世界的智能合约，并从中收集和开发挑战基准;第三，使用这些算法来推理真实世界的智能合约。第三，自动为智能合约的验证结果生成证明，这些证明可以独立检查，也可以合并到证明助手中。鉴于目前传统验证方法的局限性以及智能合约和区块链的快速发展，该项目旨在提高对该技术的信任，从而使其能够发挥其潜力。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Blockchain-based cryptocurrencies such as Bitcoin and Ethereum are becoming widespread, and come with great promise: instead of centralized financial institutions that act as middlemen for money transfers, blockchains offer a decentralized ledger, in which transactions occur directly between its participants. Such transactions can range from simple transfers between peers to complex contracts with various conditions. These are written as computer programs that are called "smart contracts." The potential of smart contracts and blockchains on the world economy is huge; however, they also carry many risks. The direct impact smart contracts have on actual assets requires a high level of assurance before this technology can be widely accepted and trusted. Verification methods for traditional software fall short in verifying smart contracts, and hence there is a pressing need to adapt these methods and develop new techniques in order to be able to verify the correctness and safety of smart contracts.This project addresses the challenge by developing algorithms capable of reasoning about smart contracts, and implementing them as part of state of the art automated reasoning tools. The project has three main objectives: first, developing algorithms for reasoning about nested datatypes and sequences, which are useful for modeling the execution of smart contracts within a blockchain, as well as for their combination with more traditional data structures; second, using these algorithms for reasoning about real-world smart contracts and collecting and developing challenge benchmarks from them; and third, automatically producing proofs for the verification results of smart contracts, which can either be checked independently or incorporated into proof assistants. Given the current limitations of traditional verification methods and the rapid growth of smart contracts and blockchains, this project intends to increase trust in this technology, which in turn can enable it to fulfill its potential.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.