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.