入力空間とイベント空間を探索するJavaScriptコードの等価性検証

情報処理学会

書誌事項

タイトル別名
  • WIP: Towards Equivalence Verification of JavaScript Code

この論文をさがす

抄録

コードの等価性検証の技術は，書き換え前後のコードが同様に動作するか，同じインタフェースの異なる実装がまったく同じ動作をするか等を確認する場面において，非常に有用なものである．コードの等価性検証を行うツールには，C言語の2つの関数の等価性の検証を行うツールUC-KLEEが存在する．UC-KLEEは遅延初期化に基づく記号実行により，動的データ構造操作も含めた正確な検査が可能である．しかし，UC-KLEEではイベント処理の順序に起因するイベント空間を考慮していない．そのため，C言語とは異なりイベントの発火順序が実行結果に大きく影響するJavaScriptコードの等価性検証においては，UC-KLEEの単純拡張は不十分である．そこで，本発表では入力空間とイベント空間の両方の探索を行う，JavaScriptにおける関数の等価性検証ツールのプロトタイプ実装を提案する．入力空間の探索はコンコリック実行によりできるだけ多くの実行パスを通すことで，イベント空間の探索はイベントの発火順序をランダムに操作することで行う．入力空間に加えてイベント空間も操作することで，ある特定の順序でイベントが発火したときにのみ通るパスの探索も可能となる．加えて，入力空間に加えてイベント空間を考慮する提案手法の等価性検査の有効性を定量的に示すことを目的とした評価実験を行った．これは，入力空間しか考慮しない従来のUC-KLEEの単純拡張を比較対象とし，いくつかの小規模テストケースを用いて入力空間とイベント空間の双方を考慮する提案手法の等価性検査の精度，効率を計測することにより行う．

The technique of equivalence verification of code is very useful in a situation where it is confirmed whether codes before and after reworking operate similarly, whether different implementations of the same interface perform exactly the same operation, and the like. UC-KLEE is a tool which verifies the equivalence of two functions in C language. UC-KLEE can perform accurate inspection including dynamic data structure operation by symbolic execution based on lazy initialization. However, UC-KLEE does not consider the event space due to the order of event processing. Therefore, unlike in C language, the simplicity extension of UC-KLEE is insufficient in equivalence verification of JavaScript code in which order of event occurrence greatly affects execution result. Therefore, in this presentation we propose a prototype implementation of a function equivalence verification tool in JavaScript which explore both input space and event space. Exploring the input space is performed by passing as many execution paths as possible through a concolic execution, and exploring the event space is performed by randomly manipulating the event firing sequence. By manipulating the event space in addition to the input space, it is also possible to search for a path that passes only when the event occurs in a specific order. In addition, we conducted an evaluation experiment aiming to quantitatively show the effectiveness of the equivalence check of the proposed method considering the event space in addition to the input space. To do this, we measure the accuracy and efficiency of the equivalence check of the proposed method considering both the input space and the event space by using several small scale test cases and compare simple extension of UC-KLEE, which only considers input space.

収録刊行物

キーワード

詳細情報 詳細情報について

  • CRID
    1050001338306687488
  • NII論文ID
    170000150344
  • NII書誌ID
    AA11464814
  • ISSN
    18827802
  • Web Site
    http://id.nii.ac.jp/1001/00195736/
  • 本文言語コード
    ja
  • 資料種別
    article
  • データソース種別
    • IRDB
    • CiNii Articles

問題の指摘

ページトップへ