Khi kỷ nguyên chuỗi khối 2.0 tập trung vào hợp đồng thông minh (Hợp đồng thông minh) và ứng dụng chuỗi khối (DApps) dần trở thành xu hướng, tính bảo mật của hợp đồng thông minh và ứng dụng chuỗi khối ngày càng trở thành tâm điểm chú ý trong ngành.

Đặc biệt, sau khi trải qua các sự cố như THE DAO và vụ đánh cắp Binance, làm thế nào để xác minh và đảm bảo tính bảo mật của các hợp đồng thông minh và ứng dụng blockchain đã trở thành một điểm nhức nhối cấp bách trong ngành công nghiệp blockchain hiện tại.

Tác giả đã thống kê đơn giản, từ tháng 9 năm 2017 đến tháng 9 năm 2018, các lỗ hổng liên quan đến hợp đồng thông minh và ứng dụng chuỗi khối cho thấy mô hình bùng phát thường xuyên và hậu quả rất sâu rộng. Nó không chỉ trực tiếp gây ra một lượng tiền thất thoát khổng lồ mà từ góc độ phát triển lâu dài, nó còn ảnh hưởng đến sự phát triển bền vững của công nghệ blockchain mới nổi trong tương lai.

Ngoài ra, mặc dù các lỗ hổng tiềm ẩn của các hợp đồng thông minh và ứng dụng blockchain hiện tại vẫn chưa được giải quyết triệt để, nhưng hiện trạng là số lượng hợp đồng thông minh và ứng dụng blockchain vẫn đang tăng nhanh với tốc độ tăng trưởng trung bình hàng chục nghìn mỗi ngày.

Không khó để thấy rằng tốc độ tăng trưởng và tính bảo mật của hợp đồng thông minh và ứng dụng chuỗi khối đang cùng tồn tại trong một mối quan hệ không lành mạnh. Nếu chúng ta so sánh cung và cầu (tốc độ tăng trưởng là "cung"; bảo mật là "cầu"), tình trạng chung hiện tại của các hợp đồng thông minh và ứng dụng blockchain là trạng thái "cung vượt cầu".

Dựa trên điều này, làm thế nào để đảm bảo tính bảo mật của các hợp đồng thông minh lớn và ứng dụng chuỗi khối đã trở thành vấn đề cốt lõi đối với các doanh nghiệp và cá nhân hướng tới tương lai trong ngành công nghiệp chuỗi khối. Trên thực tế, hiện tại có các phương pháp đặc biệt trong ngành để khắc phục điểm khó khăn này, chẳng hạn như khớp mã tính năng, kiểm tra tự động dựa trên thực thi ký hiệu và trừu tượng hóa ký hiệu cũng như kiểm tra tự động dựa trên xác minh chính thức. Trong số đó, sau khi khám phá và thực hành rộng rãi trong ngành, "kiểm toán tự động dựa trên xác minh chính thức" đã trở thành một phương pháp tương đối trưởng thành và chủ đạo trong ngành.

Do đó, tác giả đặc biệt tập trung vào "xác minh chính thức", chọn hai công cụ xác minh chính thức chính (VaaS & Mythril) trong ngành hiện tại và tiến hành so sánh thử nghiệm đơn giản. Đặc biệt, phiên bản mà công cụ Mythril dùng để thử nghiệm là "0.21.12".

tiêu đề phụ

Giới thiệu về Công cụ VaaS & Mythril

01. Giới thiệu về công cụ VaaS

interface TEST {

    function test123() external view returns (uint256);

    function getBlocknumber() external view returns (uint256);

}

contract test2 {

    function testCalling(address _testAdddress) public {

        TEST t = TEST(_testAdddress);

t.test123();//mythril dương tính giả

    }

    function testFormal(address _testAdddress) public view returns(uint256 time){

        TEST t = TEST(_testAdddress);

t.getBlocknumber();//mythril dương tính giả

        return time;

    }

}

contract Reentrancy {

    mapping(address => uint256) public balances;

    event WithdrawFunds(address _to,uint256 _value);

    function depositFunds() public payable {

        balances[msg.sender] += msg.value;

    }

    function showbalance() public view returns (uint256 ){

        return address(this).balance;

    }

    function withdrawFunds (uint256 _weiToWithdraw) public {

        require(balances[msg.sender] >= _weiToWithdraw);

        require(msg.sender.call.value(_weiToWithdraw)());

balances[msg.sender] -= _weiToWithdraw;//mythril rõ ràng là dương tính giả

        emit WithdrawFunds(msg.sender,_weiToWithdraw);

    }

}

contract TxUserWallet {

    address owner;

    constructor() public {

        owner = msg.sender;

    }

    function transferTo(address  dest, uint amount) public {

        require(tx.origin == owner);

        dest.transfer(amount);

    }

}

contract Delegatecall{

    uint public q;

    bool public b;

    address addr = 0xde6a66562c299052b1cfd24abc1dc639d429e1d6;

    function Delegatecall() public payable {

    }

    function call1() public returns(bool) {

b = addr.delegatecall

(bytes4(keccak256("fun(uint256,uint256)")),2,3);

        return b;

    }

    function call2(address add) public returns(bool){

b=add.delegatecall

(bytes4(keccak256("fun(uint256,uint256)")),2,3);

        return b;

    }

}

function createTokens() payable external {

      if (isFinalized) throw;

if (block.number < fundingStartBlock) throw;

if (block.number > fundingEndBlock) throw;

      if (msg.value == 0) throw;

      uint256 tokens = safeMult(msg.value, tokenExchangeRate);  

      uint256 checkedSupply = safeAdd(totalSupply, tokens);

      if (tokenCreationCap < checkedSupply) throw;  

      totalSupply = checkedSupply;

      balances[msg.sender] += tokens;  

      CreateBAT(msg.sender, tokens);  

    }

