其他
Beosin VaaS ,形式化验证工具如何构筑智能合约的“高级防线”?
Beosin VaaS,一款全球领先的“一键式”智能合约形式化验证平台。检测准确率高达97%以上,精确定位风险代码位置并给出修改建议,自动检测智能合约80余项的常规安全漏洞及功能逻辑缺陷。现已拥有生态用户10万+,Beosin VaaS可自动发现智能合约中存在的常规漏洞、业务逻辑错误等安全问题,并给出专家的修复意见。同时支持evm,wasm的所有公链的智能合约的上百种常规安全漏洞和业务逻辑缺陷检测,能精确定位风险代码位置,帮助开发者提高智能合约的安全能力。
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;
contract ETHGame{
struct BattleWizard{ //定义决斗属性
bytes32 currentDuel; //决斗场
uint power; //决斗能量
}
mapping (uint => BattleWizard) public wizards; //记录每个巫师的信息
mapping (bytes32 => mapping (uint => uint256)) public revealedMoves; //记录各个巫师各场的决斗的胜负信息
function resolveTimedOutDuel(uint256 wizardId1, uint256 wizardId2) public{ //更新处理超时情况下的巫师决斗结果
BattleWizard storage wiz1 = wizards[wizardId1]; //巫师1的决斗属性
BattleWizard storage wiz2 = wizards[wizardId2]; //巫师2的决斗属性
bytes32 duelId = wiz1.currentDuel; //巫师1的决斗场
require(duelId != 0 && wiz2.currentDuel == duelId); //约束:巫师1的决斗场存在,并且巫师2的决斗场需和巫师1的决斗场相同才可以继续进行后续操作
if (revealedMoves[duelId][wizardId1] != 0){ //如果巫师1满足胜利条件,则更新决斗能量
_updatePower(wiz1,wiz2.power); //更新巫师1的能量,将巫师2的能量给巫师1
wiz2.power = 0; //巫师2的能量清零
}
}
function _updatePower(BattleWizard storage wizard, uint256 power) private{ //定义巫师能量更新接口
require(wizard.power + power >= wizard.power); //确保巫师更新后的能量不少于更新前的能量
wizard.power = wizard.power + power; //执行巫师能量更新
}
}
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;
contract ETHGame{
struct BattleWizard{
bytes32 currentDuel;
uint power;
}
mapping (uint => BattleWizard) public wizards;
mapping (bytes32 => mapping (uint => uint256)) public revealedMoves;
function resolveTimedOutDuel(uint256 wizardId1, uint256 wizardId2) public{ //巫师1和巫师2决斗属性更新接口
BattleWizard storage wiz1 = wizards[wizardId1];
BattleWizard storage wiz2 = wizards[wizardId2];
uint old_power1 = wiz1.power; //记录巫师1决斗前的能量
uint old_power2 = wiz2.power; //记录巫师2决斗前的能量
bytes32 duelId = wiz1.currentDuel;
require(duelId != 0 && wiz2.currentDuel == duelId);
if (revealedMoves[duelId][wizardId1] != 0){
_updatePower(wiz1,wiz2.power);
wiz2.power = 0;
}
assert(wiz1.power+wiz2.power == old_power1+old_power2); //添加assert断言:确保状态更新前后总的决斗能量不发生变化
}
function _updatePower(BattleWizard storage wizard, uint256 power) private{
require(wizard.power + power >= wizard.power);
wizard.power = wizard.power + power;
}
}
wiz1.power+wiz2.power = old_power1+old_power2+0 = old_power1+old_power2;
wiz1.power+wiz2.power = 2*wiz2.power = 2*0 = 0。