リスク警告:「仮想通貨」「ブロックチェーン」の名のもとでの違法な資金調達のリスクに注意してください。—銀行保険監督管理委員会など5部門
検索
ログイン
简中
繁中
English
日本語
한국어
ภาษาไทย
Tiếng Việt
BTC
ETH
HTX
SOL
BNB
View Market
2つのツール(VaaSとMythril)の正式検証の比較レポート
成都链安
特邀专栏作者
2019-10-14 07:51
この記事は約7581文字で、全文を読むには約11分かかります
著者は特に「形式検証」に焦点を当て、現在の業界で主要な形式検証ツールの2つ(VaaSとMythril)を選択し、簡単なテスト比較を行っています。

スマート コントラクト (スマート コントラクト) とブロックチェーン アプリケーション (DApp) を中心としたブロックチェーン 2.0 時代が徐々に主流になり、スマート コントラクトとブロックチェーン アプリケーションのセキュリティが業界でますます注目を集めるようになりました。

特に、THE DAOやBinanceの盗難などの事件を経験した後、スマートコントラクトとブロックチェーンアプリケーションのセキュリティをどのように検証し保証するかが、現在のブロックチェーン業界における緊急の課題となっています。

著者が簡単な統計を作成したところ、2017 年 9 月から 2018 年 9 月にかけて、スマート コントラクトとブロックチェーン アプリケーションに関連する脆弱性が頻繁に発生するパターンが見られ、その影響は広範囲に及んでいました。それは直接的に巨額の損失を引き起こしただけでなく、長期的な発展の観点から、将来のブロックチェーンという新興技術の持続可能な発展にも影響を及ぼしました。

また、現在のスマートコントラクトやブロックチェーンアプリケーションの潜在的な脆弱性は適切に解決されていないにもかかわらず、スマートコントラクトやブロックチェーンアプリケーションの数は依然として毎日平均数万件のペースで急速に増加しているのが現状です。

スマートコントラクトとブロックチェーンアプリケーションの成長率とセキュリティが不健全な関係で共存していることは、難しくありません。需要と供給(成長率は「供給」、セキュリティは「需要」)で例えると、現在のスマートコントラクトとブロックチェーンアプリケーションの一般的な状況は「供給が需要を上回っている」状態です。

これに基づいて、大規模なスマート コントラクトとブロックチェーン アプリケーションのセキュリティをどのように確保するかが、ブロックチェーン業界の先進的な企業や個人にとって中心的な問題となっています。実際、業界では現在、機能コードの照合、シンボリック実行とシンボリック抽象化に基づく自動監査、形式検証に基づく自動監査など、この問題点を克服するための特別な方法が存在します。その中でも、業界での広範な探求と実践を経て、「正式な検証に基づく自動監査」は業界で比較的成熟した主流の手法になりました。

そこで、著者は特に「形式検証」に焦点を当て、現在の業界で主要な形式検証ツールの2つ(VaaSとMythril)を選択し、簡単なテスト比較を実施します。特に、テストに使用したMythrilツールのバージョンは「0.21.12」です。

副題

VaaS と Mythril ツールの紹介

01. VaaSツールの紹介

VaaS ツールは、Beosin Chengdu Lianan が独自の知的財産権を使用して独自に開発した自動形式検証ツールで、スマート コントラクトとブロックチェーン アプリケーションに「軍事レベル」の形式検証サービスを提供し、危険なコードを正確に特定できます。リスクの原因が指摘され、従来のセキュリティの抜け穴、スマート コントラクトのセキュリティ属性、機能の正確性が 95% 以上の精度で効果的に検出されます。

02. ミスリルツールの紹介

副題

テストケースの構成

コントラクト テスト ケースは、260 のトークン コントラクトと 20 のビジネス コントラクトで構成されます。

  • トークン契約には、トップ 200 トークン契約と監査用の 60 の典型的なトークン契約が含まれており、ICO、ロックアップ、ミント、バーンなどの機能をカバーしています。

  • 副題

試験結果の概要

VaaS ツールは、トークンとビジネス クラスのすべてのコントラクト テスト ケースを検出できますが、Mythril ツールはトークン コントラクトのみを検出でき、ビジネス コントラクトは検出できません。したがって、このテスト結果の概要は、トークン コントラクトのリストの比較分析にすぎないことに注意してください。

VaaS ツールには合計 28 個の脆弱性チェックがありますが、Mythril ツールには VaaS ツールと比較して 9 個の脆弱性チェックしかありません。そのため、VaaSツールの検出項目はMythrilツールに比べてはるかに多くなります。具体的な検出項目は次のように比較されます。

