基于FSM的复合智能合约安全验证方法

沙特国王大学学报一种基于FSMMouhamad Almakhoura，b，Mr. J.，Layth Slimanc，Abed Ellatif Samhatb，Abdelhamid Melloukaa巴黎东克雷泰伊大学LISSI-TincNET研究小组，法国b黎巴嫩大学工程学院-CRSI，大学校园，Hadath，黎巴嫩cEFREI，巴黎先贤祠阿萨斯大学，法国阿提奇莱因福奥文章历史记录：收到2022年2022年7月7日修订2022年8月25日接受2022年9月6日在线发布保留字：复合智能合约有限状态机验证安全正确性A B S T R A C T今天的许多智能合约是在区块链上运行的自我执行程序。在这种情况下，复合智能合约用于表示协作业务流程。复合智能合约是一种需要使用外部调用来执行其他合约以实现其任务的智能合约。复合智能合约通过使用外部调用和执行可能属于其他所有者或公司的其他智能合约，在安全要求方面带来了许多挑战。因此，必须做出特别努力来确保复合智能合约的安全验证。在本文中，我们提出了一种新的方法来验证以太坊区块链中以solidity编写的复合智能合约的安全性和正确性。该方法基于有限状态机模型和模型检测方法分别对复合智能合约进行建模和验证。我们考虑了七个安全属性以及依赖于复合智能合约中要检查的合约上下文的安全问题。为此，我们提供了两种不同但互补的验证类型。第一种类型的验证应用于所有智能合约，其属性在我们的方法中称为“标准属性”，代表通用属性，而第二种类型考虑我们称为“特定属性”的上下文相关属性，这些属性在智能合约之间有所不同。最后，我们使用计算树逻辑公式表示所有属性，并使用nuXmv符号模型检查器来验证模型的所有属性。这种方法使用不同的solidity智能合约集进行验证©2022作者（S）。由爱思唯尔公司出版代表沙特国王大学这是一个开放的访问CC BY-NC-ND许可证下的文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。1. 介绍2009年，区块链首次提出了比特币，这是第一种使用分散式无信任系统在分布式账本中记录比特币交易的加密货币（Nakamoto，2008）。很快，根据Swan（2015）加密货币是*通讯作者。电子邮件地址：mouhamad. u-pec.fr（M. Almakhour），layth.slima-n@efrei.fr（ L.Sliman ） ， samhat@ul.edu.lb （ A.E.Samhat ） ， mellouk@u-pec.fr（A.Mellouk）。沙特国王大学负责同行审查区块链带来的创新之一。2015年，区块链的第二个创新“智能合约”（SC）出现。这个术语出现在以太坊区块链（Buterin，2013）中，它具有通过智能合约构建分布式应用程序的编程语言，并以图灵完备编程语言为标志（Antonopoulos和Wood，2018）。今天，以太坊是使用最广泛的平台，用于编程和运行智能合约，其语言名为Solidity ， 灵 感 来 自 C++ ， JavaScript 和 Python （ 以 太 坊 ，2022）。智能合约是一种计算机代码，旨在强制执行两方或多方之间的交易程序代码是自我执行的。它被部署为区块链上的任何交易。因此，不可能修改已部署的智能合约随着智能合约在业务流程应用中的使用越来越多，安全验证的需求也越来越大。事实上，任何智能合约失败或安全漏洞都可能导致巨大的损失，并导致全球恐慌，因为2000多个https://doi.org/10.1016/j.jksuci.2022.08.0291319-1578/©2022作者。由爱思唯尔公司出版代表沙特国王大学这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。制作和主办：Elsevier可在ScienceDirect上获得目录列表沙特国王大学学报杂志首页：www.sciencedirect.comM. 阿尔马克霍尔湖Sliman，A.E.Samhat等人沙特国王大学学报71加密货币的市值超过2万亿美元，数千个项目、公司、平台、政府、医疗机构、社交媒体以及最近使用区块链和智能合约的Metaverse。此外，在复合智能合约的背景下，智能合约使用外部调用执行其他合约以实现其任务，确保安全要求的需求变得不可或缺，因为复合智能合约通过外部调用带来复杂的安全问题。事实上，外部调用代表了很高的安全风险，因为被调用的智能合约的上下文和结构通常是未知的。因此，必须验证许多附加的安全属性。例如，我们可以提到访问权限违规，恶意代码执行，可重入性，可见性，智能合约状态更改，DoS和合约原子性。Solidity外部调用分为SomeMethods（））和SomeAddress.call对于“合约调用”，我们可能会通过调用由外部第三方管理的不受信任的合约来执行恶意代码或导致访问控制违规。此外，即使外部合约本身不是恶意的，它也可以包括外部调用，从而调用执行恶意代码或违反访问控制策略的其他智能联系人（可见性问题）。对于“原始调用”，如以太发送函数调用外部智能合约的回退函数的情况;这可能会引入问题，因为恶意代码可能嵌入回退函数中。通常，攻击者可以强制执行合同向他们发送以太币，或者执行允许他们进行DoS攻击的恶意代码，改变智能合约状态，进行重入攻击，或者在合同中获取控制流。在本文中，我们专注于在以太坊平台上以solidity编写的复合智能合约的背景下验证安全性，因为它是最受欢迎的智能合约编码。我们从智能合约开始，逐渐从一个到复合。特别是，这项工作的重点是验证和避免可重入性，访问控制，可见性，拒绝服务，算术正确性，流动性，原子性和数据暴露以及“上下文相关”的为此，我们提出了一种新的方法来验证复合智能合约的安全性和正确性。该方法基于有限状态机（FSM）对复合智能合约进行建模，并使用符号模型检查器对FSM模型进行验证。在本文中，我们的目标是用两种类型的验证来验证复合智能合约的安全性。在第一种类型中，我们考虑七个安全属性作为所有智能合约验证的标准属性，而在第二种类型中，我们提供了一组特定的安全属性，这些属性由基于智能合约上下文的所有的属性都写在计算树逻辑公式中，这是一种严格的形式化规范语言（Emerson，1990）。最后，我们使用符号模型检查器来验证模型是否满足这些性质。本工作的主要贡献如下：我们将Solidity智能合约建模为有限状态机（FSM）。我们提供了一组算法，用于从solidity代码转换到FSM，覆盖了大多数solidity语法。我们使用两种类型的安全验证：标准和特定属性。作为第一类型验证（标准属性），我们提供了一些类型的漏洞，被归类为具有基于有限状态机的安全属性的关系的我们通过提取漏洞逻辑，为每个安全属性设计并实现FSM漏洞，然后我们将它们转换成预定义的CTL公式（Emerson，1990;Clarke and Emerson，1981）。作为第二种类型的验证（特定属性），我们根据用户定义的复合智能合约的上下文定义了一个安全属性列表，并以CTL编写，以增强验证。我们提供了一个使用符号模型检查器nuXmv（Cavada等人，2014），以验证FSM-SC模型对属性。本文的其余部分组织如下，在第2节中，我们介绍了与智能合约验证相关的工作然后，我们详细介绍了第3节中提出的方法，包括提出的体系结构和不同的阶段，以及定义的转换和安全属性的算法第4节中介绍了使用复合智能合约实例及其结果的实施和实现测试。最后，第五部分对本文进行了总结。2. 相关工作我们的方法是基于有限状态机模型和模型检测方法分别建模和验证的复合智能合约。智能合约的定义是FSM性质（以太坊，2022），其中合约是在区块链上运行的自执行代码，并提供一组功能，允许合约或用户调用操作并更改智能合约的状态。基本上，代码表示不同的条件语句（if/when. . 然后），描述未来交易的可能动作，并根据它，智能合约触发下一个动作（Dolev等人，2020年）。换句话说，智能合约基于状态、动作和条件的逻辑，其中智能合约可以被视为在其生命周期内从初始状态开始到其最终状态的若干状态之间的转换（FranzVolland等人，2018年）。此外，由于我们正在研究复合智能合约，需要了解不同级别（原子和复合智能合约）的所有状态，FSM是智能合约建模的最佳选择，因为它提供了反映其行为的合适抽象级别（Mavridou和Laszka，2018）。值得注意的是这有助于我们在建模阶段提供更准确、更接近现实的智能合约模型。为了验证，提出了许多工具来验证智能合约的安全性和正确性。这些工具根据包括符号执行的验证方法而变化（Luu等人，2016; Chen等人，2017），模型检查（Lahiri等人，2018; Bai等人，2018），抽象解释（布伦特等人，2018; Grech等人，2018），定理证明（Amani等人，2018;Grishchenko等人，2018）或Fuzzing（Liu等人，2018; Jiang等人，它们在分析类型（静态或动态分析）、级别（实体代码或字节码）和上下文（Angelo等人，2019;Praitheeshan等人，2019; Liu和Liu，2019;Almakhour等人，2020年）。这些工具中的大多数都专注于对一个智能合约的验证。据我们所知，有一些基于FSM的方法旨在验证复合智能合约的正确性，但不是其安全性。在本节的其余部分，我们将介绍基于FSM的类似方法，用于验证一个或复合智能合约。FsolidM（Mavridou和Laszka，2018）是一个设计安全以太坊智能合约的框架。该工具提供了一个正式的FSM-SC模型，一个用于创建FSM的图形编辑器，●●●●●●●M. 阿尔马克霍尔湖Sliman，A.E.Samhat等人沙特国王大学学报72cally以转换系统的形式生成了一个solidity代码（Mavridou和Laszka，2018）。此外，有四个插件，一旦选择了一个插件，该工具会生成一个预定义的代码，并添加最后生成的代码。锁定插件和转换计数器插件通过预定义的用于锁定智能合约的修饰符来防止可重入性和不可预测的状态脆弱性，并分别在所有函数中添加转换计数器VeriSolid（Mavridou等人， 2019）是一个建立在WebGME之上的开源框架（Maróti等人， 2014）和FSolidM（Mavridou和Laszka，2018）。VeriSolid是一个采用正确设计方法开发智能合约的框架首先，从转换系统或Solidity代码中，该工具从Mavridou和Laszka（2018）中定义的转换系统生成一个称为增强转换的模型。其次，VeriSolid自动将生成的过渡系统写入BIP模型（Basuet al.，2011; Basu等人， 2006）并触发BIP-to NuSMV工具（Saab ，2015）以获取smv代码。然后，用户在时态逻辑CTL中形式化属性（Emerson，1990）。最后，nuXmv模型检查器（Cavada等人，2014）用于验证smv代码是否满足CTL属性。当满足所有属性时，生成等效的实体代码。此外，存在VeriSolid的扩展（Nelaturu等人，2020）来处理交互智能合约。在Bai等人（2018）中，通过将形式化方法应用于智能合约，提供了一个智能合约模板，以便通过有限状态机来表示它。作者使用了一种名为“PROMELA”的验证建模语言（Mikk等人，1998）来对购物智能合约（SSC）进行建模（Bai等人，2018），然后使用模型检查器SPIN验证它们的正确性（Mikk等人， 1998年）。Alqahtani等人（2020）的工作提出了一种智能合约的验证方法，将SC建模为FSM，并使用NuSMV模型检查器来检查功能需求。该工具与Hyperledger Fabric（Androulaki等人，2018），并接受用Go语言编写的SC作为输入。此外，使用BIP框架对SC之间的相互作用进行建模（Basu等人， 2011年）。他们使用线性时序逻辑LTL来形式化属性，并使用bip-to-nusmv工具（Saab，2015）将BIP模型转换为SMV代码。上述工作都没有考虑复合智能合约的安全性，特别是外部调用导致的安全问题。虽然，在Mavridou和Laszka（2018）和Mavridou等人（2019），他们引入了旨在生成正确的Solidity代码的设计正确工具（代码生成器工具），引入的工具不考虑生成的智能合约的验证。FsolidM（Mavridou和Laszka，2018）使用两个插件生成了一个安全的智能合约，以避免可重入性和不可预测的状态漏洞，而不会发现它们的发生。 另一方面，VeriSolid（Mavridou等人， 2019年），这是FsolidM的扩展，仍然具有相同的最终目标，即生成正确的智能合约，但具有更多功能。VeriSo- lid提供CTL时序逻辑中属性的形式化，并针对智能合约的FSM模型进行验证，以确保其正确性并生成等价的无错误的坚固代码。在验证点中，在Bai etal. （2018），他们使用只支持LTL时态逻辑的SPIN模型检查器来提供属性，并且他们只在一个SC级别上验证智能合约的正确性。最后，在Alqahtani等人的工作。（2020）是一种用于超级账本结构区块链的特定方法，用于验证复合SC的正确性。它使用LTL时态逻辑来创建功能属性，并且不旨在检查安全问题。我们的目标是介绍一种方法，提供验证的正确性和安全性的复合SC的新方法必须使用CTL时序逻辑，这是更严格和有效的比LTL。此外，该方法必须验证用户根据合同上下文定义的特定属性，而不仅仅是SC的典型安全属性，如访问控制，拒绝服务，可重入性等。在下一节中，我们将解释我们提出的方法。3. 使用FSM的为复合智能合约验证设计的拟议方法如图1所示。使用FSM测试SC有助于验证它是否符合其规格。 对于一个或复合SC验证，我们的建议是基于将智能合约可靠性代码建模为有限状态机来描述它的行为。为此，我们的方法有三个阶段：建模，正式规格说明和验证。四个主要部分：Solidity源代码、FSM、属性和符号模型检查器.Fig. 1. 建议的架构。M. 阿尔马克霍尔湖Sliman，A.E.Samhat等人沙特国王大学学报73222建模阶段为我们提供了FSM模型，我们需要使用我们的转换算法（第3.1节）来验证该模型。它由三个主要模块组成：solidity源代码，SOL到BIP和BIP到SMV。SOL-to-BIP块代表我们自己的工具1，它将solidity代码自动转换为BIP模型该工具的工作是用有限状态机对Solidity代码进行建模，根据我们提出的子块建模到有限状态机的转换算法得到子块FSM-SC模型。然后，它生成BIP-SC模型作为表示我们的FSM-SC模型的可执行代码（子块BIP-SC）。我们使用BIP平台的形式语言（Basu等人，2011）作为一种中间语言。BIP语言允许我们以简单的方式编写FSM模型，其中我们可以不复杂地定义变量、状态和转换，例如，“on transition1 from state1 to state2 provided（C）do（a）”（Basu等人，2011年）。此外，SOL-to-BIP工具的编程和创建来自于节省时间和避免建模阶段错误的需要，特别是在复合智能合约（数千个solidity行代码）的情况下，以及不熟悉FSM和BIP模型的用户的情况下。请注意，FSM模型可以用smv语言编写，而无需通过BIP模型。但是，编写大型代码更有效，BIP，特别是当有一个名为BIP-to-NuSMV的java工具时（Noureddine等人，2015; Saab，2015），它将BIP模型转换为smv代码，这是我们模型检查器的输入语言。该工具用块BIP-to-SMV表示。另一方面，对于FSM变换的正确性BIP-SMV，我们对FSM-BIP执行一对一的转换，其中，我们的FSM模型由状态，转换，守卫和动作组成。相反，BIP模型由代表SC的组件组成，每个组件都有一组状态和转换，以及保护和操作。因此，我们只需要将BIP模型的变量替换为FSM变量，就可以得到表示FSM模型的可执行代码。这实现了我们从FSM到BIP转换的正确性，而无需证明它。此外，Noureddine等人的作者。（2015）先前证明BIP-to-NuSMV工具（Saab，2015）转换的正确性，确保我们模型的正确性第二阶段是正式规范（第3.2节），负责提供合约属性，以验证一个或复合智能合约的安全性和正确性。因此，我们的方法提供了两种类型的属性：安全性和正确性属性。对于SC安全性，我们的方法基于两种类型的安全属性（标准和特定）通过两种类型的验证来验证智能合约的安全性。这两种类型是不同的但互补的层次和目标以涵盖整个复合智能合约安全属性范围。对于第一种类型的验证，我们预定义了多达七个安全属性，作为所有智能合约的标准属性。我们提供了一些类型的漏洞，被归类为具有与安全属性的关系的检测。为此，安全属性块提取每个安全属性的漏洞逻辑。然后，利用对FSM块的建模，将这些逻辑建模为子FSM，得到FSM-漏洞。在CTL公式块中，我们用CTL公式将FSM-脆弱性转换为书面模式（Emerson，1990）。在第二种类型的验证中，是由用户根据复合SC上下文使用用户定义块定义的一组安全属性。然后，它通过CTL公式块用公式表示。对于SC正确性，正确性属性块从合同规范块中获取规范，然后用户将这些属性定义为CTL时序逻辑的公式1https://github.com/Smart-Contracts-Verification/A-Verification-Approach-for-Composite-Smart-Contracts-Security-using-FSM通过CTL公式块。第三个阶段称为验证（第3.3节），我们使用nuXmv符号模型检查器来验证建模阶段的FSM-SC与正式规范化阶段的CTL公式提供了一份报告，其中包含发现的漏洞以及每个不满意属性的反例该解决方案还旨在验证复合智能合约的安全性。3.1. 建模阶段验证过程从将复合智能合约建模为有限状态机开始。我们根据我们为此编写的转换算法我们通过元组S;s0;C;V;T来定义FSM-SC，其中：- S是有限状态的集合;- s0是初始状态的集合;- Cconstructors0;- V是一组合同变量;- T是一组转换，其中每个转换t2T包括：名称t名称;来源t从 S;目的地tt0S;警卫t警卫;行动a;3.1.1. 智能合约到FSM在本节中，我们提供了我们提出的转换算法来将复合SC建模为FSM。根据转换算法，实体代码中的每一行这些算法覆盖了最坚固的语法。算法1将算法2和算法3结合起来构建并返回FSM-SC。对于合同函数和变量，算法2用于定义初始状态和函数状态。每个函数都将成为一个以solidity函数名命名的状态。在每个函数状态之后，都有状态来确定函数的可见性（例如：public，external）。然后，算法3定义了SC函数体到状态和转换及其参数在我们的FSM模型中的转换。因此，在最后，SC的建模将为我们提供一个包含每个SC的有限状态机的状态转换系统。除了精确的状态和它们的转换的算法之外，我们预定义了一些实体语句的状态名称作为我们的建模阶段的一部分，如算法所示。这有助于我们推广验证模型。通过应用这些算法，图。图2显示了实体性语句的例子以及它们转换成状态的例子。首先，正如我们在图2的顶部所看到的，合约函数，其中智能合约中的每个函数都将成为从称为“调用”的初始状态到称为“函数名称”的状态的转换此外，函数的可见性将成为一个状态，其名称状态‘‘如果任何函数包含内部或外部调用函数，则算法3分别 在 SC 上 添 加 状 态 “callfunction/externalcallfunction_functionName“和从函数调用状态到函数调用状态的转换。对于条件语句”if，require，assert“，我们的算法将它们中的每一个建模为3个状态和 2个转换，一个提到语句的名称，例如 ”ifcondition ，requirecondition或assertcondition“，并且2个状态用于条件和！条件，以分别指示可接受和拒绝条件。此外，在我们的方法中，循环也被标记为三种状态：此外，solidity函数M. 阿尔马克霍尔湖Sliman，A.E.Samhat等人沙特国王大学学报74图二. 算法解释。函数名。另一方面，发送以太函数最后，我们指定加法作为输入。最后，我们使用BIP-to-NuSMV java工具（Saab，2015）获得smv代码。在下一节3.1.2中，我们将向您展示一个实体代码及其FSM-SC模型的示例和减法数学运算2状态称为减法(var 1，var 2）和加法（var 1，var 2）。var 1和var 2的符号表示操作的变量在定义每个SC的FSM之后，我们使用BIP平台的形式语言（Basu等人，2011）作为中间语言来建模我们的复合SC的FSM。每个SC将成为BIP模型中的原子组件。此外，BIP支持交互概念，它提供连接器来描述交互，算法1：智能合约FSM不同原子成分之间的相互作用，的数据.因此，连接器将表示SC之间的相互作用，即，外部调用在我们的情况下起作用我们自动-通过提供我们自己的用C#编写的SOL-to-BIP工具2来配合这个过程，该工具通过获取solidity源代码来2https://github.com/Smart-Contracts-Verification/A-Verification-Approach-for-Composite-Smart-Contracts-Security-using-FSM3.1.2. FSM的Solidity代码示例在本节中，我们将向您展示一个根据上面定义的算法从solidity代码转换为FSM的示例。下面的代码向我们展示了来自Swc Registry（2020）的名为SimpleDAO的智能合约的Solidity代码。因此，图3表示M. 阿尔马克霍尔湖Sliman，A.E.Samhat等人沙特国王大学学报75算法2：合约语句算法3：函数语句M. 阿尔马克霍尔湖Sliman，A.E.Samhat等人沙特国王大学学报76使用我们的转换算法的智能合约SimpleDAO的FSM模型。3.2. 形式规格阶段在智能合约中，我们将智能合约规范分为两类：安全属性和正确性属性。安全属性描述了我们如何维护智能合约的安全性。正确性属性描述智能合约验证其正确性的功能。由于我们的方法是基于模型检查器的，所以有不同的方法来表示合同规范，如计算树逻辑（CTL），线性时态逻辑（LTL），过去线性时态逻辑（PLTL）等.我们选择CTL逻辑来形式化我们的属性，并将其添加到FSM模型中以验证它. CTL（Clarke and Emerson，1981）是分支时态逻辑，通过考虑FSM中所有可能的同时执行来区分. CTL是具有路径量词的LTL的扩展，即，CTL将路径量词A（针对所有路径）和E（至少一条路径）与LTL运算符结合：X（下一条），F（最终），G（全局），直到。CTL公式的文法细节在Emerson（1990）、Clarke和Emerson（1981）以及Li et al. （2015年）。3.2.1. 使用FSM的在该方法中，我们使用这两种类型的验证来验证复合SC的安全性，通过提供这可以确保复合智能合约的安全性。对于标准属性，我们考虑检查七个安全属性：可重入性，访问控制，拒绝服务，算术正确性，流动性，原子性和来自Zipfel（2019）的数据暴露（2021），Manning（2018），Swc注册表（2020）。这个想法是寻找某些类型的漏洞，这些漏洞被归类为与安全属性有关系。如果存在漏洞，则表示相关属性未得到满足。为此，我们使用FSM从漏洞逻辑中提取FSM漏洞，以定义其CTL公式并将其添加为预定义的属性。在本小节的其余部分，我们将向您展示标准属性的坚固性示例，FSM（s）和错误解释。1. 重入它是在函数操作完成之前对调用合约的循环回调（在循环回调类型中，函数图三. FSM-DAO模型。●●M. 阿尔马克霍尔湖Sliman，A.E.Samhat等人沙特国王大学学报77！见图4。 可重入漏洞。函数下面是一个具有可重入性的Solidity代码及其FSM-可重入性以及CTL公式的示例。(a) Solidity代码示例：(b) 有限状态机FSM-可重入性（见图1） 4）：(c) CTL公式：在 所 有 路 径 中 ， 直 到 函 数 完 成 （ 操 作 ） 如 果 发 生“someAddres.call.value（）”，并且减法/置零操作是未来状态！bug.重入CTL公式：一个G的状态函数A！ E FFAG发送以太呼叫！AF状态 ¼减影a;b2. 接入控制我们考虑三个相关的漏洞来检查此属性：DELEGATECALL‘‘Delegatecall根据Swc登记研究（2020）和Wagner et al.调用不受信任的合约是非常危险的，因为目标地址的代码可以改变调用者的任何存储值，并完全控制调用者的余额。为此，我们的方法将任何“Delegetcall“函数视为(a) Solidity代码示例：(b) 有限状态机FSM-Delegatecall（见图10）（ 5）：(c) CTL公式：在所有路径中，是否使用了Delegetcall函数？这意味着，在所有可能的未来状态中，委托呼叫状态最终都会发生。DelegateCall CTL公式：AGEEF美国代表团电话通过“tx.origin“验证当使用“tx.origin“进行授权时为此，图五. 委托调用漏洞。●●M. 阿尔马克霍尔湖Sliman，A.E.Samhat等人沙特国王大学学报78(a) Solidity代码示例：(b) 有限状态机FSM-tx.origin（见图 6）：(c) CTL公式：至少，有一条路，如果有一个状态=ifconditionjrequirecondition，则下一个状态：tx：origin！''授权的tx.origin''。tx.origin CTL公式：例如，如果= requirecondition，则状态为¼！出口国：墨西哥：原产地：墨西哥联系我们无保护在合约不再有效或紧急情况下，solidity支持对于攻击者来说，他们只需要进入一个功能-包含“自毁”指令的协议(a) Solidity代码示例：(b) 有限状态机FSM-无保护自毁（见图）。 7）：(c) CTL公式：在所有路径中，如果在visibility=public的智能合约函数下使用自毁函数！bug.自毁CTL公式：AG州政府公开！EF状态自毁程序3. 拒绝服务对于拒绝服务，我们只考虑一个称为拒绝服务与意外恢复的漏洞。具有意外恢复的拒绝服务攻击之一是当您试图将以太币发送到一个错误的地址时，其交易取决于成功的资金转移。(a) Solidity代码示例：见图6。 Tx源漏洞。图7.第一次会议。不受保护的SELFDESCRIPCT漏洞。●●M. 阿尔马克霍尔湖Sliman，A.E.Samhat等人沙特国王大学学报79！9个月了！●见图8。带有（意外）恢复的FSM-DoS（场景1）。见图9。带有（意外）恢复的FSM-DoS（场景2）。(b) 具有意外恢复的有限状态机FSM-DoS（参见图8和图10）。 9）：(c) CTL公式：–至少有一条路径，其中状态= if/re-quire，则下一个状态=sending_ether_sendbug–至少，有一条路径，在state = loop语句条件下，循环体在require state depend on iteration loop中有一个send（）函数！ bug–在所有的路径中，是否存在state = address_send-ing_ether_ send！bug.具有意外还原CTL公式的DoSCTL1：AG_EF_OFF状态地址发送以太发送=呼叫=转移呼叫CTL2：EG状态循环！ 自动对焦处于循环状态！EFCTL 3：如果需要，则EG处于状态1/4！EX状态1/4地址发送以太发送jmsg：sender sending ethersend4. 流动性在任何时候，合同资金都可以转移给其他用户。为此，我们考虑两个相关的漏洞：以太锁和意外以太平衡。乙醚锁意思是不能取钱因为这个合同不会提供任何花钱的功能。(a) Solidity代码示例：(b) 有限状态机FSM-以太锁（见图 10）：(c) CTL公式：在所有路径中，如果有state = fallback（）或receive（），则下两个state分别为external和payable，和。=state= sending ether call =transfer =sendbug.醚锁CTL公式：AG将状态设为1/4回退接收！EG状态¼外部！按州交货价支付&AG（EF！（state=sending_ether_call/send/transfer））意外的以太币余额使用条件语句来检查余额“this.balance“的严格相等性●M. 阿尔马克霍尔湖Sliman，A.E.Samhat等人沙特国王大学学报80见图10。 以太锁漏洞。见图11。 意外的以太平衡漏洞。见图12。 上溢和下溢示例。一些指令比如该方法检测包含“this.balance“的比较表达式(a) Solidity代码示例：(b) 有限状态机FSM-意外以太平衡（见图） 11）：(c) CTL公式：至少，有一条路径，如果有state =（condition），那么下一个state=（this.balacne == value）！bug.意外的乙醚平衡CTL公式：如果j需要j断言条件，则EG将状态设置为¼！ EX状态此分类下一篇：balance5. 算术正确性对于算术运算，我们考虑两个漏洞：整数溢出和下溢。上溢/下溢当超过最大值或低于最小值时，分别会发生溢出和下溢。(a) Solidity代码示例（参见图 12）：(b) 有限状态机FSM-下/溢出（参见图13和图14） 14）：(c) CTL公式：●M. 阿尔马克霍尔湖Sliman，A.E.Samhat等人沙特国王大学学报81！！图十三.溢出漏洞。–在所有路径中，直到函数完成（动作），如果有一个状态=加法（a，b）和（a + b），则存在溢出错误–在所有路径中，直到函数完成（动作），如果有状态=减法（a，b）和（b> a）下溢错误溢出CTL公式：AG将状态改为功能名称&<！ AF加药a; b下溢CTL公式：AG显示状态<$函数&名称b> a显示！AF减影术a; b6. 原子性未检查的调用返回值是检查此属性时考虑的相关漏洞，可导致事务失败而不改变SC状态。未检查的调用返回值低级调用（因此，您应该始终检查返回值以处理失败的调用。(a) Solidity代码示例：(b) 有限状态 机FSM-未检查 的调用返回 值（见图1 ）。15）：(c) CTL公式：至 少 ， 有 一 条 路 径 ， 如 果 有 state=externalcontract.function（），那么下一个state！=状态状态！bug.未选中的调用返回值CTL公式：发送以太网发送地址=呼叫委托呼 叫 ！EX！如果j要求条件，请说明条件7. 数据暴露有些数据不应该公开。为此，我们通过函数默认可见性漏洞的存在来检查此属性。函数默认可见性Solidity将函数的可见性默认设置为public。例如，未经授权的用户可以访问一个函数并更改合同状态，如果它不是由开发人员指定的。(a) Solidity代码示例：(b) 有限状态机FSM-函数默认可见性（见图 16）：(c) CTL公式：在所有路径中，如果用户定义任何函数为关键函数，且未定义函数可见性！bug.函数默认可见性CTL公式：AG状态<$档功能1档j状态<$档功能 2档j状态1/4功能3/4 ！EX州<$公共图书馆3.2.2. SC–correctness verification using正如我们上面提到的，我们的方法使用CTL逻辑来表达属性。因此，SC的所有者提供一组属性以确保SC正确工作。然后，它通过将它们添加到smv文件或在单独的文件中提供它们来比如说，●●M. 阿尔马克霍尔湖Sliman，A.E.Samhat等人沙特国王大学学报82！（）×见图14。下溢脆弱性。图十五岁未检查的调用返回值漏洞。图16. 函数默认可见性漏洞。为了定义性质CTL规范可以帮助我们验证智能合约的正确性，并确保SC正确且按预期执行。3.3. 验证阶段验证阶段是我们的方法的最后阶段，在那里我们结合CTL公式的安全性和正确性与FSM-SC模型。为了验证，我们使用nuXmv符号模型检查器（Cavada等人，2014）自动检查模型是否满足安全属性，并允许用户定义任何其他属性并检查它。模型检查器在不满足规范时生成反例。4. 实施和验证我们使用Ubuntu Linux机器，4*i5（64位）CPU，32 GB内存。作为模型检查器，我们使用nuXmv版本2.0.0（Cavada等人，2014年）。我们已经验证了我们的方法与各种例子的固体代码。其中一些来自Ether.scan。此外，CTL公式已经通过包含DAO合约（首次出现可重入性的著名合约）等漏洞的典型示例以及被认为易受攻击并在不同来源中引用的函数示例（Swc registry，2020;Manning，2018;Zipfel，2021; Zipfel，2019）进行了验证，这些函数涉及收集和分类智能合约中的漏洞和攻击。所有示例和验证测试都可以在GitHub3上找到。4.1. 动机示例我们的方法旨在验证代表基于区块链的协作环境的复合智能合约的安全性，特别是在以太坊区块链中。为此，我们实现了一个用solidity编写的旅行社系统实例。这3https://github.com/Smart-Contracts-Verification/A-Verification-Approach-for-Composite-Smart-Contracts-Security-using-FSMM. 阿尔马克霍尔湖Sliman，A.E.Samhat等人沙特国王大学学报83图17.复合材料-SC示例。复合SC由五个智能合约组成：航班、酒店、汽车、搜索和预订。首先，创建SC-flight是为了管理航班，它用于通过查找最低航班价格来搜索航班此外，它还提供了4个其他函数：function_get通过传递一个id返回航班信息列表;function_create添加一个新的可用航班;function_book通过传递一个id进行航班预订并将航班状态更改为其次，SC酒店提供四个功能：获取，搜索，预订和创建。这些功能的工作原理类似于SC-航班功能逻辑，但在酒店环境中。另一方面，SC-car除了三个功能之外还定义了SC-search有一个名为searchTrip的功能，允许用户根据给定的价格搜索由航班、酒店和汽车组成的旅行。此SC进行外部函数调用，以通过优先级顺序搜索行程的元素。我们定义这个顺序：首先搜索航班，然后搜索酒店，最后搜索汽车。SC搜索将PriceTrip发送到SC航班，如果找到航班，则SC继续搜索具有剩余价格的酒店，并且汽车搜索也以类似的方式完成（参见图17）。最后，SC-book有三个独立的功能（预订航班、预订酒店和预订汽车），可以分别通过外部调用SC-flight、SC-hotel和SC-car进行预订 图图17展示了我们示例中总结的FSM和连接器。4.2. 执行在BIP模型中编写示例并将其转换为smv代码之后安全性验证是在两种不同的类型下完成的：标准属性和特定属性。首先，我们从第3.2节中预定义并表示为CTL公式的标准属性的验证开始。在这种类型中，我们可以检测到多达11个漏洞。验证报告显示，我们的方法在SC-飞行中检测到三个漏洞：溢出，功能默认可见性和未受保护的