基于VS-Code插件的智能合约自动形式化验证工具Beosin-Vaas离线免费版

11月4日，成都链安重磅推出离线免费版智能合约自动形式化验证工具Beosin—VaaS，该版本基于流行的开发工具VS Code插件，供广大开发者免费使用。获得方式如下，欢迎体验使用： https://beosin.com/#/

在此之前，成都链安已于2018年8月推出的在线免费版智能合约自动形式化验证工具Beosin—VaaS（网址：https://beosin.com/vaas/），已累计为企业和个人用户提供了7万多次的智能合约安全检测，得到了技术极客、开发者、项目方等一致的广泛好评。

为更好地服务于区块链行业，并深度践行中共中央政治局在第十八次集体学习中“推动区块链安全有序发展”的重要讲话，成都链安正紧随行业东风，以此为入局，现特推出基于流行开发工具VS Code插件的离线免费版智能合约自动形式化验证工具Beosin—VaaS！

产品背景

伴随着区块链概念的大火，区块链应用场景已开始由金融领域延伸到物联网、智能制造、供应链管理、数据存证等多个领域，其构建的可信机制生态，将能够彻底改变当前社会商业模式，引发新一轮技术创新和产业革命。

提到区块链应用场景，智能合约作为其中重要一环，就很难被忽略。智能合约作为区块链实现可信价值交换的核心技术手段，定义了整个链上交易过程中的所有逻辑规则，允许在没有第三方的情况下进行可信交易，这些交易可追踪且不可逆转。

随着区块链可赋能的应用场景越来越广泛，智能合约的安全问题也随之面临着爆发增长的风险。据不完全统计，自2011年至2019年10月期间，全球范围因区块链安全漏洞而造成的经济损失就高达84亿美元之多，因智能合约所导致的就占了三分之一以上。其中，以以太坊链平台为例，有89%的智能合约代码都或多或少存在安全漏洞或隐患。

那么，如何在区块链应用上线之前验证智能合约的安全性，是推进区块链大规模落地应用的核心问题。当智能合约部署到链上以后无法轻易修改， “事前防护”就变得尤为重要。（“事前防护”指在代码编写过程中的规范化与代码发布前的安全检测）。

成都链安作为最早将形式化验证技术应用到区块链安全领域的团队，对智能合约的“事前防护”方面十分看重；并在此衷心建议：智能合约开发者需要尽量在参考优质模版的基础上，使用安全库，并在开发完成后使用Beosin-VaaS（网址：https://beosin.com/#/）或人工审计服务对合约代码进行全方位的安全检测。做好“事前防护”，避免上线不安全的智能合约，进而影响区块链全网生态安全。

产品介绍

Beosin—VaaS作为成都链安安全矩阵“一站式”区块链安全平台的核心一环，是由成都链安团队结合多年来在区块链安全攻防实战中所累积的实践经验而自主研发的。作为一款针对智能合约的安全检测定制化工具，可精准定位风险代码位置并给出修改建议；可“一键式”自动检测出智能合约的10大项32小项常规安全漏洞，检测准确率>97%，全球最高，为智能合约代码提供“军事级”安全防护。

同时，Beosin—VaaS的可定制化和可移植性一直以来都是该工具的核心亮点。Beosin—VaaS不但支持BCOS、ETH、EOS、Fabric、ONT等多个主流链平台，还支持适配使用EVM和WASM智能合约的公链和联盟链平台。并面向这些平台，针对性增加新的检测项。

产品特点

Beosin-VaaS具有以下显著特点：

• 自动化程度高，“一键式”自动定位代码漏洞位置；
• 检测准确率>97%，全球最高；
• 从源码到字节码完备的形式化验证；
• 支持多个公链和联盟链平台；
• 支持多个智能合约编程语言，如Solidity、Go、C++、Python等。

另外，本次推出的离线免费版Beosin—VaaS，是继在线免费版Beosin—VaaS（网址：https://beosin.com/vaas/）之后，针对以太坊（Ethereum，简称ETH）智能合约安全检测开发的定制化工具，支持Windows、Linux和MACOS。以太坊应用开发者可通过VS Code插件市场免费获取和使用。

