摘要:智能合约是实现各类区块链应用的核心软件程序.近期，以太坊区块链平台（Ethereum）上的智能合约暴露出大量错误和安全隐患，在国际上引发了智能合约形式化验证的研究热潮.为提供高可信度的验证结果，智能合约程序语言的形式化必不可少.对以太坊中间语言Yul进行形式化，首次给出了其类型系统和小步操作语义的形式化定义.该语义为可执行语义（executable semantics），由120个Yul语言程序组成的测试集进行测试.该工作在Isabelle/HOL证明辅助工具中完成，为基于定理证明的智能合约正确性、安全性验证奠定了基础.
Abstract:Smart contracts are key software components of blockchain applications. Recently, a great number of bugs and security vulnerabilities have been exposed in smart contracts on the Ethereum blockchain. This resulted in extensive research efforts in the formal verification of smart contracts at the international level. To obtain highly trustworthy verification results, the formalization of programming languages for smart contracts is necessary. This work formalizes Yul-the Ethereum intermediate language. The core of this formalization consists of the first formal definitions of the type system and the small-step operational semantics for Yul. The semantics is executable, and it is validated using a test suite of 120 Yul programs. The proposed formalization is performed in the Isabelle/HOL proof assistant. It lays a solid foundation for the formal verification of the correctness and security of Ethereum smart contracts through theorem proving.
PDF全文下载地址:
http://jos.org.cn/jos/article/pdf/6246
删除或更新信息，请邮件至freekaoyan#163.com(#换成@)
以太坊中间语言的可执行语义
本站小编 Free考研考试/2022-01-02
相关话题/智能 程序 语言 软件 基础
领限时大额优惠券,享本站正版考研考试资料!
优惠券领取后72小时内有效，10万种最新考研考试考证类电子打印资料任你选。涵盖全国500余所院校考研专业课、200多种职业资格考试、1100多种经典教材，产品类型包含电子书、题库、全套资料以及视频，无论您是考研复习、考证刷题，还是考前冲刺等，不同类型的产品可满足您学习上的不同需求。 ...考试优惠券 本站小编 Free壹佰分学习网 2022-09-19面向MSVL的智能合约形式化验证
摘要:智能合约是运行在区块链上的计算机协议，被广泛应用在各个领域中，但是其安全问题层出不穷，因此在智能合约部署到区块链上之前，需要对其进行安全审计.然而，传统的测试方法无法保证智能合约所需的高可靠性和正确性.说明了如何使用建模、仿真与验证语言（MSVL）和命题投影时序逻辑（PPTL）对智能合约进行建 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02面向持续软件工程的微服务架构技术专题前言
摘要:随着软件互联网化和服务化的高度发展,持续性(continuity)成为现代软件系统的基本特性之一,覆盖从商业策划、软件开发、运维、演化的所有环节,使得软件系统在持续稳定提供功能和服务的同时,软件系统的边界和内部结构始终处于不断变化、持续更新和适应之中,持续软件工程(continuoussoft ...中科院软件研究所 本站小编 Free考研考试 2022-01-02程序智能合成技术研究进展
摘要:近年来，随着信息技术快速发展，软件重要性与日俱增，极大地推动了国民经济的发展.然而，由于软件业务形态越来越复杂和需求变化越来越快，软件的开发和维护成本急剧增加，迫切需要探索新的软件开发模式和技术.目前，各行业在软件活动中积累了规模巨大的软件代码和数据，这些软件资产为软件智能化开发建立了数据基础 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02面向智能攻击的行为预测研究
摘要:人工智能的迅速发展和广泛应用促进了数字技术的整体跃升.然而，基于人工智能技术的智能攻击也逐渐成为一种新型的攻击手段，传统的攻击防护方式已经不能满足安全防护的实际需求.通过预测攻击行为的未来步骤，提前部署针对性的防御措施，可以在智能攻击的对抗中取得先机和优势，有效保护系统安全.首先界定了智能攻击 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02面向领域的软件系统构造与质量保障专题前言
摘要:软件是推动新一代信息技术发展的驱动力.随着互联网、云计算、人工智能等技术的快速发展,软件与物联网、区块链、自动驾驶等众多领域的融合进一步加强,正引领并促进这些领域向数字化、智能化发展,为社会、经济的加速演进和创新发展带来了新的契机.因此,面向领域的软件技术不仅是软件领域,也是众多其他领域国内外 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02融合代码与文档的软件功能特征挖掘方法
摘要:在软件复用过程中，简洁、清楚的软件功能自然语言描述是帮助复用者快速了解待复用软件项目/代码库的前提和基础.但当前开源软件往往缺乏高质量的软件功能说明文档，使得这一过程变得更加复杂和困难.为此，提出了一种融合代码与文档的软件功能特征挖掘方法.该方法以动宾短语的形式描述软件功能特征，通过迭代挖掘软 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02支撑人工智能的数据管理与分析技术专刊前言
摘要:近年来,支撑人工智能的数据管理与分析技术正成为大数据和人工智能领域研究的热点问题之一.利用和发展数据管理与分析理论技术,为提升人工智能系统全生命周期的效率和有效性提供基础性支撑,必将进一步促进基于大数据的人工智能技术发展与其在更大范围的推广应用.本专刊聚焦在数据管理与人工智能融合发展的过程中, ...中科院软件研究所 本站小编 Free考研考试 2022-01-02KGDB:统一模型和语言的知识图谱数据库管理系统
摘要:知识图谱是人工智能的重要基石，其目前主要有RDF图和属性图两种数据模型，在这两种数据模型之上有数种查询语言.RDF图上的查询语言为SPARQL，属性图上的查询语言主要为Cypher.10年来，各个社区开发了分别针对RDF图和属性图的不同数据管理方法，不统一的数据模型和查询语言限制了知识图谱的更 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02PandaDB:一种异构数据智能融合管理系统
摘要:随着大数据应用的不断深入，对大规模结构化/非结构化数据进行融合管理和分析的需求日益凸显.然而，结构化/非结构化数据在存储管理方式、信息获取方式、检索方式方面的差异给融合管理和分析带来了技术挑战.提出了适用于异构数据融合管理和语义计算的属性图扩展模型，并定义了相关属性操作符和查询语法.接着，基于 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02基于人工智能方法的数据库智能诊断
摘要:数据库是一种非常重要和基础的计算机系统软件，随着数据库在各行各业的广泛应用，越来越多的人开始关注数据库运行的稳定性.由于各种各样内部或是外部作用的影响，数据库在实际运行的过程中会出现性能异常，而这可能会带来巨大的经济损失.人们大多通过观察监控指标信息来进行数据库异常诊断，但是关于数据库监控指标 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02
