ヾﾉ*＞ㅅ＜)ﾉｼ帳

ノンジャンルのふりーだむなブログです。

形式手法のこれまでとこれから

セキュリティ 形式手法 論文紹介 シンボリック実行

2019年が終わろうとしています あけおめ～さて2020年になりました。歴史が長い形式手法の今後を占うため、過去と直近の出来事を振り返りたいと思います。

ツッコミやタレコミは私のTwitter宛かあなたのブログかその他経路でお願いします～

シンボリック実行は形式的であるため本稿では形式手法に含めることにします。 Fuzzing関連はサーベイが甘いので漏れが多いかもしれません。

形式手法・形式検証とは

形式検証とは、厳密に定義された意味論の下で仕様やプログラムが所定の性質を満たすことを形式的に検証するための手法をいいます。「形式的に」とは、検証が事前に定義された知識だけに基づいており、検証手順が決定的であることをいうと私は理解しています。 形式手法は、形式検証に加えて、形式的にプログラムの仕様を厳密に定義するための手法を包含します。

本記事では形式手法を以下の通り大きく3つに独自に分類します。MECEであるかは自信ないです。私はそこまで専門家ではありませんのであしからず。

  • セマンティクスベース
    • プログラムの意味論に従って状態の変化を追跡する形式手法
  • 型ベース
    • 型に着目する形式手法
  • モデル検査
    • システムを有限の個の状態を持つモデルで表現し、各状態・各状態遷移間でシステムが満たすべき性質が満たされることを機械的に網羅的に検査する手法
    • 本稿では扱いません

これまで

セマンティクスベース

シンボリック実行

シンボリック実行の歴史の概略と個人的に重要と思っている論文などは以下の通り。 詳細は https://github.com/enzet/symbolic-execution/blob/master/README.md や A Survey of Symbolic Execution Techniques (arXiv 2018) を参照するとよい。

  1. シンボリック実行の発明（1976年）
    • Symbolic Execution and Program Testing (1976)
  2. SMTとシンボリック実行エンジンの勃興（～2015年）
    • STP 2007年→KLEE 2008年→S2E 2011年
    • z3 2008年→angr 2015年、Triton 2015年
  3. シンボリック実行の効率化に着手する研究が隆盛（～2010年後半）
    • Efficient Directionless Weakest Preconditions (2010) ※Backward Symbolic Executionを取り入れた異端児
    • Unleashing MAYHEM on Binary Code (S&P 2012)
    • Enhancing Symbolic Execution with Veritesting (ICSE 2014)
  4. エクスプロイト生成に着目する研究が隆盛（2011～2016年）
    • AEG: Automatic Exploit Generation (2011)
    • Mayhem (2012)
    • Cyber Grand Challenge (2016) ※エクスプロイト生成とパッチ生成自動化のDARPA主催のコンテスト
    • Mechanical Phish (2016) ※Drillerベース、論文なし、ソースコード参照
  5. シンボリック実行✕ファジング＝Hybrid Fuzzing（2012年～？）
    • Hybrid Fuzz Testing: Discovering Software Bugs via Fuzzing and Symbolic Execution（修士論文 2012） ※Hybrid Fuzzingの発明
    • Driller: Augmenting Fuzzing Through Selective Symbolic Execution (NDSS 2016)
    • QSYM; A Practical Concolic Execution Engine Tailored for Hybrid Fuzzing (USENIX Security 2018)
  6. シンボリック実行の簡易化（2019年～？）
    • Neuro-Symbolic Execution: Augmenting Symbolic Execution with Neural Constraints (NDSS 2019)

勘がいい人は列挙している論文の著者に David Brumley 氏が多く紛れていることに気づいたかもしれません。そういうことです（彼ブルドーザーかよ～高速地ならしｺﾞｺﾞｺﾞｺﾞ～😇

シンボリック実行の簡易化が今後盛り上がるかはわからんです。2020年のS&P, NDSS, USENIX を見れば分かるでしょう。

ニューラルネットワークの検証