需要指出的是，尽管免费版Beosin—VaaS的功能已经足够强大到有效检测出智能合约常规安全漏洞，并精确定位到有风险的代码位置、指出风险原因、指导开发者修改合约代码，对一般性的智能合约安全性而言，需求已经满足。

但成都链安建议，对于数字金融类（如DeFi）、物流供应链类、跨境支付类、防伪溯源类等复杂性业务合约、以及对安全性要求高且应用逻辑复杂的合约，选择企业版Beosin—VaaS或人工审计服务，将能够进一步保障合约安全性，避免上线有漏洞或功能不正确的智能合约带来潜在损失。

免费版、企业版以及人工审计服务对比如下：

注意事项

使用离线免费版Beosin—VaaS，需要注意以下事项：

• 本工具整个测试过程均在本地完成，这样可打消开发者对合约代码泄露的顾虑。另外，本工具基于VS Code 实现了ETH智能合约的代码高亮与代码补全，方便用户一边开发一边测试，在发现问题后迅速定位，快速修改。
• Windows系统的用户，需 保证电脑装有Node.js和Visual C++库，否则插件运行时可能出错。

Node.js下载地址： https://nodejs.org/zh-cn/download/

Visual C++库下载地址： https://visualstudio.microsoft.com/zh-hans/downloads/

选择其他工具和框架中的Microsoft Visual C++ Redistributable for Visual Studio 2019下载安装。

• 安装方法：打开VS Code，在其拓展超市中，搜索Beosin-VaaS: ETH，选择安装即可。
• 使用方法：安装完成后使用VS Code打开合约项目，选择合约文件 -> 右键（即可看见Beosin-VaaS: ETH选项）：

第一次选择Beosin-VaaS: ETH选项，会出现以下界面，用于选择需要用到的编译器： 

选择完成后，便会下载所选版本编译器，出现以下界面： 

下载完成后，便会出现操作界面：

点击Settings按钮（右上角⚙）可自定义部分测试参数：

Process Limit表示最多同时运行的进程数量。（可限制CPU核数，核数越多，测试时间越短）

Time Limit表示时间限制，超过时间测试将自动结束。

选择将要测试的合约路径，输入主合约的名字，点击Start按钮开始测试：

测试可能需要一段时间，请耐心等待。

若想要停止测试可点击End按钮，此时结果显示为当前已进行的测试结果。

完成测试后，最终结果显示如下：

版本说明

此版本为基于VS Code插件的『离线免费版』，供广大开发者免费使用。对于安全性要求高且应用逻辑复杂的合约，建议选择企业版Beosin—VaaS或人工审计服务，以进一步保障合约安全性，避免上线有漏洞或功能不正确的智能合约带来潜在损失。

在使用中，开发者若有任何意见和建议，欢迎通过VS Code插件市场Q&A或以下联系方式，向我们反馈和获得技术支持。当然，若需要企业版Beosin—VaaS、人工审计、定制化适配等服务，也欢迎联系我们了解详情。

关于我们

总部：成都市武侯区世纪城南路599号天府软件园D7座504室

分部:

北京市朝阳区广顺北大街36号 梦想加空间305室

深圳市南山区讯美科技广场3号楼16D

电话：028-83262585

邮箱：vaas@lianantech.com

微信公众号：

客服微信：

区块链行业东风正起，伴随而来的区块链安全问题也必将越发凸显。各行业“区块链+”模式应该如何赋能？智能合约的落地应用和安全检测又应该如何得到进一步提升？在这样的背景下，成都链安将在未来的日子里，深刻思考，潜心耕耘，为区块链安全事业研发出更多诸如Beosin-VaaS的安全产品。

响应国家部署局，推动产业发展，深耕区块链安全领域，筑起区块链安全防线，成都链安责无旁贷！

本文来自 深入浅出区块链社区合作伙伴：专注于区块链生态安全的Beosin 成都链安

深入浅出区块链 - 打造高质量区块链技术博客，学区块链都来这里，关注知乎、微博 掌握区块链技术动态。