正式验证指南

正式验证指南

1. 正式验证简介

什么是正式验证？

正式验证（Formal Verification，FV）使用数学建模和逻辑分析来确保程序的安全性和正确性。FV的一个关键方面是符号执行，它为输入分配符号值，从而在一次分析中探索各种程序路径。

该技术有助于验证程序是否可以违反某些条件或到达危险状态，使用如SMT求解器等工具进行可行性评估。因此，符号执行增强了测试，提供了更全面的方式来确立程序的安全性和正确性。

正式验证的好处

与传统执行方法相比，符号执行使用输入的符号值，从而能够在一次分析中检查所有可能的执行路径。

这种方法旨在概括测试，常用于验证任何程序执行是否可以违反特定属性。

符号执行可以证明某些状态的不可达性，从而以更全面的方式确认程序的安全性或正确性。

状态空间的全面分析： 正式验证涉及计算和分析合约在执行期间可能存在的所有状态。这种细致的检查有助于识别传统测试方法中可能不明显的潜在缺陷或漏洞。

总之，正式验证适合于确保在更概念化和绝对的层面上的正确性和安全性，而模糊测试则更适合于发现智能合约中的特定错误和测试不变性。

2. 我们使用的正式验证工具

工具和技术

• Halmos: 一种开源工具，允许开发人员在以太坊智能合约字节码的验证中重用单元测试属性的正式规范。
• Ityfuzz: ItyFuzz是一种混合模糊测试工具，结合了符号执行和模糊测试，以查找智能合约中的错误。从技术上讲，它使用正式验证（合成执行），并辅以利用数据流模式和比较引导的模糊测试算法。 它可以在Echidna和Scribble之上运行。
• Kontrol: 提供EVM的正式表示，并促进智能合约字节码的符号执行，结合了KEVM和Foundry。
• Pyrometer: 结合了符号执行、抽象解释和静态分析，专注于Solidity，但有可能具备语言无关性。
• hevm: 一种EVM实现，支持智能合约的符号执行、单元测试和调试。
• Heimdall: 一种高级的智能合约字节码分析工具，专注于反汇编、控制流图生成和反编译。

最常用的工具

• Halmos
• Ityfuzz
• Ityfuzz与Echidna
• Kontrol

  3. 这些工具的工作原理

Halmos

• 使用该工具的一个示例是通过符号值执行模糊测试和不变性测试，从而在测试中进行更深入的分析。
• 不变性测试的实现类似但不同；例如，可以创建特定函数使用符号字节码执行不变性。

这是一个小示例：

    function check_Invariant_Backdoor(bytes4 selector,address other, address caller) public {
        // 执行任意交易
        vm.assume(other != caller);

        uint256 oldBalanceOther = IERCOLAS(token).balanceOf(other);
        uint256 oldAllowance = IERCOLAS(token).allowance(other, caller);

        vm.prank(caller);
        (bool success,) = address(token).call(gen_calldata(selector));
        vm.assume(success);

        uint256 newBalanceOther = IERCOLAS(token).balanceOf(other);

        if (newBalanceOther < oldBalanceOther) {
            assert(oldAllowance >= oldBalanceOther - newBalanceOther);
        }

    }

/////////////////////////////////////////////////////////////////////////

// 处理程序

/////////////////////////////////////////////////////////////////////////

    function gen_calldata(bytes4 selector) internal returns (bytes memory) {

        // 创建要包含在调用数据中的符号值
        address guy = svm.createAddress("guy");
        address src = svm.createAddress("src");
        address dst = svm.createAddress("dst");
        uint256 wad = svm.createUint256("wad");
        uint256 val = svm.createUint256("val");
        uint256 pay = svm.createUint256("pay");

        // 基于函数选择器生成调用数据
        bytes memory args;
        if (selector == IERCOLAS(token).changeOwner.selector) {
            args = abi.encode(guy);
        } else if (selector == IERCOLAS(token).changeMinter.selector) {
            args = abi.encode(guy);
        } else if (selector == IERCOLAS(token).mint.selector) {
            args = abi.encode(guy, wad);
        } else if (selector == IERCOLAS(token).inflationControl.selector) {
            args = abi.encode(wad);
        } else if (selector == IERCOLAS(token).inflationRemainder.selector) {
            args = abi.encode();
        } else if (selector == IERCOLAS(token).burn.selector) {
            args = abi.encode(val);
        } else if (selector == IERCOLAS(token).decreaseAllowance.selector) {
            args = abi.encode(src, wad);
        } else if (selector == IERCOLAS(token).increaseAllowance.selector) {
            args = abi.encode(src, wad);
        } else {

            args = svm.createBytes(1024, "data"); 
        }
        return abi.encodePacked(selector, args);
    }

