智能合约形式化验证工具真能解决问题么？
在智能合约的形式化验证过程中，需要专业的编程人员对不同模板的智能合约进行特征分析、模型建立和模型验证。现在市场上出现了一些一键式的智能合约形式化验证工具，据说可以最大程度的减少验证程序、发现bug，提高工作效率。这种一键式的智能合约形式化验证工具真的有效么？为了求真笔者做了一个测试。
本次笔者测试选择的是成都链安研发的离线版免费验证工具Beosin-VaaS。我们基于VSCode的插件市场安装一个sodility开发插件（具有语法检测，高量和语法联想，方便合约开发。），安装完成后，在插件市场安装成都链安的免费检测工具Beosin-VaaS。
合约代码如下：
我们用成都链安的插件检测一下我们合约中存在的问题
开始检测
我截取部分报错解释说明一下
插件报错会展示行号和那一行的代码以及描述信息，有助于开发人员修改问题
在调用call/send函数后无论执行成功还是失败都不会直接抛异常，如果不对调用返回值进行检查，函数会继续执行，造成安全漏洞。
溢出是典型的合约漏洞，可能导致检查被绕过，合约运行逻辑出错。
Solidity中允许有未使用的变量，它们不会构成直接的安全问题，但会降低代码的可读性并且额外占用存储空间导致部署时的资源消耗增加。
成都链安的检测插件集成了编译器的告警，会提示你一些合约开发中的信息。
在transfer、transferFrom、transferOwnership等敏感函数中，用户操作不可逆，所以建议开发者在这些函数实现中增加目标地址非零检查，避免用户误操作导致用户权限丢失和财产损失。
以上是我们这个合约中部分存在的漏洞报错，有了这个插件的检测，我们就能快速定位解决问题，使我们的合约更加安全。
智能合约形式化验证工具真能解决问题么？相关推荐
- 成都链安重磅出品 | 基于VS Code插件的智能合约自动形式化验证工具Beosin—VaaS『离线免费版』...
11月4日,成都链安重磅推出『离线免费版』智能合约自动形式化验证工具Beosin-VaaS,该版本基于流行的开发工具VS Code插件,供广大开发者免费使用.获得方式如下,欢迎体验使用: https: ...
- 智能合约自动检测工具『链必验』，如何带你解锁Web3.0世界
在我们发布[链必验]新版本之后,目前已有大批开发者前来试用,今天,我们还需要详细介绍这款工具. [链必验]智能合约自动检测工具,可用来检测区块链智能合约漏洞.平台针对每个用户模拟了一条单独的测试链,用 ...
- truffle （ETH以太坊智能合约集成开发工具） 入门教程
truffle (ETH以太坊智能合约集成开发工具) 入门教程 前言 在你了解区块链开发之前,你有必要了解区块链的一些基础知识,什么是DApp,DApp与传统app的区别, 什么是以太坊,以太坊中的智 ...
- 形式化验证工具TLA+：程序员视角的入门之道
简介: 女娲是飞天分布式系统中提供分布式协同的基础服务,支撑着阿里云的计算.网络.存储等几乎所有云产品.在女娲分布式协同服务中,一致性引擎是核心基础模块,支持了Paxos,Raft,EPaxos等多种 ...
- Scyther形式化验证工具简单教程
Scyther形式化验证工具 Scyther是一种自动化的安全协议验证工具.在协议的安全性验证方面有着广泛的应用. 下面介绍其安装方法以及使用教程. 安装方法 Scyther工具在Windows 10 ...
- FPGA形式化验证工具OneSpin360学习笔记（一）
目录 OneSpin360图形界面 一致性检查举例 等价性检查举例 Onespin是领先的EDA解决方案提供商,其360系列产品为FPGA形式化验证工具.它以强大.高性能的形式化验证引擎为基础,能够覆 ...
- 区块链论文7（oyente智能合约漏洞检测工具）
Making Smart Contracts Smarter 文章路径 参考链接1 参考链接2 参考链接3 Abstract: Cryptocurrencies record transactions ...
- 元宇宙里的新零售（DMall）技术（前端+智能合约）验证
文章目录 起因 DMall是什么 商业模式 技术实现 背景 虚拟世界里的资产运营 Decentraland(一个完整的元宇宙世界该有的样子) DMall为什么是有效的数字化创新 技术验证 智能合约 P ...
- Oyente：智能合约漏洞检测工具的安装与使用
写在前面 当你阅读到这篇 博客 时,大概率你已经阅读并尝试过 Oyente 官方安装指导,甚至可能还在其它地方搜过安装教程,如果没有就当我没说... 那为什么在有各种版本的教程的情况下我依旧去写一个新 ...
- NEO智能合约反编译工具
2019独角兽企业重金招聘Python工程师标准>>> 0x00 前言 下拉最后看演示效果.项目地址 本来这应该是一个很和谐的感恩节假期,本来我可以很悠闲的写完所有作业然后随便看点论 ...
最新文章
- R语言使用dplyr聚合统计分组数据、ggplot2可视化分组线图、使用geom_line函数自定义设置线条类型、粗细、颜色(Change line types + colors by groups)
- 服务器根目录文件配置文件,在文档根目录中存储安装和配置文件
- K-means Algorithm 聚类算法
- linux+sar+服务,sar服务监控Linux
- Linux搭建NFS文件服务器
- 【JAVA】java中split以“.“ 、“\“、“|”分隔字符串
- MATLAB获取字符串中两个特定字符之间的内容
- 初等函数的麦克劳林级数展开+逆函数的展开求法
- PostgreSQL行级安全策略RLS和数据加密
- C++实现通用的文件（万能）加密方案——包含源码
- 文献调研之如何查找文献及源码
- c语言大作业小学生测验,小学生测验 面向小学1~2年级学生，随机选择两个整数进行四则运…...
- 【自动化测试】推荐一款超好用的ui自动化工具--uiautomator2
- 性能测试 - - 常见的性能测试指标
- grub rescue 之 Ubuntu 删除的问题
- linux下使用sdkmanage安装sdk
- 编写一个程序从键盘输入字符，并按要求输出
- python UnicodeDecodeError: 'utf-8' codec can't decode byte 0xbd in position 0: invalid start byte
- 北斗三号短报文终端在大坝安全监测方案的应用
- 微电网并离网下垂控制simulink模型，只有模型，支持MATLAB2018版本