CertiK:一款智能合约的代码审计平台 – 作者:2benben

屏幕快照 2018-07-10 00.00.08.png

致谢:Gemii的技术顾问wlj,感谢阿里的zf,感谢Kevin老师引荐大家认识。作者是个沦为天使投资人的传统行业工程师

这几天跟wlj聊区块链上挖洞的问题,天天被我骚扰的wlj推荐了这个,据说是zf当年导师搞得,作为大牛们的学生,搜了点资料,记了点笔记,见花献佛。

2015年开始,鉴于大家的共识、实际上链应用逐步丰富及群体的不理性导致以太坊市值暴涨。有巨大利益之处必有人性的“光辉”, 首先是ICO的发行和认购炒作,如IPO必须经过审计一样,只看白皮书不审计Github上托管的代码(有无、是否原创、功能是否有效)就认购token是一种极度非理性行为,也会间接打击到诚实开发者的积极性。 另外,基于ERC20标准开发的智能合约部署和运行在区块链上,三点原因导致其成为安全的巨大挑战:

1) 与传统软件不同,一旦智能合约上传主链则无法更改

2)上链的DAPP难以调试,特别是与在链其他合约之间的交互

3)对于的Hacker,由于涉及利益巨大,更有动力去挖区块链上智能合约的漏洞。[1] 做空、投机和Hacker有很大可能毁灭信任,打击生态,因此区块链上DAPP的代码审计工具非常有意义。

CertiK是一款通过数学方法(形式化证明)验证智能合约漏洞的分布式应用,CertiK开发了一种基于层的方法,将待审计的代码按照逻辑上的层分解为较小的证明任务,在于分布式的网络中分包并完成证明生成代码审计报告。Certik基金会的工作由耶鲁和哥伦比亚大学三位教授主持。 

屏幕快照 2018-07-09 22.52.20.png

这款分布式应用解决了三个问题:

1)一款区块链上的分布式应用整体的代码审计,而不是针对某几个函数

2)如何分包代码审计任务

3)如何让代码审计的发包和分包方互相信任 ,完成工作。 

为了解决这几个个问题,他们使用了多种实现手段:

1)智能标签 给待审计的DAPP代码的智能标签,贴标签不仅基于符号,更基于语义识别。

屏幕快照 2018-07-09 23.58.40.png2)采用他们命名的 ‘layer deep specification“ 将待审计代码分层,按照互相依赖的关系分解成许多简单模块,在分布式网络上发包,把复杂的任务简单化。

屏幕快照 2018-07-09 23.58.49.png

3)开放接口,方便多种自动验证算法接入平台验证。

4)便于机器检验的对象

5) 安全的Dapp库和插件,为了提高整个区块链社区的代码质量和可靠性,CertiK平台为集成开发环境(IDE)提供了一系列经过认证的库和插件,付token(他们的token叫CTK,后面会提到)就可以拖下来使用。

6) 定制化的代码审计内容和报告

CTK是这个分布式应用上的token和fuel,发包代码审计任务需要消耗CTK,执行审计和验证任务的节点可以获得CTK。CertiK平台引入了一种新的采矿方案,名为Proof-of-Proof(PoP)。传统的挖矿PoW (Proof-of-Work)原理是矿工找到有效区块,即将监听到的广播交易逐层哈希加密打包成merkel Tree状数据结构,穷举法找到一个随机数,使整个区块的哈希值小于目标值,  在CertiK团队看来,这种浪费算力的行为没有任何价值 (我也这么认为,费电费机器)[2] 。这个PoP方案通过CTK在五个不同角色中的流动来统一整个社区:

屏幕快照 2018-07-09 23.57.50.png

1) 客户(Customer) – 比如需要代码审计的开发者,可以向CertiK平台的网络提交需要验证的程序/系统或符合开放协议的任何证明义务(符合开放协议)

2)赏金猎人 (Bounty hunters)- 是那些希望CTK激励并希望分享他们的计算资源的人。他们提供算力完成证明和代码审计,然后等待验证。由于此角色的重要性,只允许拥有一定数量CTK的用户担任此角色。

3)检查员 (Checkers) – 验证证明和代码审计结果,可以通过记录定期交易或检查提交的证明对象来获得CTK奖励。赏金猎人只有在证明得到验证后才能获得奖励,监察员也可以获得这些奖励的一小部分。

4)Sages – 是通过CertiK平台的开放协议提供工具(验证算法引擎)的人。他们提供的工具可能被赏金猎人随机使用,可以根的评估结果获得一些CTK奖励。优秀的工具将由社区研究和传播。

5)用户(User)用户可以订阅所有CertiK平台的认证库和IDE插件,支付部分CTK,搭建自己的DApps。 (买乐高搭积木) 

CertiK尚未发token, 主要的代码审计竞争对手是Zepplin和Quantstamp,Zepplin是人肉验证的基本安全的智能合约模版库,想自己写的拖出来稍微改改就可以了,因为被很多只眼睛看过,相对比较安全。但CertiK车飙的更猛,完全通过形式化证明这种数学方法和分布式的系统查找Dapp代码中的逻辑漏洞,完成代码审计工作。 

结论: 

1. Certik技术更牛,牛在普适和严格,而非基于人肉的经验,看好CTK。

2. 区块链自身数据结构特性和巨大的利益承载,使得分布式应用的代码审计非常必要,不仅能够提高代码质量,避免被黑,(反着说就是区块链上的应用难以调试,难以更改,挖洞更有价值) ;也能有效识别空气币的源代码,砸中真正有应用价值的Dapp。

3. 买token前一定要看代码,一定要看代码,一~定~要~看~代~码。

引用:

[1] Ivica et al.  Finding The Greedy, Prodigal, and Suicidal Contracts at Scale http://ilyasergey.net/papers/maian-draft.pdf

[2] 区块链 – 技术驱动金融 : 数字货币与智能合约技术 2016.8  中信出版集团

屏幕快照 2018-07-09 23.58.16.png *本文作者:2benben,转载请注明来自FreeBuf.COM

来源:freebuf.com 2018-07-19 15:00:13 by: 2benben

© 版权声明
THE END
喜欢就支持一下吧
点赞0
分享
评论 抢沙发

请登录后发表评论