另一个示例

    function checkNoBackdoor(bytes4 selector, address caller, address other) public virtual {
        // address caller = svm.createAddress("caller");
        // address other = svm.createAddress("other");
        bytes memory args = svm.createBytes(1024, 'data');
        vm.assume(other != caller);

        uint256 oldBalanceOther = (token).balanceOf(other);

        uint256 oldAllowance = (token).allowance(other, caller);

        vm.prank(caller);
        (bool success,) = address(token).call(abi.encodePacked(selector, args));
        vm.assume(success);

        uint256 newBalanceOther = (token).balanceOf(other);

        if (newBalanceOther < oldBalanceOther) {
            assert(oldAllowance >= oldBalanceOther - newBalanceOther);
        }
    }

===

        function _check_transferFrom(address caller, address from, address to, address other, uint256 amount) public virtual {
        require(other != from);
        require(other != to);

        uint256 oldBalanceFrom   = IERCOLAS(token).balanceOf(from);
        uint256 oldBalanceTo     = IERCOLAS(token).balanceOf(to);
        uint256 oldBalanceOther = IERCOLAS(token).balanceOf(other);

        uint256 oldAllowance = IERCOLAS(token).allowance(from, caller);

        vm.prank(caller);
        IERCOLAS(token).transferFrom(from, to, amount);

        if (from != to) {
            assert(IERCOLAS(token).balanceOf(from) <= oldBalanceFrom);
            assert(IERCOLAS(token).balanceOf(from) == oldBalanceFrom - amount);
            assert(IERCOLAS(token).balanceOf(to) >= oldBalanceTo);
            assert(IERCOLAS(token).balanceOf(to) == oldBalanceTo + amount);

            assert(oldAllowance >= amount); // 确保允许足够
            assert(oldAllowance == type(uint256).max || IERCOLAS(token).allowance(from, caller) == oldAllowance - amount); // 如果不为最大值，允许减少
        } else {
            assert(IERCOLAS(token).balanceOf(from) == oldBalanceFrom);
            assert(IERCOLAS(token).balanceOf(to) == oldBalanceTo);
        }
        assert(IERCOLAS(token).balanceOf(other) == oldBalanceOther);
    }

Ityfuzz:

• 作为一种新工具，文档有限，但它开始展示所有能力，因为它结合了采用数据流模式和比较引导的模糊测试算法的正式验证（合成执行）。
• 要使用该工具，我们需要安装Blazo。

使用示例：

• 在这些示例合约中： 我们展示了ityfuzz的一项功能，涉及使用bug()关键字。该函数旨在识别包含的代码内潜在的不变性违反情况。
• 战略性放置： 在这些情况下，我们已将其战略性地放置在合约内部。这消除了编写单独测试的需要，使我们能够发现潜在问题。
• 多个Oracle： 目前，ityfuzz配备了各种旨在检测代码中漏洞的Oracle。
• 结果报告： 结果指示ityfuzz是否发现任何问题，并提供了它跟随的潜在利用步骤。

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

import "lib/solidity_utils/lib.sol";

contract Gate {
    bool public locked = true;
    uint256 public timestamp = block.timestamp;
    uint8 private number1 = 10;
    uint16 private number2 = 255;
    bytes32[3] private data;

    constructor(bytes32 _data1, bytes32 _data2, bytes32 _data3) {
        data[0] = _data1;
        data[1] = _data2;
        data[2] = _data3;
    }

    modifier onlyThis() {
        require(msg.sender == address(this), "只有合约可以调用此");
        _;
    }

    function resolve(bytes memory _data) public {
        require(msg.sender == tx.origin);
        (bool success, ) = address(this).call(_data);
        require(success, "调用失败");
    }

    function unlock(bytes memory _data) public onlyThis {
        require(bytes16(_data) == bytes16(data[2]));
        // locked = false;
        bug();
    }

    // function isSolved() public view returns (bool) {
    //     return !locked;
    // }
}

结果：

或这个例子：

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.11;

import "lib/solidity_utils/lib.sol";

