建议和反馈

请填写你的反馈内容

智能合约安全分析简述

2020-03-26 ·2123次阅读 ·读完需要9分钟

智能合约背景

以太坊正在被打造成一种能在单一平台上实现多种可能性的区块链生态系统,而智能合约是为了让人们在平台上实现更深层次的开发而设计的。

智能合约的价值主要是因为它可以与区块链发生关系,数据来源于区块链链上,执行在链上,输出结果在区块链上,而区块链上承载着一个国家的法律,这是区块链被称为“主权区块链”的原因。智能合约与区块链的结合形成了智能合约法规自动执行系统。


智能合约安全分析的原因

智能合约本质是一段运行在区块链网络上的代码,在设计和开发的过程中,不可避免的出现漏洞,部署在公链上的智能合约,由于暴露在开放网络上,容易被黑客获得,成为攻击目标,而智能合约又是不可逆的,如果出了问题,可不是给客服打电话就能解决的,也不是修复bug就有效的,区块链行业中很多人经历过 The DAO 事件,一小段时间内,大家眼睁睁看着黑客不断的把大家智能合约中的钱转走,教训很惨痛。对于区块链领域,代码即法律,代码控制着我们的数字身份,控制着我们的智能合约中的资金,因此保证智能合约的安全是非常重要的。

In contrast to classical distributed applications that can be patched when bugs are detected, smart contracts are irreversible and immutable. There is no way to patch a buggy contract, regardless of its popularity or how much money it has, without reversing the

blockchain(a formidable task).


在这样的背景下,如何有效保障海量智能合约的安全?降低人工审计复杂度,采用智能合约自动化审计,是发展趋势, 但现在自动化审计方法处于一个很不成熟的阶段,主要面临三大问题:误报率高,自动化程度低、依赖人工二次审计,审计时间比较长。


智能合约自动化审计

特征代码匹配

第一种是特征代码匹配,就是对恶意代码进行提取、抽象,形成匹配模块对待检测源码进行检测。优点是速度快、迅速响应新漏洞,缺点则是使用范围有限、漏报率高。


形式化验证formal verification

第二种是基于形式化验证的自动化审计方法。最早是在2016年由Hirai提供的,Grishchenko和Hildenbrandt进行改进,采用了Fframework和K-framework,将EVM转化为一个Formal model。F framework是航空航天领域常见的形式化验证框架,而K-framework则是一个语义的转化框架。


所谓形式化验证方法,是一种特殊的基于数学的技术,基于已建立的形式化规格,对所规格系统的相关特性进行分析和验证,以评判系统是否满足期望的特性,用于规范、开发和验证软件和硬件系统,以提高系统的安全性、可靠性和鲁棒性。形式化方法可以形容为建立在相当广泛的理论计算机科学基础上的应用,特别是逻辑演算、形式语言、自动机理论、离散事件动态系统和程序的语义,还包括类型系统和代数数据类型等理论。


一般这类研究主要应用于昂贵的航空、航天、军事器材的操作系统、危险的医疗设备程序之中。如果事关生死,高成本也值了。比如我们要写控制火车调度的软件,或者写控制医疗设备的嵌入式软件,那么仅仅写几行测试代码,或者交给黑盒测试团队,去覆盖百分之九十九的可能,这是远远不够的。我们需要不计成本的去提高软件的可靠性,这时候形式化验证就很有必要了。


形式化验证并不能完全确保系统的性能正确无误,但是可以最大限度地理解和分析系统,并尽可能地发现其中不一致性、模糊性、不完备性等错误。形式化验证可用来消除高风险代码漏洞。

形式化验证进入区块链领域的初期,以太坊社区的Yoichi Hirai对以太坊(Ethereum)的智能合约虚拟机EVM做了完整的形式化建模。此外,来自UIUC大学的团队也对EVM进行了形式化的建模和验证[12]。EVM是以太坊智能合约的底层核心,关系到以太坊安全,涉及到数字资产保护等重大议题,引起了社区的广泛关注。


此外,MakerDAO项目方发布了第一个经过形式化验证的去中心化应用程序(DApp)。MakerDAO 是一个基于以太坊的智能合约平台,该平台提供了稳定币(stablecoin),抵押贷款(collateral loans),以及去中心化社区治理功能。为了保证所部署的智能合约的安全性,MakerDAO团队对抵押贷款(CDP)核心引擎合约代码通过K-Framewok进行了验证,因此而表明其智能合约程序能够完全抵抗黑客攻击。


符号执行 sybolic execution

最后一种是现在最常用的方法,基于符号执行和符号抽象自动化审计:是通过符号表达式来执行路径的一种静态分析技术,程序执行用符号来模拟,输出是包含这些符号的逻辑或数学表达式。

分析智能合约时,通过编译源码,可以形成EVM OPCODE,然后输入到自动化分析引擎,转化成CFG,再利用这两种方法进行分析。比较典型的是Oyente和Securify 系统,可以降低误报率和漏报率,但是分析方法繁琐并且耗时。



评论(0)问答(0)
请先登录或注册

请先登陆或注册

相关推荐

比特币交易原理分析

1.比特币的UTXO模型首先,在讲比特币交易过程之前要说明一个事情。比特币系统是没有余额的概念的,它使用的是UTXO模型(Unspent Transaction Outputs,未使用过的交易输出),......
花落 · 2020-04-07
525阅读 · 0赞赏 · 0问答

极速赛车高手计划364790稳赚群

极速赛车高手计划364790稳赚群......
GavinIsabella · 2020-04-05
77阅读 · 0赞赏 · 0问答

极速赛车人工计划群364790

极速赛车人工计划群364790......
GavinIsabella · 2020-04-05
71阅读 · 0赞赏 · 0问答

Serpent 指南

有关Serpent 1.0的信息请查阅以前的文档Serpent是一种用来编写以太坊合约(Ethereum Contract)的高级编程语言。Serpent翻译成中文意思是”大蛇”,如这个名字所示,这是......
gomez · 2020-04-03
320阅读 · 0赞赏 · 0问答

分析区块链链下扩容:状态通道、TrueBit、Plasma

我们正处于区块链 2.0 转化的时代,目标是大规模的商用。传统的区块链技术,如比特币和以太坊,在性能上面已经显得力不从心,本文就来聊一聊区块链链下扩容技术。比特币和以太坊有多快?作为史上最慢的分布式数......
区块链开发 · 2020-04-01
390阅读 · 0赞赏 · 0问答

说说区块链扩容之 Layer2 的扩展

 前言:自区块链技术诞生以来,对其“性能”的诟病就从来没有停止过。虽然从技术上说,一个基于分布式对等网络架构的系统,与成熟的中心化技术相比,其“性能”方面有着天然的劣势,但业内人士对区块链“......
区块链技术 · 2020-04-01
455阅读 · 0赞赏 · 0问答

月月月

2430

LK币

3

粉丝

37

笔记

感谢"月月月"

这篇精彩的笔记,目前已经帮助

  • 0
  • 2
  • 1
  • 2
  • 3
喜欢0
链客社群 加入

微博进入

商务合作>

广告投放>

公司名称:北京链客行科技有限公司

联系方式:010-67707199

ICP备案号:京ICP备18032136号

Copyright:链客区块链技术问答社区 版权所有

感谢您的提问,问题被社区永久收入以便新人查看。一定要记得采纳最佳答案哦!加油!

感谢您的善举,每一次解答会成为新人的灯塔,回答被采纳后获得20算力和相应的LK币奖励

您将赞赏给对方2LK币的奖励哦!感谢您的赞赏!

您将赞赏给对方2LK币的奖励哦!感谢您的赞赏!