智能合约的形式化验证
上次编辑: , Invalid DateTime
智能合约让用户能够创建去中心化、无需信任和稳健的应用程序,给用户提供新的用例并解锁价值。 因为智能合约掌控着大量价值,对于开发者来说,安全性是一个关键考量。
形式化验证是增强智能合约安全性的推荐技术之一。 形式化验证采用形式化方法(opens in a new tab)指定、设计和验证程序,多年来一直用来确保关键硬件和软件系统的正确性。
在智能合约中实现后,形式化验证能证明合约的业务逻辑符合预先定义的规范。 相比于其他评估合约代码正确性的方法(例如测试),形式化验证能够更有力地保障智能合约功能正确。
什么是形式化验证?
形式化验证是指根据形式化规范评估系统正确性的过程。 简言之,形式化验证让我们可以检查系统的行为是否满足某些要求(即,系统按照我们的想法运作)。
系统(本例中的智能合约)的预期行为使用形式化建模来描述,而规范语言为创建形式化属性提供支持。 然后,形式化验证技术可以验证合约的实现是否符合其规范,并提供合约正确性的数学证明。 当合约符合其规范时,则称其“功能正确”、“设计正确”或“构建正确”。
什么是形式化模型?
在计算机科学中,形式化模型(opens in a new tab)是指对计算过程的数学描述。 程序抽象成数学函数(方程),模型描述给定输入时如何计算函数的输出。
形式化模型提供了一个抽象层次,可以在该抽象层次上对程序行为的分析进行评估。 有了形式化模型,便可以制定形式化规范,描述了需要的相关模型属性。
采用不同技术对智能合约建模,以便进行形式化验证。 例如,有些模型用来推理智能合约的高级行为。 这些建模技术对智能合约应用了黑盒视图,把智能合约视为接受输入然后根据这些输入执行计算的系统。
高级模型侧重于智能合约和外部代理之间的关系,例如外部帐户 (EOA)、合约帐户和区块链环境。 这些模型有助于定义属性,这些属性规定了合约应该如何响应某些用户的交互行为。
相反,其他一些形式化模型侧重于智能合约的低级行为。 虽然高级模型有助于推理合约的功能,但它们可能无法捕捉到实现的内部运作细节。 低级模型对程序分析应用了白盒视图并依赖于智能合约应用程序的低级表示,例如程序跟踪和控制流程图(opens in a new tab),来推理与合约执行相关的属性。
低级模型被视为理想模型,因为它们体现着智能合约在以太坊执行环境(即以太坊虚拟机)中的实际执行。 低级建模技术在确立智能合约的重要安全属性和检测潜在漏洞方面特别有用。
什么是形式化规范?
规范简单来说是指特定系统必须满足的技术要求。 在编程中,规范代表程序执行的总体思路(即程序应该做什么)。
对于智能合约,形式化规范是指属性,即对于智能合约必须符合的要求的正式描述。 这些属性被描述成“不变量”,代表合约执行的逻辑断言,并且在任何情况下都必须无一例外始终为真。
因此,我们可以认为形式化规范是使用形式化语言编写的语句的集合,描述智能合约的预期执行。 规范涵盖合约的属性和定义合约在不同情况下的行为。 形式化验证的目的是确定智能合约是否具有这些属性(不变量)以及在执行过程中这些属性是否未被违反。
在开发安全的智能合约实现时,形式化规范非常重要。 无法实现不变量或者在执行过程中属性被违反的合约容易出现漏洞,可能会损害功能或者受到恶意的利用 。
智能合约形式化规范的类型
形式化规范支持对程序执行的正确性进行数学推理。 与形式化模型一样,形式化规范能够详尽描述合约实现的高级属性或低级行为。
形式化规范从程序逻辑(opens in a new tab)的元素中推导出来,可对程序的属性进行形式化推理。 程序逻辑具有形式化规则,它们使用数学语言表示程序的预期行为。 可以使用各种程序逻辑制定形式化规范,包括可达性逻辑(opens in a new tab)、时间逻辑(opens in a new tab)以及霍尔逻辑(opens in a new tab)。
智能合约的形式化规范可以大致分类为高级或低级规范。 无论属于哪一类,规范都必须充分明确地描述被分析系统的属性。
高级规范
顾名思义,高级规范(又称为“面向模型的规范”)描述程序的高级行为。 高级规范把智能合约建模成一个有限状态机(opens in a new tab) (FSM),有限状态机可以通过执行操作在不同的状态之间转换并使用时间逻辑定义有限状态机模型的形式化属性。
时间逻辑(opens in a new tab)是“用时间限定的命题的推理规则(例如,“我总是饿”或者“我最终会饿”)。” 当应用于形式化验证时,时间逻辑用来声明建模成状态机的系统的正确行为的断言。 具体而言,时间逻辑描述智能合约可以进入的未来状态以及它如何在不同状态之间转换。
高级规范一般详述智能合约的两个关键时间属性:安全性和活性。 安全属性代表“任何坏事始终都不会发生”的想法,通常用来表示不变性。 安全属性可以定义常规软件要求(例如不发生死锁(opens in a new tab)),或者表达合约领域特定的属性(例如,函数访问控制的不变量、状态变量的容许值或代币转账的条件)。
以下面的安全要求为例,它描述了在 ERC-20 代币合约中使用 transfer()
或 transferFrom()
的条件:“发送人的余额始终不能少于请求发送的代币金额。”。 这种合约不变量的自然语言描述可以转化为形式化(数学)规范,以便随后能够进行严格的有效性检查。
活性属性断言“好事终究会发生”,并涉及到合约通过不同状态的能力。 活性属性的一个例子是“流动性”,指的是合约在收到请求把余额转账给用户的能力。 如果违反了该属性,用户将不能提取存入合约的资产,就像在 Parity 钱包事件(opens in a new tab)中发生的情况一样。
低级规范
高级规范以合约的有限状态模型作为起点,并定义该模型的所需属性。 相比之下,低级规范(又称为“面向属性的规范”)通常把程序(智能合约)建模成由数学函数集合组成的系统,并描述这类系统的正确行为。
简言之,低级规范分析程序跟踪并尝试从这些跟踪中定义智能合约的属性。 跟踪是指改变智能合约状态的函数执行序列;因此,低级规范有助于规定合约内部执行的要求。
低级形式化规范可以作为霍尔式属性或执行路径中的不变量来给出。
霍尔式属性
霍尔逻辑(opens in a new tab)提供了一套形式化规则来推理程序(包括智能合约)的正确性。 霍尔式属性使用霍尔三元组 {P}c{Q} 表示,其中 c 代表程序,P 和 Q 是 c(即程序)状态的谓词,它们正式描述成前置条件和后置条件。
前置条件是描述函数正确执行所需条件的谓词;用户调用合约必须满足该要求。 后置条件是描述函数在正确执行时所达成条件的谓词;用户在调用函数后可以期待该条件为真。 在霍尔逻辑中,不变量是一个在函数执行时保留的谓词(即它不改变)。
霍尔式规范可以保证部分正确性或完全正确性。 如果在函数执行前前置条件为真,并且在执行终止时后置条件也为真,则合约函数的实现为“部分正确”。 如果在函数执行前前置条件为真,保证执行可以终止,并且当执行终止时后置条件为真,就可以得到完全正确性的证明。
获得完全正确性的证明很难,因为有些执行在终止前可能会延迟,或者根本不会终止。 也就是说,执行是否终止可以说是一个有争议的问题,因为以太坊的燃料机制阻止程序无限循环(执行要么成功终止或者因为“ 燃料耗尽”错误而结束)。
使用霍尔逻辑制定的智能合约规范需要为合约中函数和循环的执行定义前置条件、后置条件和不变量。 前置条件通常包括函数的输入有误的可能性,而后置条件描述了对于这些输入的预期响应(例如,抛出一个特定异常)。 用这种方式,霍尔式属性有效地保证合约实现的正确性。
许多形式化验证框架使用霍尔式规范来证明函数的语义正确性。 也可以使用 Solidity 的 require
和 assert
语句直接向合约代码添加霍尔式属性并作为断言。
require
语句表示前置条件或不变量并通常用来验证用户的输入,而 assert
捕捉安全所需的后置条件。 例如,通过使用 require
作为前置条件检查调用此函数的帐户的身份,可以实现正确的函数访问控制(安全属性示例)。 同样,可以通过使用 assert
来确认函数执行后的合约状态,防止违反合约中状态变量允许值的不变量(例如,流通的代币总数)。
执行轨迹级属性
基于执行轨迹的 规范描述导致合约在不同状态之间转换的操作以及这些操作之间的关系。 如前所述,执行轨迹是以特定方式改变合约状态的操作次序。
这种方式依赖于智能合约的模型,即具有一些预定义状态(由状态变量描述)和一系列预定义转换(由合约函数描述)的状态转换系统。 此外,控制流程图(opens in a new tab) (CFG) 通常用来描述合约的操作语义,它是程序执行流程的图形化表示。 在这里,每个执行轨迹都表示成控制流程图中的一条路径。
执行轨迹级规范主要用来推理智能合约中内部执行的模式。 通过创建执行轨迹级规范,我们断言一个智能合约的容许执行路径(即状态转换)。 使用符号执行等技术,我们可以形式化验证执行不会遵循未在形式化模型中定义的路径。
我们通过一个有公共可访问函数的去中心化自治组织合约的示例,来介绍执行轨迹级属性。 在这里,我们假设去中心化自治组织合约允许用户执行以下操作:
存入资金
存入资金后可以给提案投票
如果用户未给提案投票,可以要求退款
执行轨迹级属性的示例可以是“没有存入资金的用户无 法对提案投票”或“未对提案投票的用户始终应该可以要求退款”。 这两个属性断言优先执行次序(在存入资金之前无法投票和给提案投票之后无法要求退款)。
智能合约的形式化验证技术
模型检查
模型检查是一种形式化验证技术,它使用一种算法根据规范检查智能合约的形式化模型。 在模型检查中,智能合约通常表示为状态转换系统,而允许的合约状态的属性使用时间逻辑来定义。