contract BytecodeVault {
    // address public owner;

    // constructor() public payable { 
    //     owner = msg.sender;        
    // }       

    modifier onlyBytecode() {
        require(msg.sender != tx.origin, "不允许使用高级合约！");
        _;
    }

    function withdraw(bytes memory senderCode) external onlyBytecode {
        uint256 sequence = 0xdeadbeef;

        // bytes memory senderCode;
        // address bytecaller = msg.sender;

        // assembly {
        //     let size := extcodesize(bytecaller)
        //     senderCode := mload(0x40)
        //     mstore(0x40, add(senderCode, and(add(size, 0x20), 0x1f), not(0x1f)))
        //     mstore(senderCode, size)
        //     extcodecopy(bytecaller, add(senderCode, 0x20), 0, size)
        // }

        require(senderCode.length % 2 == 1, "字节码长度必须是奇数！");

        for (uint256 i = 0; i < senderCode.length - 3; i++) {
            if (senderCode[i] == bytes1(uint8(sequence >> 24))) {
                if (senderCode[i + 1] == bytes1(uint8((sequence >> 16) & 0xFF))) {
                    if (senderCode[i + 2] == bytes1(uint8((sequence >> 8) & 0xFF))) {
                        if (senderCode[i + 3] == bytes1(uint8(sequence & 0xFF))) {
                            bug();
                        }
                    }
                }
            }
        }
        // revert("未找到序列！");
    }

    function isSolved() public view returns (bool) {
        return address(this).balance == 0;
    }

}

结果：

Kontrol:

• Kontrol是一个强大的工具，它基于KEVM构建，并具有非常实用的功能，比如：

  • Kontrol KCFG可视化工具。该工具允许你在符号执行的不同节点分析虚拟机的状态。

实现示例：

// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.13;

import "forge-std/Test.sol";
import "../src/token.sol";

contract TokenTest is Test {
    Token token; 

    address Alice;
    address Bob;
    address Eve;

    function setUp() public {
        token = new Token();
        Alice = makeAddr("Alice");
        Bob = makeAddr("Bob");
        Eve = makeAddr("Eve");
        token.mint(Alice, 10 ether);
        token.mint(Bob, 20 ether);
        token.mint(Eve, 30 ether);
    }

    function testTransfer(address from, address to, uint256 amount) public {
        // 这个证明在使用kontrol执行时有很多分支，
        // 因为`from`和 `to`参数可以是以下每个地址中的一个
        // (Alice, Bob, Eve, address(this), address(vm), address(token))。

        // 前四个`vm.assume`调用允许符号参数`from`和`to`接受
        // 在token存储中初始化并具有有效余额的值。

        // 这是一个玩具示例，展示了分支和约束如何工作。

        vm.assume(from == Alice || from == Bob || from == Eve);
        vm.assume(to == Alice || to == Bob || to == Eve);
        vm.assume(from != address(this) && from != address(vm) && from != address(token));
        vm.assume(to != address(this) && to != address(vm) && to != address(token));
        vm.assume(to != from);

        vm.assume(token.balanceOf(from) >= amount);

        uint256 preBalanceFrom = token.balanceOf(from);
        uint256 preBalanceTo = token.balanceOf(to);

        vm.prank(from);
        token.transfer(to, amount);

        if(from == to) {
            assertEq(token.balanceOf(from), preBalanceFrom);
            assertEq(token.balanceOf(to), preBalanceTo);
        } else {
            assertEq(token.balanceOf(from), preBalanceFrom - amount);
            assertEq(token.balanceOf(to), preBalanceTo + amount);
        }
    }
}

4. 我们的方法和方法论

与客户工作流程的集成

这些是我们在其他项目中使用这些工具的示例，曾使用Halmos、Foundry、Echidna、Medusa、Ityfuzz进行分析......

在这里我们详细展示了我们为执行测试所做的工作：

• https://github.com/scab24/Autonolas
• https://allthingsfuzzy.substack.com/p/formal-verification-in-practice-halmos
• https://github.com/scab24/Formal_Verification

5. 客户前提

必要的信息

为了进行有效的验证，我们需要：

• 系统文档和需求规范。
• 对源代码或相关部分的访问。

6. 成本和定价模式

定价结构

我们提供灵活的定价结构，具体取决于项目的复杂性和规模。费用预计根据：

• 代码复杂性。
• 所需分析的长度和深度。

7. 结论和行动呼吁

为什么选择我们？

联系

如需与我们联系，你可以给我们写信：

• Twitter: bloqarl
• Twitter: secoalba
• Telegram

• 原文链接： github.com/ZealynxSecuri...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～