形式化验证工具之离线免费版Beosin—VaaS
形式化验证工具之离线免费版Beosin—VaaS
近期，笔者注意到一款智能合约自动形式化验证工具Beosin—VaaS推出了离线免费版。所谓**“离线免费版”，相较于之前该公司推出的在线免费版、企业版而言，亮点自然不言而喻。对于开发者来说，离线版的验证工具将提供一个不联网的测试环境，在很大程度上能从根源上将黑客攻击的可能拒之门外。
经笔者测试，虽然这次推出的版本为免费版，但功能毫不逊色，依然能有效检测出智能合约的常规安全漏洞，并精确定位到有风险的代码位置，以及导开发者修改合约代码。**对大多数智能合约的安全性而言，需求都已经满足。在此附体验网址：https://beosin.com/#/，有需要的朋友可自行前往体验。
尽管笔者认为离线免费版Beosin—VaaS的功能已足够强大，但根据官方发布的消息，对于一些复杂类型的业务合约、以及对安全性要求高的业务合约，比如数字金融类（如DeFi）、物流供应链类、跨境支付类、防伪溯源类等等，还是建议选择企业版Beosin—VaaS或人工审计服务更好。
下面笔者将针对这款离线免费版Beosin—VaaS工具进行简单展述。
1.什么是形式化验证技术？
其实，形式化验证技术最早是应用于航空、军事等领域的安全关键软件中的技术，本身受众范围没那么广。当成都链安最早尝试将形式化验证技术应用在验证智能合约的安全性上，最后发现审计效果比起传统的验证方式，更具备优势。
**形式化验证技术是一种基于数学和逻辑学的方法。**具体来讲，在智能合约部署之前，对其代码和文档进行形式化建模，然后通过数学的手段对代码的安全性和功能正确性进行严格的证明，可有效检测出智能合约是否存在安全漏洞和逻辑漏洞。
该方法可有效弥补传统靠人工经验查找代码逻辑漏洞的缺陷，其优势在于，用传统的测试等手段无法穷举所有可能输入，而用数学证明的角度，就能克服这一问题，提供更加完备的安全审计。
2.什么是Beosin—VaaS工具？
Beosin—VaaS相关工具就是将形式化验证技术应用在对智能合约安全性验证的集大成者。Beosin—VaaS能够面向EVM和WASM智能合约，自动化检测智能合约的10大项32小项常规安全漏洞，为智能合约提供**“军事级”的安全保护**；并精准定位风险代码位置并给出修改建议；检测准确率>97%，全球最高；从源码到字节码完备的形式化验证；支持多个智能合约编程语言，如Solidity、Go、C++、Python等。
3.一些Beosin—VaaS的测试实例
笔者选取了655个测试问题进行检测，Beosin—VaaS工具总计检测出635个问题，命中率为96.9%；误报共115个，误报率为15.3%。因此，Beosin—VaaS工具可检测出业务类大多合约案例，具体检测项如下：
Beosin—VaaS工具检测项
| 漏洞检测项 | Beosin—VaaS工具 |
|---|---|
| ERC20 标准规范 | √ |
| Fake Recharge Vulnerability（假充值） | √ |
| TransferToZeroAddress（目标零地址检测） | √ |
| Re Entrancy（重入） | √ |
| TXOriginAuthentication（tx.origin使用错误） | √ |
| Invoke Low Level Calls（call调用,delegatecall调用,自杀函数调用） | √ |
| BlockMembers Manipulation（区块参数依赖） | √ |
| Invoke Extcodesize（调用Extcodesize函数） | √ |
| Invoke Ecrecover（调用Ecrecover函数） | √ |
| Unchecked Call Or Send Return Values | √ |
| （call和send的返回值检测） | √ |
| Redefine Variable From Base Contracts（合约继承中的变量覆盖） | √ |
| Unprotected Ether Withdrawal（无保护的转账） | × |
| Check This Balance（合约资金受到严格限制） | √ |
| ArbitraryJumpwith Function（具有函数类型变量的任） | √ |
| Overload Assert（重写assert函数） | √ |
| CompilerVersionDeclaration（编译器版本声明） | √ |
| Constructor Mistyping（构造函数失配） | √ |
| Unary Operation（+= 写成=+ ） | √ |
| No Return（返回值适配） | √ |
| Unchecked Api Return Values（没检查API返回值） | √ |
| Emit Event Beforerevert(事件在revert前触发了) | √ |
| Integer Overflow（整数溢出） | √ |
| Exception State(异常检测，包括数组越界、除0、assert失败等)） | √ |
| Call problem | √ |
| Function problem | √ |
| Require Fail | √ |
通过大体测试，离线免费版自动形式化验证工具Beosin—VaaS在很大程度上都能够满足大多数开发者的验证需要。大家可以前往https://beosin.com/#/进行体验，不吝赐教。