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

点击翻译按钮获取中文摘要

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.