SaTC: CORE: Medium: Collaborative: Automated Support for Writing High-Assurance Smart Contracts

由比特币和以太坊等加密货币推广的智能合约是运行在金融基础设施之上的程序，并根据用户定义的算法控制资金流动。这样的合约可以实现新的、去中心化的金融工具，甚至是虚拟公司，这些虚拟公司仅由一组以编程方式管理其行为的智能合约来定义。例如，类似eBay的智能合约可以直接连接买家和卖家，支持各种拍卖机制，并管理必要的付款（包括托管），而不需要eBay、PayPal和信用卡公司目前征收的交易费用。一般来说，将业务流程转移到智能合约中有望降低成本，减少摩擦，并通过消除中介和自动化结算来释放创新。然而，编写智能合约需要深入了解加密技术、非标准执行成本模型和经济机制设计。现有的智能合约编程语言很少支持这种推理；事实上，合约漏洞（如TheDAO）已经导致数百万美元的盗窃。相比之下，该项目将开发新的技术和工具来支持高保证智能合约的开发，重点是使此类合约特别难以正确编写的挑战。该项目将通过设计一种新的高级语言固化来解决编写高保证智能合约的独特挑战，该语言允许程序员表达合约的意图及其设计约束（例如，资源使用的界限，同步性或保密性要求，或经济预期）。我们将开发工具来分析并将这些合同编译成可执行的代码。在高层次上，固化将支持跨三个维度的高保证智能合约编写。首先，固化将自动和注释驱动的编译混合到一组不同的底层加密原语中，这些原语是提供智能合约所需的安全性所必需的。编译过程将与自动化资源分析工具集成，该工具将计算智能合约使用的天然气量的严格界限。反过来，资源分析将支持对高级属性的自动推理，特别是那些具有经济风味的属性。例如，给定一个合同，使用概率资源分析的新分析工具将确定玩家的预期收益是否通过遵循协议而最大化，表明它是否与激励相容。跨合同扩展分析将评估系统风险是否被理解和减轻。本项目在高保证智能合约方面的基础性工作将有助于实现区块链技术的愿景。此外，智能合约编程还为安全教学提供了独特的教学机会。因此，研究成果将被纳入研究生安全课程、智能合约安全MOOC以及面向K-12教师的外展计划。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Smart contracts, popularized by cryptocurrencies like Bitcoin and Ethereum, are programs that run atop financial infrastructure and command the flow of money according to user-defined algorithms. Such contracts can implement new, decentralized financial instruments or even virtual corporations defined only by the bundle of smart contracts programmatically governing their behavior. For example, an eBay-like smart contract could directly connect buyers with sellers, support a variety of auction mechanisms, and manage necessary payments (including escrow), without the transaction charges currently imposed by eBay, PayPal, and the credit card companies. In general, moving business processes into smart contracts promises to lower costs, reduce friction, and unleash innovation by eliminating intermediaries and automating settlements. However, programming smart contracts requires a deep understanding of cryptographic techniques, a non-standard execution cost model, and economic mechanism design. Existing smart-contract programming languages provide little support for such reasoning; indeed, contract vulnerabilities (such as TheDAO) have already led to multi-million-dollar thefts. In contrast, this project will develop new techniques and tools to support the development of high-assurance smart contracts, with an emphasis on the challenges that make such contracts particularly difficult to write correctly.This project will address the unique challenges of writing high-assurance smart contracts by designing a new high-level language, Solidified, that allows a programmer to express both the intent of the contract and its design constraints (e.g., bounds on resource usage, synchronicity or secrecy requirements, or economic expectations). We will develop tools to analyze and compile such contracts into executable code. At a high-level, Solidified will support high-assurance smart-contract writing across three dimensions. First, Solidified will mix automatic and annotation-driven compilation to a diverse set of underlying cryptographic primitives necessary to provide the security smart contracts require. The compilation process will be integrated with tools for automated resource analysis that will compute tight bounds on the amount of gas a smart contract uses. Resource analysis, in turn, will enable automated reasoning about higher-level properties, particularly those with an economic flavor. For example, given a contract, new analysis tools, using probabilistic resource analysis, will determine whether a player's expected payoff is maximized by following the protocol, indicating whether it is incentive compatible. Extending the analysis across contracts will evaluate whether systemic risks are understood and mitigated. This project's foundational work in high-assurance smart contracts will help realize the vision of blockchain technology. In addition, smart-contract programming also provides a unique pedagogical opportunity for teaching security. Hence, research results will be incorporated into graduate security courses, a smart-contract security MOOC, and an outreach program for K-12 teachers.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.