作者:JSIA / NBIA
15.区块链安全
2018 年以来,随着区块链的快速崛起,智能合约应用也出现井喷式爆发。
然后由于诸多因素限制,智能合约安全问题更是层出不穷。
由于区块链天然的金融属性,以及区块链本身不可篡改和全公开的特性,得一旦暴露合约漏洞,造成的损失将不堪设想。目前智能合约审计的主要形式是合约代码测试和审计。合约代码测试一般采 用自动化测试工具完成,自动生成大量的测试用执行合约来进行测试,检测在尽 量多的条件下,合约是否能够正确执行。但由于测试用例无法保证 100%覆盖所 有的情况,所以,即使测试结果没有发现问题,也不能保证合约的实现一定没有 漏洞。合约代码审计是由安全审计人员对合约源码从代码实现和业务逻辑等多个 角度进行审计。安全团队能够检查出大部分的合约漏洞和隐患,并在业务逻辑的 实现上给与项目方指导或者建议。但由于审计工作在一定程度上依赖于审计人的自身经验和主观判断,并不能 100%完全杜绝安全风险和漏洞。
另外一些较为复杂的业务逻辑以及更高阶的性质,如经济学,博弈论范畴问题,通过测试或者审计的方式更是难以有效验证。
苏州链原信息科技有限公司安比实验室的合约审计采用了测试+人工审计+ 形式化验证相结合的方式进行的。
形式化证明是通过形式化逻辑的方式来表示合约代码,这个过程依赖于严密 的数学逻辑推理,可以明确保证在一定范围内的绝对正确,能弥补以上两种传统 方式的局限。因此形式化证明在一些安全攸关的领域,如航天、高铁、核电、航 空,已经逐步得到应用,并且取得了非常好的效果。
智能合约代码,同样也是对安全要求极高,因而对于规模相对较小而设计杂的智能合约而言,形式化程序验证无疑是保证其安全可靠的有效方法之一。这 也是全球首个完成对大型 DApp 的形式化验证。
本文链接:https://www.hellobtc.com/kp/mt/09/2197.html
来源:白话区块链