function finalize() external {

      if (isFinalized) throw;

      if (msg.sender != ethFundDeposit) throw;

      if(totalSupply < tokenCreationMin) throw;      

      if(block.number <= fundingEndBlock && totalSupply != tokenCreationCap) throw;

      // move to operational

      isFinalized = true;

      if(!ethFundDeposit.send(this.balance)) throw;  

    }

function refund() external {

      if(isFinalized) throw;                       

if (block.number <= fundingEndBlock) throw;

      if(totalSupply >= tokenCreationMin) throw;  

      if(msg.sender == batFundDeposit) throw;    

      uint256 batVal = balances[msg.sender];

      if (batVal == 0) throw;

      balances[msg.sender] = 0;

      totalSupply = safeSubtract(totalSupply, batVal);

      uint256 ethVal = batVal / tokenExchangeRate;     

      LogRefund(msg.sender, ethVal);               

      if (!msg.sender.send(ethVal)) throw;       

    }

}

contract Auction {

    address public highestBidder = 0x0;

    uint256 public highestBid;

    function Auction(uint256 _highestBid) {

        require(_highestBid > 0);

        highestBid = _highestBid;

        highestBidder = msg.sender;

    }

    function bid() payable {

        require(msg.value > highestBid);

        highestBidder.transfer(highestBid);

highestBidder = msg.sender;

highestBid = msg.value;

    }

    function auction_end() {

    }

}

if (lastTimeOfNewCredit + TWELVE_HOURS < block.timestamp) {

msg.sender.send(amount);

    creditorAddresses[creditorAddresses.length - 1].send(profitFromCrash);

    corruptElite.send(this.balance);

    ...

    return true;

}

else {

msg.sender.send(amount);

return false;

}

function distributeBTR(address[] addresses) onlyOwner {

    for (uint i = 0; i < addresses.length; i++) {

        balances[owner] -= 2000 * 10**8;

        alances[addresses[i]] += 2000 * 10**8;

        Transfer(owner, addresses[i], 2000 * 10**8);

}

    }

contract A {

    uint c;

    function add(uint8 a,uint8 b){

uint8 sum = a+b;

        c=sum;

    }

}

...

contract ERC20 is ERC20Basic {

  function allowance(address owner, address spender) constant returns (uint);

function transferFrom(address from, address to, uint value);

  function approve(address spender, uint value);

  event Approval(address indexed owner, address indexed spender, uint value);

}

...

 function transfer(address _to, uint _value) onlyPayloadSize(2 * 32) {

    balances[msg.sender] = balances[msg.sender].sub(_value);

    balances[_to] = balances[_to].add(_value);

    Transfer(msg.sender, _to, _value);

  }

contract A {

    B b;

    uint c;

    function test(uint a){

        b = new B(a);

        c = b.get(200);

    }

}

contract B {

    uint b;

    function B(uint e){

        b=100;

    }

    function get(uint a)returns(uint){

        require(a<100);

        return a;

  }

}

Thông qua phân tích so sánh đơn giản ở trên về logic, kích thước và dữ liệu của công cụ VaaS và công cụ Mythril, tác giả tin rằng người đọc sẽ có thể đưa ra những nhận định và đánh giá tương ứng dựa trên định hướng và trọng tâm kinh doanh của bản thân sau khi đọc.

Bất kể hợp đồng thông minh và ứng dụng chuỗi khối hay thậm chí là tính bảo mật của toàn bộ ngành công nghiệp chuỗi khối, trong tương lai, chúng tôi sẽ cần phát triển theo mô hình cân bằng mối quan hệ giữa cung (tốc độ tăng trưởng) và nhu cầu (bảo mật) và chúng tôi cần nhiều hơn nữa Biết rõ đâu là điểm đau của hiện trạng, và làm thế nào để cải thiện và đổi mới để đối phó với điểm đau.

Dù là người ủng hộ công nghệ tiên tiến hay người đam mê công nghệ chuỗi khối, bất kỳ ai có cái nhìn sâu sắc, có tư duy phi tập trung và nhận ra rằng các hợp đồng thông minh và ứng dụng chuỗi khối sẽ có ảnh hưởng sâu rộng trong tương lai đều có thể hiểu được mục đích của tác giả đối với "hình thức" hóa học. xác minh" là mục đích của báo cáo thử nghiệm này.

Đúng là mặc dù hiện đang chú ý nhiều hơn đến cách thúc đẩy triển khai các hợp đồng thông minh và ứng dụng chuỗi khối cũng như việc xây dựng tổng thể hệ sinh thái chuỗi khối, nhưng vẫn còn nhiều lỗ hổng và rủi ro trong kiến ​​trúc kỹ thuật cơ bản chưa được giải quyết , nó sẽ là quá tham vọng.

Do đó, tác giả gợi ý rằng để đảm bảo tính bảo mật của các hợp đồng thông minh lớn và ứng dụng chuỗi khối, cũng như duy trì hoạt động tốt và duy trì hệ sinh thái chuỗi khối, "xác minh chính thức" đã trở thành một cách quan trọng để kiểm toán tự động.

Đây là giai đoạn cần thiết để phát triển các hợp đồng thông minh và ứng dụng chuỗi khối hiện tại để đánh giá tính khả thi của một công cụ kiểm toán và xác minh nhất định thông qua các khía cạnh đánh giá như tỷ lệ âm tính giả, tỷ lệ dương tính giả, tỷ lệ trúng và giới hạn thời gian thử nghiệm. nghiêm túc thực hiện sứ mệnh.