シンボリック実行の適用領域について新しい動きも見られるようになりました。

  • Symbolic Execution for Deep Neural Networks (arXiv 2018)

  • Concolic Testing for Deep Neural Networks (ASE 2018)

プログラムの実装の正しさを形式検証（定理証明）

プログラムに対する事例は以下の通りです。この辺の話は形式検証では既定路線ですね。

  • K Framework

    • K Frameworkは、意味論を扱うことができるフレームワーク。プログラム言語の仕様を定義し、あるプログラムを実行し、初期状態がある状態に遷移することを保証できる。
    • OSS！

  • Runtime Verification

    • K Frameworkをベースに、C言語プログラムやスマートコントラクトが正しく実装する製品を提供する会社

  • Imandra

ブロックチェーンに対する事例は以下の通りです。これは想像ですが、ブロックチェーンで形式手法が積極的に取り入れられている理由は、一度導入されてしまうとバグによって生まれた不正な結果の取り消しが困難であり、金と時間をかけた従来型のテストを行ってもユーザーにそのコストを払ってもらうことは非現実的であるため安価に品質保証できる手法が求められている、といったところでしょうか。

並列計算や分散システムに対する形式検証（定理証明）

2018年から私の目に入るようになったのが、並列計算や分散システムに対する形式検証です。産業系の場で取り組みの成果の共有が多くありました。

型ベース

BPF

BPFはプログラムが安全であることを検証するための検証器を持っています。検証器は型をベースに実装されています。

cf. BPFプログラムの作成方法、BPFの検証器、JITコンパイル機能 (2/3)：Berkeley Packet Filter（BPF）入門（3） - ＠IT

これから

私が気になっているテーマや動きをまとめていきます。

（継続？）シンボリック実行とランダムテストの中間を攻める新しいソルバーの登場

2019年時点では、シンボリック実行エンジンの実装や、シンボリック実行の効率化に着手する研究やシンボリック実行だけでクスプロイト生成に着目する研究は落ち着いた（オワコン化）したように見えます。

エクスプロイト生成については、現在Fuzzingの文脈で語られることが多いため、今から研究する場合はFuzzingをメインとして行い、シンボリック実行は補助的に用いるのがいいかもしれません（が、QSYM という強力な解みたいのが出ているのできついかもしれません）。

シンボリック実行よりは処理が軽くて探索を効率化できるような手法として、私は型をベースにした何かが面白そうと感じていますが、どうですかね（サーベイしてない顔

（継続）ブロックチェーン✕形式手法

この組み合わせの盛り上がりは2020年以降もしばらく維持されると思います。

で、面白いのが、京大の末永先生（形式検証ガチ勢）やDaiLambda社たちに、Tezosから検証系の何かを開発するための助成金が下りたようです。ウォッチしたい動きですね。

https://tezos.foundation/news/tezos-foundation-issues-grants-for-tezos-smart-contract-projects

Led by Atsushi Igarashi, Ph.D., a professor at the Graduate School of Informatics, and Kohei Suenaga, Ph.D., an associate professor at the Graduate School of Informatics, the team will create an accessible development tool for these verification techniques and contribute to the growth of the Tezos ecosystem in Japan and the greater Asia region. Jun Furuse of DaiLambda and Tezos Japan collaborates with Kyoto University on this project.

（継続？）AIの学習済みモデルに対する形式検証

第三者がAIの品質を検証できるようにするという体は相変わらず今後維持されると思います。

関連研究が増加するとしたら、どんな成果が出てくるか私は想像がつかないですね…。面白いのが出てくるといいなぁ。

（継続）並列計算や分散システムに対する形式検証

このテーマは継続して取り組まれて、国内でゆるやかにコミュニティが出来上がってくるような気がしています。

私はこの辺をキャッチアップするのはまだできなそうなので、トピックを追うだけにしておこうと思います。

（継続？）形式検証を頑張る国内の会社の増加

形式検証を頑張る国内の会社の増加しました。国内で形式手法が盛り上がっていくといいですね。

彼らからの情報発信は引き続き追っていきたいと思います。

気になっている個別トピック