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

SaTC：核心：中：协作：编写高保证智能合约的自动支持

• 批准号: 1801369
• 负责人: Bryan Parno
• 金额: $ 80万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-08-01 至 2023-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1801369&HistoricalAwards=false
• 关键词: SaTC; CORE; Medium; Collaborative; Automated

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.

由比特币和以太坊等加密货币普及的智能合约是在财务基础架构上运行并根据用户定义的算法来指挥货币流的计划。 此类合同可以实施新的，分散的金融工具，甚至可以通过编程来管理其行为的智能合约来定义的新型金融工具，甚至可以实施虚拟公司。 例如，像eBay一样的智能合约可以直接将买方与卖方联系起来，支持各种拍卖机制，并管理必要的付款（包括托管），而没有eBay，PayPal和信用卡公司目前征收的交易费用。 通常，将业务流程转移到智能合同中有望通过消除中介和自动化定居点来降低成本，减少摩擦和释放创新。但是，编程智能合约需要对密码技术，非标准的执行成本模型和经济机制设计有深入的了解。 现有的智能合同编程语言对这种推理几乎没有支持；实际上，合同漏洞（例如Thedao）已经导致了数百万美元的盗窃案。 相比之下，该项目将开发新的技术和工具来支持高保证智能合约的开发，重点是使这些合同特别难以正确写入的挑战。此项目将解决编写高级智能合约的独特挑战，即通过编写高级智能语言来设计新的高级语言，既可以稳固，又可以表达其整体构成的限制（其范围及其构成的构成（Exect）（Exect）（Exect of Contern Insection）（Exects e。同步性或保密要求或经济期望）。 我们将开发工具来分析和编译此类合同到可执行的代码中。在高级，固化的情况下，将支持三个维度上的高保证智能合同写作。 首先，固化将自动和注释驱动的汇编与提供安全智能合约所需的必要的一组基础加密原始图。 汇编过程将与用于自动资源分析的工具集成在一起，该工具将计算出智能合约使用的气体量的紧密界限。 反过来，资源分析将使自动推理有关高级属性，尤其是具有经济风味的物业。 例如，鉴于合同，使用概率资源分析的新分析工具将通过遵循协议来确定玩家的预期收益是否最大化，表明它是否兼容了奖励。 跨合同扩展分析将评估是否了解和减轻系统性风险。 该项目在高保证智能合约中的基础工作将有助于实现区块链技术的愿景。此外，智能合同编程还为教学安全提供了独特的教学机会。因此，研究结果将纳入研究生安全课程，智能合同的安全MOOC以及针对K-12教师的推广计划中。该奖项反映了NSF的法定任务，并被认为是值得通过基金会的知识分子的评估来支持的，并具有更广泛的影响。

项目成果

Probabilistic Resource-Aware Session Types

• DOI: 10.1145/3571259
• 发表时间: 2020-11
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Ankush Das;Di Wang;Jan Hoffmann

Raising expectations: automating expected cost analysis with types

• DOI: 10.1145/3408992
• 发表时间: 2020-06
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Di Wang;David M. Kahn;Jan Hoffmann

Blockchains Enable Non-Interactive MPC

• DOI: 10.1007/978-3-030-90453-1_6
• 发表时间: 2021
• 作者: Vipul Goyal;Elisaweta Masserova;Bryan Parno;Yifan Song

Galápagos: Developing Verified Low-Level Cryptography on Heterogeneous Hardware

Galápagos：在异构硬件上开发经过验证的低级密码学

• 发表时间: 2023
• 期刊: Proceedings of the ACM Conference on Computer and Communications Security (CCS
• 作者: Zhou, Yi;Gibson, Sydney;Cai, Sarah;Winchell, Menucha;Parno, Bryan
• 通讯作者: Parno, Bryan

Central moment analysis for cost accumulators in probabilistic programs

• DOI: 10.1145/3453483.3454062
• 发表时间: 2021-06
• 期刊: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
• 作者: Di Wang;Jan Hoffmann;T. Reps