什么是区块链？
区块链是比特币的底层技术，其本质上是一个基于共识机制、去中心化的分布式账本数据库。共识机制是指在分布式系统中保证数据一致性的算法；去中心化是指参与区块链的所有节点都是权力对等的，没有高低之分，同时也是指所有人都可以看到过往的区块和交易，这也保证了无法篡改和造假。基于以上特点，总结得出：区块链是由许多对等节点组成，通过共识算法保证区块数据和交易数据的一致性而形成的一个统一的分布式账本。
区块链四大主要特点
Distribute(分布式的)：区块链是全球化的，系统上的节点来自世界各地。区块链没有中心节点，数据分布式地存储在各个节点上。
Autonomous(自治的)：区块链是一种去中心化的、自治的交易体系。表现在两个方面：首先节点平等，每个节点可以自由加入和离开。其次是区块链运行即自行产生区块并同步数据，无需人工干预。
Contractual(按照合约执行的)：一方面体现在区块链中的节点均按照既定的规则执行，如果违背规则则节点会被抛弃；另一方面体现在智能合约，智能合约是程序化的条款、规则，包含在交易中，交易验证时须执行智能合约之后才能被接收。
Trackable(可追溯的)：区块链数据是公开透明的，不能被篡改，且相关交易之间有一定的关联性，很容易被追溯。
智能合约及其安全问题
基于区块链技术实现了许多去中心化应用，以太坊(Ethereum)就是其中之一。以太坊的核心技术之一是智能合约，智能合约是运行在以太坊上的计算机程序，其编程语言是Solidity，是一种类似于JavaScript的语言。
智能合约就是传统合约的数字化版本。其本质是计算机程序，可以在满足其源代码中写入的条件时自行执行。因区块链的不可篡改性，所以合约是不可更改的。
智能合约部署流程：
智能合约作为运行在区块链上的计算机程序，极大的丰富了区块链的功能，使得区块链不仅仅是分布式账本数据库，而且能够完成一定程度的业务处理。
智能合约中有代币（也就是钱）的概念存在，同时作为一种计算机程序，很难摆脱bug。一旦安全漏洞被利用，极有可能导致灾难性的后果，例如丢失加密货币、扰乱金融秩序等。据抽样统计超过90%已部署的智能合约是不安全的。
智能合约自身的正确性和安全性却面临着巨大的问题。著名的DAO安全漏洞，Parity多签名钱包两次安全漏洞都由智能合约的安全问题引起，分别导致5千万、3千万、1.52亿美元的损失。4月22日BEC代币（美图代币）被盗事件，由于一行代码的安全漏洞引发其市值几乎归零。
然而，尽管问题十分严重，限于智能合约安全问题最近两年突然爆发。虽然国内外科研机构也进行了相关研究，却没有能够有效检测智能合约安全性的方案。智能合约安全性问题迫在眉睫。
论文Survey of Attacks on Ethereum Smart Contracts中归纳总结了多种攻击形式。其中有调用未知，缺乏gas（智能合约调用需要消耗的“气体”），异常乱序，类型转换等攻击。
学术论文发表情况
以Google学术数据统计为例，搜索关键字：Ethereum、smart contract、security-analysis，2015年之前未有相关文献，2016年发表54篇，2017年发表115篇，而到了2018年，只上半年就已发表了70篇之多。这些已发表的论文多收录在NDSS、ICSE等顶级期刊和顶级会议中。由此可以看出“智能合约安全审计”已然成为一个研究热点，且有较高的科研水平和研究价值。
Zeus(IBM)
使用形式化验证方法对智能合约代码进行安全性分析。
验证流程：
1. 将智能合约源代码转化成中间形式policy(策略)，策略可以理解为一定长度的代码块。此步骤是将智能合约源代码转换成一种中间形态，为下一步提取谓词做准备。原因在于漏洞检测引擎无法识别源码层面的漏洞；
2. 利用自定义语义转化规则将policy转换为抽象语言，提取谓词约束。简单来说就是将solidity源代码符号化并添加约束条件，举个例子：如果policy中存在send方法（send方法是solidity中发送以太币的方法），那么就会添加约束条件：send_value<=account_balance，条件的含义是发送的以太币数量不能大于账户剩余以太币数量；
3. 将抽象语言转换成可验证的CHC(约束子句)。此步骤是将抽象化的智能合约代码片转换成校验引擎可识别的形式;
4. 利用校验引擎F* framework对生成的CHC进行校验，F* framework是NASA为检验航空电子设备安全性开发的一款漏洞检测引擎。
校验流程：
Reguard
系统架构庞大，由于需要使用一款既定的校验框架F* framework，不得不进行多次形式转换。验证流程复杂繁琐，且经过多次转换可能导致功能缺失。
使用模糊测试针对重放攻击漏洞进行检测。此思路基于这样一个事实：智能合约每执行一个交易会生成一个状态。不同的交易对应不同的状态。模糊测试是通过随机引擎生成随机数据，将随机数据组成大量可执行交易对智能合约进行测试，随机引擎通过测试结果的反馈动态改良生成数据的质量以确保尽可能地探索智能合约的状态空间。基于有限状态机分析每一笔交易的状态，检测是否存在重放攻击。
方案架构图如图所示：
方案简单来讲就是利用穷举法搜索智能合约的状态空间中是否存在重放攻击。原理简单，易实现，只针对重放攻击，功能相对单一。
总结
目前区块链领域的智能合约代码审计处于初步阶段。在国外，苏黎世联邦理工学院已经提供了针对初步的以太坊合约的审计服务：Securify.ch，国内，360等企业也开始关注这一领域。
对以太坊造成大规模“杀伤力”的漏洞大多来源于ICO募集资金等大额资金合约中，对于此类有ERC20（如OpenZeppelin），ERC721等标准代币合约来帮助实施，但此类合约安全性急需代码审计保证。相信在未来的发展中，形式化验证会发挥更大的作用，同时函数式编程在配合形式化中也会有很好的场景。
论文《Survey of Attacks on Ethereum Smart Contracts》地址：
了解更多区块链技术课程，点击以下链接：
https://edu.aqniu.com/course/6502
相关阅读
