区块链系统和智能合约的形式验证101:形式化要求

在我们的四部分系列的第二部分中,我们将讨论对系统要求进行形式化的过程,以及如何使其适合于区块链系统智能合约的形式验证的更大范围。

回想一下,正式验证就是要知道我们的系统实现(例如区块链系统/智能合约)是否满足我们的系统要求。

今天的文章是关于将我们的需求文档转换为等价的形式化、数学化需求规范的过程。

区块链系统和智能合约的形式验证101:形式化要求

英语是现代商业的通用语。因此毫不奇怪的是我们经常把需求写成简单的英文文档。不幸的是,出于正式的验证目的,英语文档太不精确,通常会掩盖重要的实现细节。基于这个原因(我们将在后面看到),我们通常需要正式的验证专家来帮助我们将英语需求文档重写为正式的数学要求规范。例如,假设我们正在设计一个实现公开竞价拍卖的智能合约。我们可以将拍卖合同的要求写成如下:

英语语言要求

每个拍卖都有一个主物,一个有效期,一个最低竞标,一个可选的最高竞标者(默认为无)和无限数量的竞标者。在拍卖进行中,投标人可以按顺序进行投标。如果出价大于最低出价,则将其记录为新的最低出价,同时将出价者记录为最高出价者。否则,出价将被忽略。拍卖结束时,除非出价人没有出价,否则将从出价人的帐户中扣除等于最高出价人出价的金额并将其转移到拍卖主物。

因此现在我们要将英语描述转换为正式的数学描述。为此我们将选择适合表达我们所需属性的数学逻辑。就像英语一样,还有多种语言一样。法文 中文; 等等…,我们可以使用不同的数学逻辑。一些常见的选择包括:方程式逻辑,一阶逻辑,集合论,高阶逻辑/类型论,重写逻辑或可达性逻辑。我们如何知道要使用哪个?事实证明,在(a)形式化我们的要求,(b)我们的定理证明者和(c)我们的形式语义中使用的逻辑都需要整合在一起,因此我们如何对过程的一部分做出选择将影响其他。

为了我们的目的,我们将使用可达性逻辑(这也是K框架使用的逻辑),因为它(1)使我们能够非常自然地形式化对演化系统的需求,以及(2)具有强大的工具支持。因此这意味着我们将系统描述为可达性逻辑理论。可达性逻辑理论具有(a)描述我们系统状态的语法和配置;(b)描述我们系统要求的可达性规则。现在我们发明一些语法和配置来定义拍卖合同状态。为此我们将使用K语言提供的语法架构。

拍卖状态(语法/配置)

syntax Address ::= (Letter | Number)*
syntax MaybeAddress ::= Address | “None”

configuration <host> Address </host>
              <start> Number </start>
              <end> Number </end>
              <highestBidder> Address </highestBidder>
              <minBid> Number </minBid>

使用此语法和配置,我们可以编写如下的具体拍卖状态:

<host> ab2r3f <host>
<start> 10 </start>
<end> 20 </end>
<highestBidder> None </highestBidder>
<minBid> 15 </minBid>

希望该配置的含义很清楚:拍卖在时间unit 10开始,在时间unit 20结束,由地址为ab2r3f的帐户所有者主持,尚无可行的出价,且最低出价为15个令牌。现在这个简单的语法描述已经有可能帮助我们发现问题——特别是,它可以帮助我们了解系统状态描述是否不完整。实际上我们的拍卖配置缺少一个关键要素:当前时间!这种遗漏是有道理的,因为在我们原始的合约说明中从未直接提及时间,而只是间接提及了时间。因此修改后的拍卖合约状态配置将如下所示:

configuration <host> Address </host>
              <start> Number </start>
              <end> Number </end>
              <currentTime> Number </currentTime>
              <highestBidder> Address </highestBidder>
              <minBid> Number </minBid>

现在我们知道拍卖何时开始。例如拍卖配置:

