如何评价形式化验证?

485次浏览

形式化验证应用在智能合约里真的就能确保万无一失了吗?
回答
1个回答

李笑来会哭吗

2018-11-06

李笑来会哭吗,吴忌寒怕热吗

        广义上讲, 形式化验证 方法是借助数学的方法来解决软件工程领域的问题,主要包括建立精确的数学模型以及对模型的分析活动。狭义的讲,形式化方法是运用形式化语言,进行形式化的规格描述、模型推理和验证的方法。就形式化建模而言,形式化表示必须包含一组定义其语法语义的形式化规则。这些规则可用于分析给定的表达式是否符合语法规定,或证明该表达式具有某种性质。形式化验证补充了模拟验证的不足,二者各有优势,互为补充,缺一不可

| 讨论形式化验证,必须要先讨论形式化规范

 

形式化规范 (formal specification) 是指通过数学语言对系统的预期行为 (例如将数量 S 的 token 从账户 A 转移到账户 B) 和性质 (例如转账不会造成账户 B 额度的溢出) 进行严格和全面的定义。形式化规范往往定义了系统的正确性和安全性

 

给定一个系统的形式化规范,我们即可以从规范出发开始迭代设计和实现出这个系统。在迭代的每一步中,我们可以通过精化 (refinement)、集成 (synthesis) 、形式化证明在内的一系列方法在数学上严格的保证迭代产生的系统和迭代前的规范或者系统保持一致。

 

除了从形式化规范出发设计和实现一个系统,我们也可以使用包括符号执行 (symbolic execution)、模型检测 (model check) 和形式化证明 (formal proving) 在内的一系列方法验证已有的设计和实现与该规范保持一致。

 

| 安全攸关的区块链领域

 

区块链领域亦然,一方面,小错误也会导致大损失;另一方面,巨大的经济利益也会吸引大量的攻击者。

 

以太坊黑客攻击第一大案The DAO中,攻击者窃取了当时价值5500万美元的以太币,并且导致了以太坊的硬分叉;这之后,与以太坊智能合约相关的攻击一直在继续——比如,2017年11月,以太坊Parity钱包由于被黑客攻击,导致用户损失了价值约为1.5亿美元的数字资产。

 

据统计,仅2018年上半年,就已经有大约11亿美元的数字资产被盗,与区块链系统相关的漏洞(如以太坊中的智能合约漏洞)以及围绕数字资产的生态系统安全问题(如多个中心化交易所被盗)更是层出不穷。

 

目前区块链系统中的相关漏洞,以及数字资产生态系统的安全问题,归根结底是相关程序设计与实现的问题。在形式化方法以前,这类问题多是通过程序测试来发现的。

 

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

 

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

 

| 结论

 

大多数人认为形式化验证方法高深莫测,究其原因,形式化验证方法不是一种通用技术,而是需要和领域结合来发挥价值的一种特定技术。在区块链领域,形式化方法究竟是一种nice to have还是一种must have,也是与项目特点密不可分的。

 

随着区块链技术与项目应用的探索不断深入,项目方对于规避错误、对抗黑客攻击和避免财产损失的需求已经越来越强。

 

当互联网世界中的绝大部分活动都完成上链,当社会中的绝大部分群体都需要区块链的绝对安全来保护自己的财产安全的时候,形式化验证方法作为区块链技术的must have才会迎来大爆发。

0评论