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

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

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.