VaaSとミスリルの検出項目の比較

01. 同一検査項目の検査結果

選択した 260 のトークン テスト ケースについて、Mythril ツールは 15 分以内に 184 のコントラクト結果を実行できますが、76 には検出結果がありませんでしたが、VaaS ツールはすべての結果を実行できます。 Mythril ツールと VaaS ツールの両方で実行できる 184 件の結果を比較すると、結果は次のようになります。

  • ヒット率と誤検知率

検出結果を比較すると、同じ検出項目で比較した場合、VaaS ツールの検出能力は Mythril ツールの検出能力よりもはるかに高いことがわかります。計算によると、VaaS ツールの検出精度は 96.9%、Mythril ツールの検出精度は 36.6%、VaaS ツールの誤検知率は 15.3%、Mythril ツールの誤検知率は 48.5% となります。詳細については、以下の図を参照してください。

なお、ヒット率と誤報率の計算式は以下のとおりです。

  • ヒット率 = ヒット数 / 総質問数

  • 誤検知率 = 誤検知の数/(誤検知の数 + ヒット数)

著者の統計によると、VaaS ツールと Mythril ツールの両方で実行された検出項目は合計 655 の質問でした。

  • VaaS ツールは合計 635 件の問題を検出し、ヒット率は 96.9%、誤検知は合計 115 件、誤検知率は 15.3% でした。

  • Mythril ツールは合計 240 件の問題を検出し、ヒット率は 36.6% でした。合計 226 件の誤検知、誤検知率は 48.5% でした。中でも、Mythril ツールの再入攻撃とサービス妨害の誤報率は比較的高く、全体の 93.3% を占めています。

検出の合計値を次の表で比較します。

  • テストの制限時間

Mythril ツールの平均テスト時間は 226.2 秒ですが、VaaS ツールの平均テスト時間は 164.4 秒です。 VaaS ツールの動作効率が Mythril ツールよりも優れていることがわかります。

02. VaaSツールの特定検出項目の検出結果

詳細については、以下の表を参照してください。

副題

事例紹介

01. 同一検出項目の場合

  • 再入学

場合:

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();//ミスリルの誤検知

 

    }

 

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

        TEST t = TEST(_testAdddress);

t.getBlocknumber();//ミスリルの誤検知

        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;//ミスリルの明らかな誤検知

        emit WithdrawFunds(msg.sender,_weiToWithdraw);

    }

}



  • VaaS ツールのテスト結果:


  • ミスリルツールのテスト結果:


▷ 著者の分析によれば、VaaSツールはリエントランシー攻撃の発生場所を報告し、Mythrilツールは外部呼び出しに対するアラームを発し、アラームは合計4件あり、そのうち2件は通常の外部呼び出しで、もう1件は異常であった。明らかな誤報であり、誤検知率が高くなります。

  • TXOriginAuthentication (tx.origin 使用エラー)

場合:

contract TxUserWallet {

    address owner;

 

    constructor() public {

        owner = msg.sender;

    }

 

    function transferTo(address  dest, uint amount) public {

        require(tx.origin == owner);

        dest.transfer(amount);

    }

}



  • VaaS ツールのテスト結果:


  • ミスリルツールのテスト結果:


▷ 著者の分析によると、VaaS ツールと Mythril ツールの両方が tx.origin キーワードを検出して警告することができます。


  • 低レベル呼び出しの呼び出し (呼び出し呼び出し、デリゲート呼び出し呼び出し、自殺関数呼び出し)

場合:

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;

    }

}



  • VaaS ツールのテスト結果:


  • ミスリルツールのテスト結果:


▷ 著者の分析によると、この事件ではデリゲタコールが2回あったのに対し、Mythrilツールは1回しか報告しなかったため、過少報告の危険性がある。


  • BlockMembers の操作 (ブロック パラメーターの依存関係)

  • 場合:

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;       

    }

}



  • VaaS ツールのテスト結果:


  • ミスリルツールのテスト結果:


▷ 著者の分析によれば、VaaSツールとMythrilツールはどちらもブロックパラメータの依存関係を検出できるが、Mythrilツールには誤検知のリスクがある。


  • サービス拒否

  • 場合:

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() {

    }

}



  • VaaS ツールのテスト結果:


  • ミスリルツールのテスト結果:


▷ 著者の分析によれば、VaaSツールとMythrilツールはどちらもサービス妨害のリスク検出を実行できる。ただし、この場合、highestBidder がコントラクトを悪意を持って攻撃し、その結果、転送が継続的に失敗し、コントラクトがサービスの受け入れを拒否した可能性があります。この場合、VaaS ツールはサービス拒否のリスクを検出できます。しかし、Mythril ツールはそれを検出しませんでした。


  • Call Or Send Return Valuesのチェックを外す(呼び出しおよび送信戻り値検出)

  • 場合:

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;

}



  • VaaS ツールのテスト結果:


  • ミスリルツールのテスト結果:


▷ 著者の分析によると、VaaSツールとMythrilツールはどちらも未チェックのコール呼び出しの戻り値を検出できるが、Mythrilツールには誤検知のリスクがある。


  • 整数オーバーフロー

  • ケース 1:

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);

}

    }



▷ 著者の分析によれば、上記の場合、balances[owner]の値がチェックされていないため、アンダーフローが発生する可能性があるが、Mythrillツールはエラーを報告しないため、Mythrillツールは定常動作をチェックしないことになる。


ケース 2:

contract A {

    uint c;

    function add(uint8 a,uint8 b){

uint8 sum = a+b;

        c=sum;

    }

}



  • VaaS ツールのテスト結果:


  • ミスリルツールのテスト結果:


▷ 著者の分析によると、Mythrill ツールの非 uint256 データ型のオーバーフロー検出は正確ではありません。


ケース 3:


  • Mythril ツールの検出結果の一部:


▷ 著者の分析によると、Mythrill ツールは一部の特定の変数を処理せず、誤検知が発生しました。配列、msg.value、now など。



02. VaaSツールの具体的な検知項目の事例


ケース 1:

...

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);

  }



  • 試験結果:


ケース 2:

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;

  }

}



  • 試験結果:


▷ 著者の分析によれば、ケース2のコントラクト間の呼び出しに関しては、ソースコードがあればVaaSツールは正常に呼び出してテストできるが、Mythrilツールはそれができない。これが、Mythril ツールがビジネス契約の検証を実行できない理由の 1 つです。

上記の VaaS ツールと Mythril ツールのロジック、ディメンション、データの簡単な比較分析を通じて、読者は読んだ後に自身のビジネスの方向性と焦点に基づいて、対応する判断と評価を行うことができると信じています。

スマートコントラクトやブロックチェーンアプリケーション、さらにはブロックチェーン業界全体のセキュリティに関わらず、将来的には供給(成長率)と需要(セキュリティ)の関係のバランスをとったモデルで開発する必要があり、さらに多くのことが必要になります。現状の問題点がどこにあるのか、その問題点に対応して改善および革新する方法を明確に把握します。

最先端のテクノロジーの支持者であっても、ブロックチェーンテクノロジーのオタクであっても、分散型思考を持ち、スマートコントラクトとブロックチェーンアプリケーションが将来的に広範囲に影響を与えることを認識している洞察力のある人であれば、化学物質を「形成」するという著者の目的を理解できるでしょう。検証」がこのテストレポートの目的です。

確かに現在、スマートコントラクトやブロックチェーンアプリケーションの実装、ブロックチェーンエコシステム全体の構築をどのように促進するかにさらなる注目が集まっているものの、基盤となる技術アーキテクチャにまだ解決されていないさまざまな抜け穴やリスクがあるのは事実です。 、それは野心的すぎるでしょう。

したがって、大規模なスマートコントラクトとブロックチェーンアプリケーションのセキュリティを確保し、ブロックチェーンエコロジーの良好な運用と維持を維持するために、「形式的検証」が自動監査の重要な方法になっていると著者は示唆しています。

偽陰性率、偽陽性率、ヒット率、テスト時間制限などの評価次元を通じて、特定の検証および監査ツールの実現可能性を判断することは、現在のスマート コントラクトやブロックチェーン アプリケーションの開発に必要な段階です。使命を真摯に遂行すること。

智能合约
Odaily公式コミュニティへの参加を歓迎します
購読グループ
https://t.me/Odaily_News
チャットグループ
https://t.me/Odaily_CryptoPunk
公式アカウント
https://twitter.com/OdailyChina
チャットグループ
https://t.me/Odaily_CryptoPunk
AI要約
トップに戻る
著者は特に「形式検証」に焦点を当て、現在の業界で主要な形式検証ツールの2つ(VaaSとMythril)を選択し、簡単なテスト比較を行っています。
著者ライブラリ
成都链安
Odailyプラネットデイリーアプリをダウンロード
一部の人々にまずWeb3.0を理解させよう
IOS
Android