1. 链一财经首页
  2. 资讯

链安创始人:形式化验证方法是目前更完备解决安全问题的方法

6月3日,由CSDN、灵钛科技联合主办,火星财经(微信:hxcj24h)协办的“以太坊 技术及应用大会”在北京召开。成都链安科技CEO & 创始人杨霞在会议上发表了主题为“面向以太坊的智能合约形式化验证平台VaaS”的演讲。

微信图片_20180603181159.jpg

杨霞认为,采用形式化验证是解决智能合约和区块链底层平台问题的方法。她介绍了对智能合约验证的三个步骤,以及形式化验证的经典案例。

以下为杨霞演讲全文:

大家下午好!我与大家分享我们团队做的《面向以太坊的智能合约形式化验证平台VaaS》,这个形式化验证平台是为了提高智能合约安全性的。我们从2016年底开始做这个事情,现在已经做了一些东西出来,在今天的大会与大家分享。

我们是中国第一个从事区块链形式化验证的团队,去年九月参加“全球区块链峰会”时,我当时也站在讲台上分享了我们智能合约的形式化验证成果。今天我们做得东西更多了。

我们成立了一个公司叫成都链安科技,是中国首个专门从事区块链安全的公司,目前与国内十多家区块链行业的知名企业建立了长期的战略合作。

上午蒋总与大家分享了很多区块链的安全问题,据数据来看,80%的智能合约 是或多或少存在安全问题,特别是BEC,很小的一行代码导致了64亿人民币一夜之间蒸发,带来的教训非常惨痛 。对于这样的漏洞 ,链安科技可以快速查找出来。

针对解决智能合约和区块链底层平台面临的这些问题,我们怎么做?我们采用形式化验证的方法。形式化验证是一种数学的方法,在做区块链安全之前,我个人做形式化验证很多年,原来是给军口行业航空航天 安全关键的软件采用这种形式化验证方法来提高安全性。后来区块链的安全暴露出问题之后,我开始引用这个形式化验证方法到智能合约 中来,感到同样非常有效果。

形式化验证是一种证明我们这个软件或者硬件系统的正确性,它怎么证明?数学形式化的描述和数学的推理,是逻辑的推理。X可能是个软件,可能是个硬件,也可能是某个协议的系统,我们证明它是否达到我所期待的目标,要达到这个期待的目标的同时没有多的也没有少的,正好达到我所需求的。这个东西达到我需求的目标用测试就可以了,但测试是不完备的,不知道有没有其他问题,比如现在我查出了常见漏洞 ,但不能证明你没有其他的漏洞 。所以形式化验证方法是目前更完备的解决安全问题的方法,它难度非常高,门槛比较高。

它的目标是为了提高代码的正确性和可靠性,常规提高代码的质量有三种方法:大家熟悉的测试、中间的验证、评估。我们用的是其中验证的方法,它具有更高的完备性。这个图中间有验证和评估,中间一部分是测试,测试只能用于查找已有的bug,看我们的功能是否满足需求,同时输入 很多测试案例,看这个结果是否满足我们的要求,但它并不能证明你没有其他的,也就是说你测完之后心里还是没有底。因此,我们用数学手段去推理证明它,把代码变成公式,去证明它有没有其他问题出现。

我们现在对智能合约 的验证都采用这三个步骤,第一步,对智能合约或其他程序要完成的功能进行形式化的描述,第二步,对代码进行形式化描述,第三步,开始证明。

这是形式化验证的经典案例,它原来用到军方要求比较高的系统,在用到智能合约 之前大部分用在飞机、控制系统、军事机密的系统,我个人在此前也是为类似的系统做服务。这是我们的军事系统。这是我们两个软件的标准,CC是安全最顶级的标准,要求通过CC标准第五级以上的规范,必须经过形式化的验证。我个人非常荣幸加入CC标准,参与标准的撰写,最近它们联系我去给它们写一部分标准,我觉得还是蛮好的。

VaaS平台是经过一年半左右时间研制的形式化验证平台,采用多种形式化的技术,开发的一套面向多个区块链平台,目前对以太坊和EOS都提供支持,研究自己的一套形式化验证工具,智能合约 提供军事级的安全验证,杜绝逻辑漏洞 ,确保系统安全,这是我们已经做到的事情,最终输出安全的区块链平台。

我们的平常优势,是全球第一个支持EOS的,去年我九月份就已经宣讲了以太坊这块,但我没说我是第一个,因为做这个事情之前以太坊自己也有打算,虽然没有成果,我们在以太坊也是第一个支持的。我们的优势在于形式化验证的自动能力很高,因为形式化验证传统来讲需要大量人工参与,我们的优势是尽可能减少人工参与,更多用机器完成,所以我们做了一套验证工具。我们能够支持多个区块链平台,火币和Ok交易所指定我们做智能合约 安全审计。

我们提供几种验证服务,第一个,检测合约 是否存在常见,第二个是验证合约 中用户给定的功能属性 满足性,第三个是合约 的功能正确性验证,第四个是对底层区块链平台核心代码检查。

(短视频播放)这个是以太坊平台以BEC合约 为例,一键查出漏洞,精确定位到代码出错的位置,后面加上我们人工复核,把这个漏洞补上,把代码改了,再验证就通过了。

这是我们另外一个完备的证明工具,是有专利 的,可以把合约源代码自动转换成形式化的代码,再通过人工写定理。在没有用刚才那个转换之前,写这个定理需要180多行,而后面只需要30多行,这是自动化做的,也是我们的独创。比如对同样一个合约 ,人工验证要1000多行,但通过我们只需要200多行,减少人工干预,提高自动化能力。

根据国家《关于防范代币发行融资风险的公告》,大家应警惕代币发行融资与交易的风险隐患。

本文来自LIANYI转载,不代表链一财经立场,转载请联系原作者。

发表评论

登录后才能评论

联系我们

微信:kkyves

邮件:kefu@lianyi.com

时间:7x24,节假日bu休息

QR code