<host> ab2r3f <host>
<start> 10 </start>
<end> 20 </end>
<currentTime> 5 </currentTime>
<highestBidder> None </highestBidder>
<minBid> 15 </minBid>

描述了尚未开始的拍卖。我们还需要澄清其他问题,例如数字必须为零或正数,因为我们不希望货币或时间为负数。

拍卖合同要求(规则)

可达性逻辑规则的形式为:

rule Configuration1 => Configuration2 requires A ensures B

可以将其理解为:处于配置1所描述的状态且满足条件A的系统必须演变为配置2所描述的确保条件B的系统。为方便起见,我们将假定未提及的配置部分不会发生变化。现在让我们看一些示例规则。

格式正确的持续时间

立即想到一个简单的规则:对于任何持续时间,我们都需要(a)持续时间是静态的,即不变;(b)开始于结束之前。可以通过以下形式的规则来描述:

rule <start> S </start>
     <end> E </end>
  =>
     <start> S </start>
     <end> E </end>
  requires S < E

(a)满足以下条件:开始时间和结束时间不受此规则的影响;要求(b)包含在require子句中。

时间和出价的单调性

在除了最奇特的物理学研究之外的所有研究中,时间总是在向前发展。让我们将该要求编码为规则:

rule <curTime> C </curTime>
  =>
     <curTime> C’ </curTime>
  requires C <= C’

该规则是说当前时间C必须演变为某个时间C’(可能不同),以使C小于或等于C’。

我们有一条几乎相同的规则,规定最低出价必须始终增加价值或保持不变(以防万一没有新的出价):

rule <minBid> M </minBid>
  =>
     <minBid> M’ </minBid>
  requires M <= M’

拍卖结束

最终规则规定,拍卖状态在拍卖结束后不得更改。我们可以这样写:

rule <end> E </end>
     <curTime> C </curTime>
     <highestBidder> B </highestBidder>
     <minBid> M </minBid>
  =>
     <end> E </end>
     <curTime> C’ </curTime>
     <highestBidder> B </highestBidder>
     <minBid> M </minBid>
  requires E <= C

此规则完全符合我们的要求。

从以上描述中,您可能会以为智能合约验证并不是那么难。不幸的是,为了简化解释,我们隐藏了验证问题的大部分复杂性。现在让我们拉开帷幕,看看验证真实智能合约的复杂性。在实践中:

1. 们的系统语法/配置实际上描述了整个区块链系统,例如我们的语法和配置将是以太坊虚拟机(EVM)字节码的语法和配置;
2. 我们的规则将讨论特定的EVM字节码拍卖智能合约如何演变。该合同将涉及我们上面提到的状态组件的变量,即它将有一个拍卖主机的可变主机,即地址,拍卖开始时间的可变起始,等等。

(1)-(2)的结果是,在实践中,我们推理的源代码程序(无论是智能合约还是区块链系统代码)仅间接描述了我们要设计的系统,即我们没有去设计全新的语言从头开始专门描述我们的问题。这意味着我们正式要求的映射必须讨论与我们整体所需的系统行为完全不相关的概念,例如EVM详细信息与拍卖完全无关,例如EVM指令和内存位置。

我们已经看到了如何使用K将英语要求映射到形式化数学要求的概述,并着眼于验证区块链系统和智能合约。此外我们看到形式验证问题更加深入。它需要同时(i)逻辑专家(例如可达性逻辑)和;(ii)系统专家(例如以太坊)。幸运的是,存在许多逻辑工具(例如K框架)和教科书,可以帮助系统专家精通解决形式验证所需的数学逻辑技能。

您的公司或组织是否使用形式验证来加速开发过程并减轻潜在的设计风险?您是否需要一个值得信赖的合作伙伴来帮助您解决围绕区块链系统设计,智能合约语言或智能合约实施的问题?如果是这样,我们很乐意为您提供帮助。

关键词: 区块链系统  智能合约  

该内容来自于互联网公开内容,非区块链原创内容,如若转载,请注明出处:https://htzkw.com/archives/28098

联系我们

aliyinhang@gmail.com