自从首次出现比特币交易以来，区块链就吸引了许多兴趣并获得了巨大的动力。尽管关于比特币作为一种数字加密货币可能存在一些有争议的问题，但区块链已经适应了金融和非金融领域的许多领域。随后的数字货币，公平安全计算和PKI应用建立在区块链规范上。
甚至有人认为，像任何全新的信息技术一样，区块链一开始可能看起来是破坏性的，但它可以帮助开发包括去中心化模型和集中式模型的更大的生态系统，并建立现代计算规范。
区块链是一个公共分布式帐本，保留所有有效的交易并包括线性连接的块。最好将其描述为“由所有网络节点共享，由矿工更新，由每个人监视，并且不受任何人拥有和控制”的记录，其中节点都是互联网实体，例如计算机和移动设备。
设备和矿工是指那些可以通过计算能力验证交易的节点。最突出的特征是分散化，它不依赖中央机构来保护和验证每笔交易的有效性，因此消除了潜在的中间后台交易并防止了黑客入侵。通过区块链机制，所有矿工都收集并验证了无信任交易，这使得重复性几乎是不可能的。
区块链存储在每个节点上，并在分布式共识基础上运行。当新交易广播到网络时，所有矿工都需要对其进行验证。在双花攻击的情况下，即某人花了一次以上的资金（尤其是在数字货币中，因为可以复制电子代币），区块链通过工作证明（难题）方案解决了这一问题，即仅允许已解决问题并验证所有交易的节点创建要添加到区块链的新块。
由于可以通过挖掘区块链来获取利润，因此它已成为许多黑客的目标。发生了很多基于区块链的攻击。例如，随着量子计算的发展，可能发生身份盗窃攻击，这种情况发生在某人的所有资产被盗用之后，人们的所有资产都可能被偷窃而几乎无法恢复时，这种情况就可能发生，从而可以迅速破解密码密钥。
另外，由于区块链的匿名和分布式属性，可以将其转换为非法场所。Silk Road，作为一个在线黑市，是一个通过比特币交易所出售非法物品的平台。此外，当具有比其他节点更多的计算资源（即51％处理能力）的高级节点可以指挥所有交易并操纵新区块的产生时，可能会发生著名的51％攻击。
尽管自从创建第一个区块以来，在区块链中还没有发生51％的攻击，但是毫无疑问，这种风险确实存在，尤其是在小型网络中。
区块链可以成为黑客探索然后做一些邪恶事情的基础。在发生上述攻击的情况下，区块链安全协议（也称为中本聪共识）的设计变得至关重要，并且自提出以来就进行了探索和修改。为了帮助防止恶意侵害，已将许多形式主义应用于描述安全协议，并通过独特的自动和半自动技术进行了调查。这些技术主要基于过程计算，树自动机，高阶逻辑等。
为简单起见，在本文中，仅在有界会话上处理区块链协议，即以下提到的所有事物都被视为有限事物。采用模型检查方法来检测区块链的潜在攻击，即对于给定的安全属性，如果未检测到漏洞，则相关的区块链协议必须对该属性安全。
提出了基于环境的演算来描绘区块链协议的行为，演算采用了跟踪语义，因此区块链协议的每个潜在运行都可以作为具体的跟踪进行细化：
•提出了用于保密性的区块链核心协议规范，可以从协议描述中自动生成，从而为研究其安全性奠定了基础。
•分布式拒绝服务（DDoS）攻击显示在区块链场景中仍然存在，并且可能导致“三角攻击”。根据跟踪语义检测其相关的保密性。另外，建议采取一些避免这种攻击的措施。
DDoS攻击通常是由建立僵尸网络引起的，以防止对目标系统服务的合法访问。将DDoS攻击应用于区块链背景，并解释其随后的“三角攻击”，这可能导致节点认为交易已通过验证，而交易可能已丢失。相应的安全属性建立在区块链协议上，并在此处通过模型检查方法进行验证。
在本节中，非形式化地介绍三角攻击的发生方式。考虑这种情况，其中只有一个“network gate”可以将交易分散到外部，如图1所示。A，B，C，D，E，F和H是区块链上的节点。下图描绘了网络拓扑结构，该结构用于通过路由实现广播功能。
假设A，B，C在本地网络中，而C是将在此区域发生的所有交易转移到外部的“gate”。如果A要在完成交易清单后将某些比特币转移给B进行某些商品交易，则它将该清单（上图中的tr：A→B）发送给B和C
偶然地，这时A和B“leave”了区块链网络，这可能存在于真实区块链网络中。这可能自愿或无意地的导致DDoS攻击。
因为在区块链协议中，新的交易广播不一定需要到达所有节点。只要它们到达许多节点，它们很快就会进入一个块。块广播也可以容忍丢失的消息。因此，节点C具有对该事务的绝对控制权。
如果C是恶意的，它可以隐藏该事务，即C不会将该事务传播到外部的其他节点。经过6个区块后，B返回到区块链网络。如果B仅复制丢失的区块而不是检查A发送的交易是否确实存在于区块链中并将货物交付给A，则B将遭受一些本应由A支付的金钱损失。请注意，如果C可以收听网络并找到B离开网络时的间隔时间。而且，即使这样，A也会与C勾结，欺骗B。而且，DDoS可以完全达到此目标，从而阻止B对区块链的访问。
A.初步知识
在本节中给出一些正式定义，这些定义将在以后使用。提出了过程演算的以下原语，用于描述有界会话中的区块链协议。跟踪语义可以描述区块链协议的所有可能运行。
定义1（消息）： 表示三个不相交的可数集，V代表变量，B代表binder名称，L代表标签。令变量为x，y，z…；binder名称为m，n，k…，以及标签的范围a，b，c …
集合M中的消息M，N，L… 的指定迭代如下：
其中：
•pm来自不可分解的主消息集；
•m [pm1，…，pmn]是原子消息，具有从pm1到pmn的灵活参数；没有参数的称为名称。
•{M} L是具有纯消息M和加密密钥L的加密消息。
注意，像k [A，S]这样的绑定器显示为由主体A和S共享的对称密钥。主体A的公钥和私钥分别由+ k [A]和-k [A]表示。
还给出了流程的定义，该定义将用于引用区块链协议中每个主体的行为。
定义2（过程）：令P，Q，R …在整个可计数过程范围内。进程的语法定义如下：
其中：
•0表示不执行任何操作的过程；
•a（x）.P通过通道a接收输入消息M，其行为类似于P {M / x}；
•aM.P通过信道a发送消息M，其行为类似于P；
•（new x：A）P仅将名称x限制为集合A，在其他方面的作用类似于P；
•[M = N]P即如果M = N，则P的行为与P相同，否则拥塞，即，它无法进行任何转换；
•（νn）P表示n是P中的本地名称，其他进程只有在P发送出去后才知道n，（νn）用于捕获消息的新鲜度；
•对拆分语法显示，如果M是像（N，L）那样的对，则令（x，y）= P中的M将为P {N / x，L / y}，否则它将拥塞；
•P || Q表示进程P和Q同时运行；
•解密表明，如果M是加密的消息{N} L，L可以解密该消息，则{x} L的情况M的行为类似于P {N / x}，否则它被拥塞；
•V eri ∗ (M)与区块链中的验证操作有关，即，矿工使用它来验证交易的有效性；
•POW是指工作量证明，即扫描适当的随机数以使其满足加密散列函数，例如SHA256 ；在区块链协议中，工作量证明主要是通过增加区块上的随机数直到找到目标值使其满足哈希要求来实现的；
•Append（M）是指每个矿工在验证了该区块中的所有交易之后，需要将新产生的区块附加到其本地区块链中；
•P + Q充当P或Q，即，一旦其行为类似于P，则将不会作为Q执行。
定义3（具体跟踪和配置）：动作是形式为a（M）或a¯M的术语。满足从其前缀操作中获得的每个输入消息的字符串，代表协议的可能运行。我们称其为具体跟踪，并使用来表示它。具体配置s P由具体轨迹s和过程P组成。
具体的跟踪用于对区块链协议的行为进行建模。
定义4（具体过渡规则）。具体配置之间的转换规则定义如下。s | — M表示M属于具体轨迹s上的输出操作中的那些消息，即msg（s）| —M。
这里的函数Opp用于在加密和解密中生成补充密钥，即Opp（+ k [A]）= -k [A]，Opp（-k [A]）= + k [A]。freshN（V）是一个函数，它可以产生一个不会出现在V中的新名称（此处V是源配置的新名称集）。具体的过渡规则可以在下图中找到。
令−→*为−→的反和及物闭合。具体配置的可达性问题询问是否给定初始配置<s，P>和最终配置<s’，P’>，是否存在<s，P>-→∗ <s’，P’>，即<s ，P>可以达到<s’，P’>，其中s’是由<s，P>生成的具体轨迹。P ath是一系列连续配置。请注意，此处的跟踪可以跟踪进程的占用空间，这可以帮助分析协议的保密性。
B.区块链核心协议表示
首先给出矿工在区块链中的正式表示，然后组成他们并构建区块链协议的表示。
在比特币转移交易场景中，矿工分为三种：发送者，接收者和一些验证者，即验证所收集交易的有效性的其他矿工。请注意，所有矿工都可以进行工作量证明并将交易路由到其邻居。
假设发送方A打算向接收方B发送一些比特币。请注意，这里我们只是忽略了有关比特币转换的一些更详细的信息，例如工作量证明的详细解析过程，梅克尔树的结构变化，在一个块上总结所有事务，并产生一个与它们相对应的统一哈希值，依此类推。仅描述核心区块链协议。
非形式化地，这些步骤概述了核心区块链协议：
1）A使用其私钥为之前的交易提供数字签名，即要发送给B的比特币的来源以及接收者B，然后将此签名添加到此交易的末尾。
2）A将该交易广播到区块链网络，区块链上的每个节点都会将该交易收集到其潜在区块中。
3）每个矿工都进行工作量证明，即试图解决一个难题，以竞争在此周期中创建新区块的特权。具体而言，所有矿工在一定的限制下都试图找到可以满足SHA256要求的合适值。作为奖励，可以在此过程中生产一些新的比特币，然后将其奖励给可以成功生成下一个新区块的人。同时，每个矿工都需要验证收集到的交易的有效性并将其路由到其邻居。
4）当某人解决工作量证明时，它会将所有收集到的有效交易以及带有时间戳的时间戳广播到区块链网络。然后其他矿工验证这些交易的有效性。
5）如果所有矿工都同意这些交易，即这些交易在验证后有效，那么将生成包含这些交易的新区块并将其附加到当前区块链中。通过这种方式，构建区块链时将新区块一一添加。经过6个区块后，可以说B收到了A转移的钱。
整个交易过程按流程形式化如下。请注意，这里说的是用于矿工彼此通信的通道是专用的，但是稍后在分析区块链协议的安全性属性时，将忽略通道名称之间的差异，即所有通道都被视为与通道之间交互的方式。环境。
•首先，发送方A的描述如下（与上述步骤1和2有关）：
它显示事务主要由三个部分组成：上一个事务pretr，接收方B的地址addrofB和转换后的金额。最初，A使用哈希函数生成此事务的摘要，并使用其私钥对该摘要进行加密。加密的摘要被视为要发送给A邻居的数字签名。然后，A将此数字签名和原始交易路由到其邻居C。
•验证者C从A接收消息。C使用与A相同的哈希函数计算事务摘要，并将其与接收的摘要进行比较。如果它们相同，则C可以确保该事务确实来自A。然后C将该事务收集到一个潜在的块中。同时，C致力于寻找工作量证明（POW）的解决方案，并选择将此交易路由到其邻居验证者D（与上述区块链协议的步骤3有关）。
D将执行与C相同的操作，但是接收和发送操作仅在通道d中进行。即由d（x）接收和由d（x）发送。请注意，这里允许C不发送接受的交易，这可能在真实的区块链场景中发生。因此验证者C可以做以下三件事之一：
•矿工E解决工作量证明时，会立即将新生产的区块转发给其邻居。注意这里C，D，E可以是区块链中的任何矿工。使用B [tr1，…，trn]表示一个包含n个事务的块（与上面的步骤4有关）。
•其他矿工（例如矿工F）验证此新生产区块中所有交易的有效性。如果他们都同意这些交易，那么他们会将这个区块附加到当地的区块链上。请注意，在F的最后一个过程下面是0，它仅表示此循环中此块的完成。实际上，在真正的区块链中，矿工将继续构建下一个区块（与上述区块链协议的第5步有关）。
因此，区块链协议可以被描述为矿工的组成。
最后但并非最不重要的是，矿工C，D，E，F不是特定的矿工。一个可以是它们中的任何一个，例如C也可以是D，E或F。此外，A可以扮演其中任何一个的角色。
为了表示安全属性，定义了一些操作术语。可以通过在区块链协议模型生成的轨迹上的可达性问题来对安全属性进行建模。
定义5.令α为一个动作：一组动作术语表示如下：
定义了t和|=两种关系。前者存在于跟踪项和动作项之间，后者存在于配置项和动作项之间。它们的归纳定义如下 而s指的是痕迹)：
区块链协议的保密属性直观上意味着每个有效交易都应成功添加到后续区块中，即不会丢失任何有效交易。
为了定义此属性，说如果可以将有效交易成功添加到区块链，则其对应的跟踪必须以Append（x）.0结尾。同时，如果跟踪以Append（x）.0结尾，则先前的操作必须包括一个发出事务的操作。如前所述，可以将保密属性建模为操作项，因此保密属性定义如下。
定义6（区块链协议的保密性）：给定关于区块链协议保密性的正式过程，如果满足以下条件，它就可以满足保密性（假设C是将交易路由到外部网络的第一个验证者，C是与其邻居的通信通道）：
1）三角攻击：
可以通过以下方式捕获，即，据说一笔交易已添加到区块链中，但实际上并未广播给所有矿工。请注意，这里忽略了通道名称之间的差异。
在此跟踪中，过程Append（M）发生在没有转移交易的发送过程的情况下，这与定义6中的区块链协议的保密性矛盾，因此可以将其视为攻击。考虑到所示的情况，这意味着在A将事务转移到C之后，C不会将该事务路由到其他矿工，即，根据C的描述，C不会执行c¯（x），因此交易从C丢失。
2）对策：
如果强迫每个矿工发送其接受的交易，则可以避免上述攻击。形式上，可以在区块链协议规范中将C的行为修改为：
在这种情况下，矿工C无法随意放弃发送动作。因此，如果可以将有效交易添加到区块链，则必须已将其广播给所有矿工。此外，为抵御上述攻击，针对区块链上的节点提供了一些建议，如下所示：
•从接收方B的角度来看：参与交易的节点应积极保护其在区块链上的存在，这强调了“不信任任何人”的概念。即使发生事故故障，节点返回区块链后也应首先检查相关交易。如果承诺的交易未在任何区块中发生，则接收方可以拒绝交付货物。
•从发送方A的角度来看：如果只有一个“gate”将交易转移到外部，则节点应继续监听区块链网络，并选择不发送交易，或只是延迟交易。
本文采用模型检查的方法，通过过程演算来定义区块链核心协议规范，并基于跟踪语义对其保密性进行了检查。作为DDoS攻击在区块链上的一种应用，提出了三角攻击并将其形式化，以与跟踪语义上的保密性相矛盾。此外，还提出了针对攻击的一些对策。
未来计划根据其模型在区块链协议上发现更多潜在的攻击。
- 结尾 - 精彩推荐 【技术分享】探讨恶意软件检测中的对抗性样本 【技术分享】针对自私挖矿的重新审查（下） 【技术分享】针对自私挖矿的重新审查（上） 戳“阅读原文”查看更多内容 原文始发于微信公众号（安全客）：【技术分享】针对区块链中三角攻击检测的跟踪分析
