「火星公开课」第136期|链安科技杨霞：如何预防智能合约漏洞
浪花财经
智能合约已成为区块链安全的重灾区。
今年5月，EOS被爆“史诗级”安全漏洞，攻击者可以通过发布包含恶意代码的智能合约，控制虚拟货币交易。这距美蜜币发生此类严重漏洞仅仅过去了1个月。
今年4月，美蜜币因智能合约出现重大漏洞遭到黑客攻击，BEC凭空蒸发了10亿美元，最后价值几乎归零。
时间再拉到一年前，Parity的多签名钱包合约被曝漏洞，导致3200万美元的数字货币被盗，甚至连DAO、BEC这样的著名项目市值也出现了一夜归零的惨痛事件，而所有代币都由智能合约生成。
据区块链安全网数据显示，区块链重大安全事故在2018年爆发式增长，因智能合约漏洞而引发的经济损失已赶超交易平台事故成为第1名。
针对智能合约的安全问题，「火星财经创始学习群」轮值群主任铮、副群主廖志宇邀请到成都链安科技CEO杨霞，于7月31日21:00详解了智能合约形式化验证平台VaaS。
她表示，VaaS将原本应用于军工领域的「形式化验证」方法，应用于智能合约安全审计，即基于数学建模方法对系统进行描述，通过形式化验证，开发者可以对程序的安全性事先进行审查，排除逻辑漏洞和安全漏洞，从而保证合约的安全。
结合以太坊和EOS智能合约漏洞，她建议项目方在合约开发完成除了自己做好测试外，还应选择专业的第三方进行安全审计，因为安全审计公司能多角度分析合约代码，找出开发者容易忽略的问题，做到事先预防安全事件的发生。
以下为杨霞分享原文，由火星财经整理：
一、关于形式化验证
形式化验证最早是应用于航天、航空、军事等领域的安全关键软件中的技术，本身是一个很冷门的领域，受众范围也没那么广，基本都是在高校和研究所里在研究，我们最早尝试将这样的技术去验证智能合约安全，最后发现形式化验证方法应用于智能合约安全审计效果不错。
形式化验证是一种基于数学和逻辑学的方法。具体来讲，在智能合约部署之前，对其代码和文档进行形式化建模，然后通过数学的手段对代码的安全性和功能正确性进行严格的证明，可有效检测出智能合约是否存在安全漏洞和逻辑漏洞。
该方法可以有效弥补传统的靠人工经验查找代码逻辑漏洞的缺陷。形式化验证技术的优势在于，用传统的测试等手段无法穷举所有可能输入，而我们用数学证明的角度，就能克服这一问题，提供更加完备的安全审计。形式化验证跟传统互联网安全公司的做法有着本质的区别，传统的互联网安全公司是「以攻促防」，而我是直接从代码自身安全角度出发，实现预防不安全事件的发生。
「形式化验证方法举例」
通过对合约文档和和代码进行形式化的建模，通过数学推理和证明的方式验证智能合约的功能正确性和安全属性。可以发现代码的逻辑漏洞和安全漏洞，弥补人工方式对逻辑漏洞查找的不足。
以近期频发的溢出类安全漏洞属性检查为例，如检查代码
int8 c=a+b
是否存在溢出漏洞，下面展示对这行代码的功能正确性和安全属性的证明过程。
首先，我们对整数类型建模，定义形式化规则：
Int8.repr: Z -> int8
该规则通过截取纯数学整数（取值范围从无穷小到无穷大）的低8位数值得到一个8位长度的机器整数。然后写加法运算的形式化规范，如下：
{a:int8,b:int8} //
设置代码执行的前提条件，保证a和b的类型是8位有符号机器整数;
{c = a + b;} //
加法运算的源码程序；
{(int8.repr(a+b)) // ((Int8.repr (a+b)) = (a+b))} ; //
设置代码正确执行的后置条件。
其中，(int8.repr(a+b))描述，是为了证明代码的功能正确性是否满足，即需要证明源代码是对a和b进行求和而不是求差或任何其他运算逻辑，并且将运算结果转换为int8类型。此外，需要对是否溢出的安全属性进行证明，因此添加后置条件：
((Int8.repr (a+b)) = (a+b))
因为一旦
a+b>int8.max_singed 或
a+b
(Int8.repr (a+b)) ≠ (a+b)。
最后，根据前置条件证明代码的执行是否满足上述后置条件。如果产生一个不可证明结果，说明程序功能不正确，或者存在溢出安全漏洞。然后根据证明结果，对源程序进行分析修改，然后再重新证明，直到证明通过为止。我们采用这种数学的证明方式将代码形式化描述为公式，并对其属性进行同样对其他逻辑漏洞和安全漏洞进行证明，基于此原理，我们实现了自动化的验证工具，能够方便、快速地验证出代码的功能正确性和安全属性。
二、黑客如何攻击区块链平台的智能合约？
区块链技术容易遭受黑客攻击的包括区块链底层平台、区块链智能合约两个方面。而智能合约由于代码小，复杂度较低，攻击较方便，因此黑客攻击的最主要目标为智能合约。造成这些的攻击的主要原因在于这些程序自身存在安全漏洞或者逻辑漏洞。
区块链作为一个新兴技术，出现安全事件是可以理解的。任何软件系统都不可避免的存在bug或者安全漏洞，也就是说这些安全问题不只是存在于区块链平台中。但是由于区块链平台一旦出现安全问题将会带来巨大的财产损失，从而造成币市恐慌。
这些安全问题是可以采取适当措施进行解决的，比如对在智能合约部署之前，对其进行严格的安全审计，是可以有效提高智能合约程序的安全性，提前预防安全隐患。我们的VaaS智能合约安全审计平台，采用了形式化验证方法和技术，并且率先实现了自动化检测合约安全漏洞的工具。
三、VaaS系统架构及VaaS“一键式”自动形式化验证平台操作演示
VaaS平台可以理解为自动化智能合约安全审计工具，采用多种形式化验证方法和数学模型，可以“一键式”自动定位到有风险的代码位置和风险原因，有效的查找合约的10多种安全漏洞和逻辑漏洞，具有验证效率高、自动化程度高、人工参与度低、易于使用、支持多个合约开发语言、支持大容量区块链底层平台的形式化验证等优点，能显著提高智能合约安全性，目前VaaS平台支持EOS和以太坊智能合约的安全审计。
我们已用VaaS检测出EOS、以太坊平台多种安全漏洞，并且针对这些漏洞进行了全面分析和总结，给开发者安全的建议，从而显著提高了他们的安全等级，后期VaaS平台还将逐步支持其它主流区块链平台的形式化验证工作。
四、智能合约安全生态建设方面的工作
除了研究区块链平台的智能合约、形式化验证外，我们也一直努力为区块链安全生态做出自己的贡献。我们会定时、定期地对已上线的以太坊智能合约的安全漏洞进行分析；通过对EOS合约的安全审计，发现并总结EOS智能合约存在的问题，为广大智能合约开发者给予智能合约开发的建议。
此外，对交易所代币出现异常情况进行安全提示和报告、同时对区块链相关安全漏洞也会进行深入分析。我们最终将发现的漏洞即时总结并将建议报告给开发者，避免漏洞被黑客利用，致力和全球所有安全技术者共同维护区块链生态的安全。以下是我们发现的区块链生态相关的主要漏洞及分析总结：
1、3份合约存在Owner权限被盗问题
近期，用VaaS平台对以太坊链上智能合约进行安全审计的过程中，发现了3份合约存在新的安全漏洞。 
此漏洞是合约构造函数constructor()使用不当从而导致Owner权限被盗。
问题描述：
以太坊solidity0.4.22引入了新的构造函数声明形式constructor()，该函数引入的目的是避免编程人员在编写构造函数时的命名错误。
然而，由于用户编写函数时习惯性的使用function进行声明，从而导致构造函数constructor的使用引入新的漏洞。
正确的构造函数形式：constructor() public { }
错误的构造函数形式：function constructor() public { }
Owner权限过大存在的安全隐患：
Owner是Solidity语言中对智能合约开发者的称呼，owner可以归纳为超级权限。对前100基于以太坊ERC20协议智能合约（例如Bancor、Augur、MakerDAO、KyberNetwork、EnigmaMPC的智能合约）安全事件进行分析后，超级权限被盗可存在如下安全隐患：
•随时冻结代币转账
•任意铸造发行新的代币
•销毁任意账户内的代币
•额外增发代币
•停止整套交易系统运行
Owner权限如此之大，说明众多“去中心化”的产品，实际上隐藏一个潜在威胁，掌握在开发者的手上，所有对代币虎视眈眈的黑客或者内部人员都会想方设法夺取这个控制权。
如此强大的权限一旦被黑客窃取是相当危险的，黑客可以对依赖智能合约交易的代币为所欲为，无论是冻结，增发，还是自毁，只需要调用合约中一个函数就可轻松实现，进而操纵整个代币的价值。而与之相关的代币也必将遭受冲击，后果不堪设想。
如何避免将会导致的风险？
既然合约开发者可能会存在使用constructor函数不当，那么作为项目方应该如何去防范后期可能造成的风险呢？给出下面两种建议方法：
1.新的constructor使用方法为，前面无function声明：
2.Remixde等编译器会对constructor的错误使用产生警告，开发者千万不要忽略编译器告警，推荐更改源码，消除所有编译器警告。
建议广大开发者在合约编写上遵守开发规范，并且在写合约敏感函数（如构造函数、回调函数）时，应严格遵循官方命名要求，同时千万不要忽略编译器告警，在合约发布到主链之前，应在官方提供的测试网站上进行充分验证。
2、发现了以太坊智能合约的安全漏洞
我们利用形式化验证工具VaaS对Top500智能合约进行深入安全审计，发现RMC、UselessEthereumToken两个代币合约存在严重安全漏洞！
RMC代币漏洞分析：
下图是RemiCoin (RMC)代币中的一段代码：
问题分析：
这段代码实现了ERC20 代币规范中的transferFrom函数，该函数的功能是用户(_from)向另外一个用户(_to)转账一定数量的代币，但是在该函数中却使用了错误的逻辑，在红色框中要求只有：
allowed[from][msg.sender]
的值小于value时，代码才能继续运行，而下面却进行了：
allowed[from][msg.sender] -= value的操作，
造成了溢出错误，让该函数具有严重的漏洞。
漏洞危害：
而攻击者就可以利用这个漏洞，不需要私钥即可无限制的将任意账户的RMC币转到指定的账户(_to)，从而导致所有持有RMC币的账户都有可能被盗取，严重危害了用户的财产安全。
RMC代币自去年7月进入交易所以来，代币价格最高时达到近2美元，市值300多万美元。12月，有攻击者对该合约进行攻击，并被爆出漏洞，随后，代币价格一路暴跌，跌至4月份的不到0.02美元。
此时，由于该漏洞导致不需要用户的私钥即可对账户余额进行操作，这使得用户手中的RMC代币也变得毫无价值。
UselessEthereumToken代币漏洞分析：
无独有偶，与此类似的是，据悉名为UselessEthereumToken的代币，号称世界上第一个100%诚实的以太坊ICO，也出现了严重的安全漏洞：
问题分析：
上图红框中的逻辑是：
balances[_from] <= _value
且：allowed[_from][msg.sender] <= _value
且：balances[_to] + _value <= balances[_to]
才能进行转账操作，而接下来的运算导致：balances[_to]、balances[_from]、allowed[_from][msg.sender]均产生溢出。
漏洞危害：
攻击者无需任何私钥，只需调用该函数时，把传入的参数_value设置得足够大，即可操纵_from和_to的账户余额。
最终，这个漏洞使得UselessEthereumToken就像其名字一样，变得毫无价值。
目前，仍有攻击者利用上述漏洞对两个智能合约进行攻击，下图为攻击者利用漏洞大量盗取RMC币：
下图为攻击者利用漏洞大量盗取UET币：
在这些漏洞的背后，往往是由于智能合约开发者的经验欠缺。而如何有效地防止此类漏洞的发生，成为了区块链智能合约开发中工作中的一个难题。安全是这场竞赛的核心赛道，对各方而言，都不容忽视。
3、对区块链相关安全漏洞进行深入分析并给出建议
为了对区块链安全生态做出更多的贡献，我们对以太坊平台的十几种已发现安全漏洞进行了全面的分析和总结，并且针对某些近期报出的安全漏洞进行深入分析，并给予开发者一些友好建议。下面选择一部分典型问题进行描述：
（1）对Mint漏洞的分析建议：
我们对于最近有人报道的关于铸币函数Mint的高危漏洞问题，也进行了分析，我们认为mint函数不一定导致恶意增发。我们对以太坊市值Top 500的代币合约进行了审计，发现有107个合约使用的mint函数，可使代币发起方实现代币的无限增发。
我们将此情况与交易所进行了及时反馈，通过跟项目方和交易所的沟通发现，并不是所有的铸币函数都是高危漏洞，有的合约使用该函数是因为代币发起方项目必不可少的功能需求。当然，也不排除有的项目方会利用该函数恶意增发的可能。
（2）对burn、Destroy漏洞的分析建议：
我们使用VaaS区块链智能合约自动化安全审计平台，对以太坊市场市值TOP500代币进行漏洞代码形式化验证，发现29个代币合约使用destory()，burn()或类似的功能函数，可使代币发起方自由的控制销毁用户地址代币余额。
我们认为存在该函数的代币合约，代币发起方的确可以自由的控制销毁用户地址余额。但是如果在代币出现重大风险的时候或者某个账户失控的时候，控制该用户币的流通，减少损失。
（3）对以太坊ERC20代币approve函数使用建议：
以太坊ERC20代币标准，用户可以通过approve函数授权第三方帐户为其管理指定额度的代币。但用户在变换指定额度操作过程中，可能存在二义性，导致多次授权。比如：用户A授权用户B使用100代币额度，后来用户A要改变授权额度为50代币，用户A通过approve函数授权为50代币过程中，用户B可能刚好提取了100代币，从而导致用户B可以再提取50代币。
为了避免二义性的授权操作，我们建议:
i. 在更改授权之前，需通过approve函数设置授权代币数量为0.确认代币未被提取后，再进行授权更改。
ii. 建议代币智能合约开发使用increaseApproval和decreaseApproval函数，进行授权更改操作。
（4）对交易所USDT充提问题的分析：
近期，有安全公司突然发表言论：提醒各大交易所尽快暂停 USDT 充值功能，并自查代码是否存在逻辑缺陷。经过我们分析，此次漏洞是因为，交易所可能没有对用户USDT充值交易进行确认，导致用户可能“假充值”，根本原因是再进行区块链Dapp开发时，对区块链接口开发理解不充分、没有做好严格安全把控。
4、通过对EOS合约审计发现EOS智能合约存在的安全问题，并进行问题总结和建议
VaaS-EOS自动化合约审计工具对多个eos合约进行了安全审计，发现存在整型溢出等问题，部分合约实现不够严谨。为了便于大家在EOS平台写出更加安全的智能合约，我们将发现的一系列问题进行了分析和总结，并给出了建议。
我们通过对已审核的EOS合约分析，发现存在如下主要问题：
（1）存在整型溢出错误
使用自己的数据结构描述代币，对代币数值进行算数运算时未进行安全检查。在误操作时容易产生整型溢出错误，可能导致代币量归零甚至变成负数的严重结果！
（2）权限检查不严谨
权限检查不严谨，造成逻辑漏洞。部分代币合约设置了冻结账户和代币的功能，然而将检查 “冻结” 的代码仅仅放在transfer（转账）函数中，从而导致执行issue（发行代币）的时候不受“冻结”状态影响，可以任意增发代币。
（3）API函数的不规范使用
注意EOS API函数的参数类型。如 string_to_symbol(uint8_t , const char *)，第一个参数传入的整型变量需要小于256，若使用该API前未对输入进行检查，则可能导致整型溢出，从而导致操作了错误类型的代币，带来严重后果。
（4）常规代码错误
数据库API使用不严谨，如multi_index中提供的get和find。其中get会检查数据是否查询成功，数据未找到则断言退出，而find不会检查数据查询情况，需要用户自行判断，如果缺少判断直接使用将会导致指针使用问题。
既然EOS代币合约存在不严谨之处，那么作为项目方应该如何去防范后期可能造成的风险呢？我给出下面三种建议方法：
（1） 合约中使用官方提供的 asset 数据结构描述代币，对代币的算数运算同样利用asset完成。
（2）在使用multi_index的find函数时，一定要进行返回值的检查。
（3）对所有输入都通过断言检查有效性，调用API函数前，检查参数类型和大小。
最后，建议代币合约参照EOS官方给出的eosio.token示例进行实现，避免疏忽从而导致安全检查不完备。
EOS代币合约虽然目前还没有上线，但是项目方一定不能掉以轻心，避免再次重蹈整型溢出等问题引发的代币被盗事件。
总体而言，我认为从目前审计EOS代币合约所遇到的问题来看，开发者在合约敏感代码（如操作代币数额）前后，一定要做好参数限制和权限检查，使用EOS API时一定要搞清楚该函数的输入限制和返回值形式，同时多多参考官方的示例实现。
另一方面，智能合约安全作为一个关键的链上交易程序，一旦部署将无法撤销。因此，项目方合约开发完成后除了自己做好测试外，选择专业的第三方单位进行安全审计也是很有必要的，因为安全审计公司能多角度分析合约代码，找出开发者容易忽略的问题，做到事先预防安全事件的发生。
嘉宾简介
杨霞 / 成都链安科技CEO
电子科技大学副教授，最早研究区块链形式化验证的专家，一直为航空航天、军事领域提供形式化验证服务，主持国家核高基、装发重大软件课题等近10项国家课题。CC国际安全标准成员、CCF区块链专委会委员，发表学术论文30多篇，申请20多项专利。
对话发起人
任铮Kevin/共识实验室合伙人
计算机、工商管理双硕士。曾任职于蓝港资本、光华弘人资本等多家VC机构担任合伙人。区块链投资包括： celer,ankr，quark，bumo，newton，blockcloud，uinp，nervos，path，merculet，cocos等项目。LeekLab创始人，中关村创投及基金协会理事，北京文创投融资协会副秘书长，中国人工智能产业联盟理事，前北大国际投资管理协会会长，中南创盟理事。
廖志宇Emma/超脑链Ultrain联合创始人
著名抗日英雄廖耀湘将军之后，就读美国常青藤名校Columbia University。前金砖资本合伙人，早期投资了人人车，蔚来汽车等项目，曾任360智能硬件投资总经理，欧洲顶尖投行goetzpartners中国区创始CEO，纽约私人银行国际客户总监。拥有全球顶级商业资源，深谙资本运作，跨境并购与TMT投资经验。
本文为火星财经原创稿件，版权归作者所有，未经授权不得转载，转载须在文章标题后注明“文章来源：火星财经”，若违规转载，火星财经有权追究法律责任。
