ヾﾉ*＞ㅅ＜)ﾉｼ帳

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

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

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

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の品質を検証できるようにするという体は相変わらず今後維持されると思います。

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

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

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

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

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

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

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

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

SECCON 2019 決勝 の Challenge 4 follow-me-again を振り返る

CTF セキュリティ 友利奈緒

2019/12/21（土）から2019/12/22（日）の2日間にかけてSECCONの決勝が開催されました。 私は友利奈緒としてChallenge 4の出題をしました。好評なようで良かったです。 今年は国内大会と国際大会が同じスケジュール・問題セットで実施されました。 試合時間は6時間＋6時間と長期戦でしたね。本当にお疲れさまでした。 私の問題を粘って解いてくれたチームが多く感謝します。 こちらも約30チーム日本語・英語問わず問い合わせが来たり、致命的なバグの修正を競技時間中に行ったりと大変でした…。 （リカバリーはできたものの、本番中に大きなやらかし3つして迷惑かけてごめんなさい。

さて、私が出題した問題は follow-me-again です。今年の予選で出題した follow-me は実はこれの予告編でした。 皆さん、どこまでちゃんと解けましたか？ follow-me は与えられたバイナリと実行トレース（実行された分岐命令と分岐結果の時系列の並び）から、実行パスを割り出し、そのパスを通るような入力を求めるという問題です。 Write-upはチェックしましたが、

あたりが主だっていました。楽しんでもらえて嬉しいですが、ファジングを除き特定のバイナリに依存した解法が好まれており、私は不満でした。 が、ここまでの流れは完全に計算通りでした（CV 夜神月）。 決勝で私が目指したのは、バイナリが変化したときにも適用できるような一般的な解法をプレイヤーに実施してもらうことです。

決勝の follow-me-again は、SECCON決勝のルールに則る形でAtttackとDefenseのフェーズに分かれています。 Attackは、Defenseの雰囲気を掴んでもらうためのサニタイズ問題1問、暗号やCPUエミュレータの実装に関する知識を問う3問の構成です。 回答状況を見ると2日目に提出が多かったので後回ししてくれたのでしょう。期待通りです。 最初に着手して欲しかったのがDefenseです。 Defenseは、予選と同様計算機を模したバイナリと実行トレースが与えられそれと同じ実行パスを通る入力を求める問題が1時間毎に出題されます。 それを早解きしたチームが得点できます（SECCONのDefense Pointの仕様上、早く解くほどDefense Pointを得られます）。

GitHubに問題とソルバーを雑に置いたので見てみてください。

https://github.com/K-atc/follow-me-again-public

決勝の結果は私好みでした。 Attackは、4問中2問正解が中央値に落ち着きました。全完（すばらしい！）が数チームといういい塩梅の結果です。 Defenseは、国内はkimiyuki（ぼっちーむで国内2位の実力者）と dodododo（国内1位）の争いがありましたが、kimiyukiが大半のポイントを獲得しました。 国際は4チームくらいが奪い合っていましたが、2日目の午後辺りからnoranekoが完全に抑えました。 国内も国際も1番手と2番手の提出時刻の差が10秒や40秒の熾烈な争いとなりました。 限られた数チームが僅差で争う――こうやって難易度調整がうまくいくとうれしいですね。

f:id:katc:20191223001609j:plain

ここで友利賞のお知らせです。 国内・国際大会それぞれで最も優れたソルバーを書いたチームを表彰します :tada: 奈緒、賞品はありません。あしからず。

国内大会の友利賞は～～～～ kimiyuki です！おめでとうございます！ 受賞の理由は、まともに早く動くソルバーを国内で唯一作れたことです。 シンボリック実行に逃げずに貪欲法を使ったソルバーも評価高いです。Weite-up待ってます(´へωへ`*)

国際大会の友利賞は～～～～noraneco です！おめでとうございます！ ベスト・オブ友利賞も差し上げます！ 受賞の理由は、国際のDefense Pointを抑えたその性能、第11、12ラウンドで今までの流れを断ち切ったバイナリに対しても途切れずに即答するその性能です。 kimiyuki ソルバーは第11ラウンドで3回分のDefense Pointを取り逃してもったいなかったです。 ではWeite-up待ってます(´へωへ`*)

…まぁ彼らのソルバーは2,3分かかるようですが、私のソルバーは10秒です。まだまだですね（とはいえ私のソルバーを見れば分かると思いますが、時間の制約上仕方ないです）。

最後に、遊んでくれた皆様ありがとうございました！ Challenge 4のおかげで学びと実践のある2日間になったなら嬉しいです。

おまけ：問題を1問も解けなかった人へ

問題を解くうえで前提知識が足りてなかったのでしょう。 最近のバイナリ解析を学んでみてください。キーワードとしては、DBI、シンボリック実行、Intel Software Development Manual、です。 どれもアカデミア方面でバイナリ解析や脆弱性検出で必要な知識なので、触りだけでも理解しておくと今後の人生で役立つでしょう。 Intel SDMは、分岐命令のジャンプ有無の計算方法がどこに書かれているのかを覚えて、読み解けるようになりましょう。

初学者向けの参考書籍として、Practical Binary Analysis | No Starch Press をおすすめします。

Special Thanks

Attackの問題で、x86エミュレータの rkoder/emu_x86 をお借りしました。素直な実装で使いやすかったです。

「見えているのに見えていない！立体錯視の最前線」に行ってきた

美術

9月5日、出勤前に寄り道して、明治大学博物館（明治大学の駿河台キャンパス）の特設展として開催されていた「見えているのに見えていない！立体錯視の最前線」を観覧してきました。 「駿河台」から連想されるように大学の周りは坂で、ちょっとしたハイキングでした。

会場はワンルームマンション2部屋分くらいのこじんまりしたスペースで、私以外にも10人くらいは常にいたくらいには盛況していました。

内容はだまし絵立体（無限階段）から鏡を使った錯視まで幅広く展示されていました。

知見を箇条書きしていきます。

  • だまし絵立体は裸眼では錯視を感じにくく、カメラを通すとようやく錯視を知覚することができる。
  • 鉛筆で折れ線を書いたままの厚紙でできたものも多い。圧倒的手作り感。

感想

鏡を使う錯視が一番わかりやすく、脳が混乱して面白かったです。 写真の例だと実物と鏡像が一致しないという面白さがあります。

f:id:katc:20190905112018j:plain

展示も工夫されていました。実物だけをぱっと見ても、どう見るのが正解なのかが分かりません。 作品タイトルの隣に写真があって、「このようにスマホのカメラに映れば正解」とアノテーションがあったので鑑賞しやすかったです。 （がこの細やかな配慮に半数の作品を見てから気づきました😇）

素直に科学とアートが両立していてずるいと思いました！ 私はエンジニアリングとイラストを両方かじってますが、1つのことで科学とアートを両立するものは珍しいです。 私もこういうスイートスポット見つけたいなー。

［論文紹介］Neuro-Symbolic Execution: Augmenting Symbolic Execution with Neural Constraints (NDSS 2019)

シンボリック実行 論文紹介

はい、シンボリック実行だいすきクラブの友利奈緒です。通勤中に論文を読んでる系の女の子なのですが、ここ半年は本を読んでいたので論文サーベイがすっかりご無沙汰になっていました＞＜

Semantic Scholarから送られるSymbolic Executionタグのアラートを半年眺めていた限りでは、Blockchainのスマートコントラクトの検証（Verification）やJavaScript・Javaのシンボリック実行が多かった印象でしたが、調べてみると面白い論文が出てました。シンボリック実行はまだまだ盛り上がっててよかったです…>_<…

今回は今年のNDSS（コンピュータセキュリティの学会系トップカンファレンス）で採択された "Neuro-Symbolic Execution: Augmenting Symbolic Execution with Neural Constraints" の論文紹介です。 リンク先には論文とスライドと発表動画があります。

https://www.ndss-symposium.org/ndss-paper/neuro-symbolic-execution-augmenting-symbolic-execution-with-neural-constraints/

論文では言及されていないが、私が補足が必要と思って書き足したところには「友利注」を付けます。

シンボリック実行の説明は省略します。 シンボリック実行には数種類のアルゴリズムがあるのですが、一般に言われるシンボリック実行の説明は以下のスライドの9～15ページ目を読むとだいたい分かると思います。

speakerdeck.com

背景

本論文で着目している、シンボリック実行における問題は次の3つ。

  • 制約導出の困難さ
    • 一般に目的の状態（本論文では特定箇所の脆弱性）が発現する地点に到達するのが難しい
      • 例）複雑なループ
        • 友利注：ループがn個あり1個のループが高々m回で抜けられるならば、状態数は O(m^n) 。基本無理ゲー
      • 要はパス爆発（Path Explosion）問題に直面する
  • 制約ソルバーの限界
    • KLEEは浮動小数点に非対応。最近のSTPとZ3は浮動小数点に対応しているがとても遅い。
      • 友利注：整数よりも実数が圧倒的に探索空間が広いので遅いのは仕方ないかも。
    • 浮動小数点をBitVector（SMTにおけるバイナリ値の表現形式）として扱っても実用的な時間内で充足できなかった。
  • 実行対象のコードの欠損
    • シンボリック実行エンジン（が採用しているライブラリ）が実行対象で呼び出される一部の関数に対応していない（シンボリック実行あるある）。
      • 友利注：シンボリック実行エンジンはライブラリ関数の呼び出しに対し、通常実行で使用されるライブラリ（glibcなど）の代わりに簡易なライブラリを用意して対処する。
        • KLEEはuClibcという簡易で軽量なlibcを採用しているが、全部のlibc関数には対応していない（本論文の場合はfabs）。
        • angrはsymbolic summaryと呼ばれるlibcの各関数の作用をシンボリックに表現した関数を取り揃えているが、全部のlibc関数には対応していない。

やったこと

Newro-symbolic実行エンジンNeuExを実装した。NeuExは脆弱性の候補箇所（CVP; Candidate Vulnerability Point) に対して、脆弱性を発現する入力（Crash Inputs; Validated Exploits）を生成する。

コンセプト

本論文では先の困難に対して以下のアプローチを取った。

  • (1) シンボリックモードとニューロンモードの2つの実行モードを持つ
    • シンボリックモードは従来シンボリック実行
    • シンボリックモードが行き詰まるとニューロンモードに移行
      • 4種類の移行条件：(a) モデル化されていないAPIの呼び出し (b) ループの繰り返し数が上限値に到達 (c) Z3がタイムアウト (d) メモリ使用量が上限値に到達
    • ニューロンモードでは入力は具体値。制約をニューラルネットワークで内包し、制約を満たす入力 \mathbf{x} （実行対象への入力）と出力 \mathbf{y} （制約式で拘束された変数）の組を学習する。
      • 友利注：クラス分類問題ではない。あくまで関数 N: x \mapsto y の表現方法を学習するだけ（回帰問題）。
  • (2) シンボリック制約を多層パーセプトロンにより近似解で求める
    • シンボリック制約は誤差関数に変換される
    • 解の導出方法はニューロンモードで述べたとおり。

Neuro-symbilicのアイデア（ニューラルネットワークとシンボリック実行の組み合わせ）は新規。先行研究（友利注：引用されている範囲では不変式（Invariant）に関するもの）では制約の導出にシンボリック実行ではない帰納的なアプローチが取られていたが、1つもニューラルネットワークを採用していなかった。

アプローチ詳細

システム構成

f:id:katc:20190608193341p:plain
Fig. 4

Neural Modeの構成

f:id:katc:20190608193225p:plain
Fig. 5

以下の要領でニューラルネットワークの訓練データ (\mathbf{x}, \mathbf{y}) （論文の表記は (\mathbf{I}_i, \mathbf{O}_i) ）を得る。

  1. Neural Modeに移行後、NeuExはコールグラフを参照し、現在のシンボリック状態でパス上では到達可能なCVPを選出する。
  2. 着目している分岐（友利注：原文ではsymbolic branch。【何のこと？】）を始点、着目するCVPを終点として、始点から終点までを実行する。
    • 入力はシンボリック制約から生成された具体値をシードとしてランダム生成されたもの（たいてい10万個）
    • 入力のうちいくつかは終点に到達する（友利注：このとき\mathbf{x} と\mathbf{y}の対応を得られる）
    • 友利注：終点はCVPにおける制約式で拘束された変数 \mathbf{y} を含むことに注意

Neural-symbolic制約の充足

NeuExはNeural-symbolic制約充足にSymSolvとNeuSolvと呼ばれる2種類の制約ソルバーを組み合わせる。

SymSolv

SymSolvはいわゆるSMTソルバーが対応するような制約式を取り扱う制約ソルバー。

NeuSolv

論文とスライドの書き方がわかりにくいので、NeuSolvについては全面友利注とする。【注意：本論文・スライド・発表動画を参照した上でエスパーした内容が多分に含まれる上に、私の数学力不足に起因する誤りがある可能性がある】

NeuSolvは、ニューラル制約を数値解析における最急降下法により解く。

ニューラルネットワークは先の学習により関数 N: \mathbf{x} \mapsto \mathbf{y} を自身のネットワークにより表現可能となっている。 ここで、あるCVPのシンボリック制約を式 C(\mathbf{y}) = 0 とする。NeuExはこれをロス関数 L(\mathbf{y})（友利注：ニューラルネットワークの学習におけるロス関数とは別物）に変換する。

ロス関数 L は以下の性質を持っている。

  • 制約を充足するまでは \nabla L が非ゼロ
  • 下限が存在
    • でないと探索が停止しない
  • 友利注： 関数 N, L について、 N: \mathbf{R}^n \rightarrow \mathbf{R}^m, \quad L: \mathbf{R}^m \rightarrow \mathbf{R}

ロス関数の性質から、以下を満たす \mathbf{\hat{x}} はCVPの制約を満たす。

L(N(\mathbf{\hat{x}})) = \min(L(N(\mathbf{x}))

上の非線形方程式を解くために数値解析で用いられる以下の最急降下法を用いる（ k は反復回数）。

{\mathbf{x}}^{(k+1)} = {\mathbf{x}}^{(k)} + \epsilon \nabla L (N(\mathbf{x}^{(k)})) （これは論文の式(5)）

問題は \nabla L (N(\mathbf{x})) が計算可能かどうかである。

\mathbf{y} = N(\mathbf{x}), z = L(\mathbf{y}) とすると、

\nabla L (N(\mathbf{x})) = \left[\dfrac {\partial z}{\partial x_0}, \cdots, \dfrac {\partial z}{\partial x_i}, \cdots, \dfrac {\partial z}{\partial x_n}\right]^T .

ここで連鎖律により、

\dfrac {\partial z}{\partial \mathbf{x}} = \dfrac {\partial z}{\partial (y_1, \cdots, y_ m)} \dfrac {\partial (y_1, \cdots, y_j, \cdots, y_ m)}{\partial (x_1, \cdots, x_i, \cdots, x_n)} = \nabla L(\mathbf{y}) \dfrac{\partial N}{\partial \mathbf{x}} (*1)

であることに注意すると、 \nabla L(\mathbf{y}) = \left [ \dfrac{\partial L(\mathbf{y})}{\partial y_1}, \cdots, \dfrac{\partial L(\mathbf{y})}{\partial y_m} \right]^T は L の定義（Table II）から導出可能であり、また

\dfrac{\partial y_j}{\partial x_i} = \dfrac {\partial N_j(\mathbf{x}) }{\partial x_i} \approx \dfrac{ N_j(x_1, \cdots, x_i + \Delta x_i, \cdots, x_n) - N_j(x_1, \cdots, x_i, \cdots, x_n)}{\Delta x_i}

であるから、 \nabla L (N(\mathbf{x})) は計算可能。

(*1) \dfrac{\partial N}{\partial \mathbf{x}} はヤコビ行列

（本当にこれで合ってるのだろうか？ \nabla L (N(\mathbf{x})) の計算方法の説明がどこにも無かったし…）

シンボリック制約からニューラル制約への変換方法

Neuro-symbolic Executionを実行しているとシンボリック制約とニューラル制約の2種類の制約が混合する。 混合した制約を解くためにNeuExはシンボリック制約をニューラル制約（正確にはロス関数 L ）に変換する。 変換はTable IIに従う。

f:id:katc:20190607003245p:plain
Table II

ロス関数 L は上述の性質を満たすように人為的に定義されている。

Neuro-symbolic Executionにおける制約充足アルゴリズム

f:id:katc:20190609024330p:plain
Algorithm 1

※アルゴリズムの説明は省略。

（友利注：書くの飽きてきた…。方針としては、DAG上で変数の依存関係が独立なコード片を順々にNeural Executionし、最後にそれらの制約をシンボリック実行の結果とマージという感じみたいね。）

評価

NewExの実装は以下の構成。

  • KLEE v1.4ベース（友利注：KLEEの2019/06/09時点の最新版はv2.0（2019年5月リリース）。1つ前のバージョンが1.4）
  • libcには KLEE-uClibc を採用（友利注というか疑問：ソースコードが入手可能であることを前提にしてる？）
  • SMTソルバーはZ3

評価は以下の観点で行った。

  • (a) KLEEに対する効率性
    • 素のKLEEと比べてNeuExはより多くの脆弱性を見つけるのか？（友利注：原文よりも目的を明確に意訳した）
  • (b) Neural Modeの効用
    • Neural Modeの呼び出し回数、エクスプロイト生成数、実行時間はどうか？
    • 友利注：Neural Modeが一度も呼ばれなかったり、何もエクスプロイトを生成してなかったり、Neural Modeの実行時間が卓越したりするオチもあり得るので大事な観点。
  • (c) 既存のシンボリック実行テクニックとの比較
    • 友利注：素のKLEEを最適化するとKLEEよりも成績が良くなるのは自明なので、同一環境で既存の最適化手法（今回はLESEと、Veritestingを採用したangrの探索モード）と比較するのは必須。

実験条件

(a) KLEEに対する効率性

KLEEに対してNeuExはCVPに到達できた数とその早さにおいて優位であり、エクスプロイトの生成数（友利注：脆弱性を再現できた数）においても優位。

f:id:katc:20190609031848p:plain
Table III

f:id:katc:20190609033429p:plain
Fig. 7, 8

(b) Neural Modeの効用

Neural Modeは使用されたし、いくつかのCVPに到達できているし、少数のエクスプロイトを生成したことが分かる。

f:id:katc:20190609033115p:plain
Table IV

(c) 既存のシンボリック実行テクニックとの比較

  • LESE (ISSTA 2009)（バイナリのループに関する推論を行うテクニック）
    • LESEの実装が公開されていないので、論文に掲載された実験条件と同等環境を用意し、同じベンチマークを実施した。
    • NeuExはNeuro Modeのみ使用した。変数の関係性の学習においてニューラル制約のアイデアがLESEに対して優位であることを確認するため。
    • 脆弱性検出の早さについては、NeuExはLESEに対して平均2桁倍だった。
  • Veritesting (ICSE 2014)（友利注：静的シンボリック実行と動的シンボリック実行を複合するなど）
    • Veritesting の実装（友利注：MergePoint）が公開されていないので、Veritestingを再実装している angr と比較した。
    • Veritestingは脆弱性の箇所を教える必要あり。同じ開始条件で実行するとNewExは34分で脆弱性を検出したが、angrは12時間以内に検出せず。angrでは198の外部関数の呼び出しがあったがいずれも対応せず。

結論

  • NeuExはニューラルネットワークを用いてプログラムの振る舞いを近似する制約を学習する。
  • Neuro-symbolic Execition はシンボリック制約とニューラル制約の複合した制約を解くことができる。
  • 素の動的シンボリック実行に対してバグの検出件数が94％増加した。

所感

単純なネットワークでもプログラムの断片における変数間の関係（ N: \mathbf{x} \mapsto \mathbf{y}）を学習できるんだなぁという知見を得た。 ニューラルネットワークの実装に関する以下の記述を読んでも、入出力の次元数 、隠れ層の次元数と層数が書かれてなかったのでどの程度のネットワークがあればいいのかがワカラン。 Neural ModeとNeuSolvだけを見ても新規性があるかどうかが気になる。

Training. Next, the neural constraint inference engine takes 80% of all the generated sample sets for training the neural net. We use a standard MLP architecture with Relu activation function implemented in Python and Google TensorFlow [29] with a total of 208 LOC. We use the early-stopping strategy to avoid over-fitting. We test the remaining 20% of the sample set on the learned neural net to measure its accuracy. We continue the training until we achieve at least 80% accuracy. If the loss of the trained neural net does not start decreasing after a threshold of 50 epochs, we discard the search for an exploit for the corresponding CVP.

Neural ModeとNeuSolvはシンボリック実行に依存していないように見える。 \mathbf{x}, \mathbf{y}, L(\mathbf{y}) を得られれば適用可能に見える。 \mathbf{x}, \mathbf{y} はランタイムで得られ、 L(\mathbf{y}) はCVPを元に機械的に計算可能。 ならシンボリック実行だけでなくファジングでも適用できるのでは？

私の理解が正しければ元のプログラム自身も関数 N を持っているとみなせるので、ニューラルネットワークを用いて \dfrac {\partial N}{\partial \mathbf{x}} を計算しなくても、元のプログラムを使ってそれを計算できる気がする（まぁ実装して検証すればいい話）。よく分からなくなってきた…😇

付録：多層パーセプトロンの復習

ニューラルネットワークの構成方法の1つである多層パーセプトロンについて復習しよう。

まず多層パーセプトロンのネットワーク構成について復習する。

多層パーセプトロン

層数 L の多層ネットワークを考える。層 l+1 のユニットの出力 \mathbf{z}^{(l+1)} は、1つ下の層 l のユニットの出力 \mathbf{z}^{(l)} から

\mathbf{u}^{(l+1)} = \mathbf{W}^{(l+1)} \mathbf{z}^{(l)} + \mathbf{b}^{(l+1)}

\mathbf{z}^{(l+1)} = \mathbf{f}(\mathbf{u}^{(l+1)})

のように計算される。ここで、 \mathbf{W} は重み、 \mathbf{b} はバイアスとよばれ、\mathbf{w}をこれらのパラメータすべてを成分に持つベクトルとする。

ネットワークの最終出力 \mathbf{y} は

\mathbf{y} \equiv \mathbf{z}^{(L)}

と得る。

次には学習方法を復習する。

確率的勾配降下法

入力 \mathbf{x}_n を与えたときのネットワークの出力 \mathbf{y}(\mathbf{x}_n; \mathbf{w}) がなるべく訓練データ(\mathbf{x}_n,\mathbf{d}_n) の \mathbf{d}_n に近くなるように \mathbf{w} を調整する。これを学習と呼ぶ。

ネットワークのパラメータ \mathbf{w} の調整には

\mathbf{w} ^ {(t+1)} = \mathbf{w} ^ {(t)} - \varepsilon \frac{\partial}{\partial \mathbf{w}} L(\mathbf{w})

を用いる。ここで t をエポック、L を誤差関数とする。

PYNQでLチカしてみる～Verilog＆Chisel3～

これは備忘録です。かなり雑な書き方でメモります。

Verilog編

参考： Chisel + PYNQでLチカ（お正月FPGAあそび） - /home/tnishinaga/TechMEMO

  1. Xilinxの Vivado Design SUite - HLx Edition 2019.1 をダウンロードしてインストール
    • 要アカウント登録
    • インストールには40GBの空き容量が必要
    • ダウンロードとインストールに5時間くらいかかった
  2. PYNQをPCに接続
  3. Lチカコードを書く
  4. ポート割り当て
  5. Bitstreamを生成
  6. ボード書き込み
    • [PROGRAM AND DEBUG] - [Open Hardware Manager] - [Program Device] で書き込み先のボードをPYNQと指定し、書き込むファイル（自動で入力されているはず）を選択する

ポート割り当て

RTL を生成したあとに、IOポートと作成したモジュールのポートの対応関係を割り当てる。

[RTL ANALYSIS] タブをクリックし、 [Open Elaborated Design] タブの中にある [Schematic] をクリック。ウインドウ下部に [I/O Ports] のサブウインドウが表示されなかったら、メニューバーの [Window] - [I/O Ports] をクリック。

割り当ては各ポートの [Package Pin] フィールドをクリックした後、ポート名をタイプして行う。

Lチカコード

module blink(
    input clk,
    output [3:0] port_out
    );

parameter cnt_1sec = 27'd124999999;
reg [26:0] cnt = 27'd0;
reg onoff = 1'b1;

always @(posedge clk) begin
    if (cnt == cnt_1sec) begin
        cnt <= 27'd0;
        onoff <= ~onoff;
    end
    else begin
        cnt <= cnt + 27'd1;
    end
end

assign port_out = {onoff, onoff, onoff, onoff};

endmodule

assign out = {onoff, onoff, onoff, onoff} になっていて、出力ポートが宙ぶらりんになっていて、LEDが光らないというやらかしをした。

Chisel3編

2019/06/02 Chisel3

参考： Chisel + PYNQでLチカ（お正月FPGAあそび） - /home/tnishinaga/TechMEMO

  1. Chiselのテンプレート を git clone
  2. Blinkモジュールを追加
  3. ビルド → Blink.v を生成
  4. Vivado でビルド → PYNQに書き込み【エラー発生で不可】

Blinkモジュールを追加

github.com

  • Blink.scala でLチカを実装
    • 入力のClock信号はVerilog生成時に自動追加されるので宣言不要
  • BlinkMain.scala でVerilogコードを生成する
    • ※本来はテストコードも書くファイルだが省略

/src/main/scala/blink/Blink.scala:

package blink

import chisel3._

class Blink extends Module {
  val io = IO(new Bundle {
    val portLed = Output(UInt(4.W))
  })

  val cnt1sec = RegInit(124999999.U(27.W))
  val cnt = RegInit(0.U(27.W))
  val onoff = RegInit(false.B)

  when(cnt === cnt1sec) {
    cnt := 0.U
    onoff := ~onoff
  } .otherwise {
    cnt := cnt + 1.U
  }

  io.portLed := onoff
}

/src/test/scala/blink/BlinkMain.scala:

package blink

import chisel3._

object BlinkMain extends App {
  chisel3.Driver.execute(args, () => new Blink)
}

ビルド

  • --target-dir は生成したファイルを格納するフォルダの場所。
  • --top-name はVerilogなど生成するファイルのbase nameを指定する。
$ sbt 'test:runMain blink.BlinkMain --target-dir build --top-name Blink'
[info] Loading settings from plugins.sbt ...
[info] Loading project definition from /***/chisel-pynq/chisel-template/project
[info] Loading settings from build.sbt ...
[info] Set current project to chisel-module-template (in build file:/***/chisel-pynq/chisel-template/)
[warn] Multiple main classes detected.  Run 'show discoveredMainClasses' to see the list
[info] Running blink.BlinkMain --target-dir build --top-name Blink
[info] [0.010] Elaborating design...
[info] [6.169] Done elaborating.
Total FIRRTL Compile Time: 1189.4 ms
[success] Total time: 29 s, completed Jun 2, 2019 7:51:56 AM

$ ls build
Blink.anno.json  Blink.fir  Blink.v

参考） Blink.v

module Blink( // @[:@3.2]
  input        clock, // @[:@4.4]
  input        reset, // @[:@5.4]
  output [3:0] io_portLed // @[:@6.4]
);
... snipped ...

Vivado でビルドしてみる

Implementationできなくて詰んだ。ナニコレ🤔 🤔 🤔

f:id:katc:20190602173531p:plain

[Place 30-574] Poor placement for routing between an IO pin and BUFG. If this sub optimal condition is acceptable for this design, you may use the CLOCK_DEDICATED_ROUTE constraint in the .xdc file to demote this message to a WARNING. However, the use of this override is highly discouraged. These examples can be used directly in the .xdc file to override this clock rule.
    < set_property CLOCK_DEDICATED_ROUTE FALSE [get_nets clock_IBUF] >

    clock_IBUF_inst (IBUF.O) is locked to IOB_X1Y112
     and clock_IBUF_BUFG_inst (BUFG.I) is provisionally placed by clockplacer on BUFGCTRL_X0Y31

技術書典6でSecure旅団に寄稿しました

セキュリティ 同人誌

今更の宣伝ですが、Secure旅団の同人誌第4弾『セキュリティ畑でつかまえて』に「K Framework を用いた脆弱性検出支援」という題で寄稿しました。 先の技術書典6で頒布されました。 現在電子版がBoothで販売されています。

セキュリティ畑でつかまえて - Secure旅団 - BOOTH

参考までに私の内容を冒頭だけ掲載します。

はじめに

はい、ども、友利奈緒（@K_atc）です。 私が所属しているサークルTomoriNaoが技術書典6で落選太郎したのでお邪魔してみました＞＜ 私はソフトウェアの脆弱性検出を趣味で研究しています。レイヤー低めな人です。

今回は、K Frameworkというプログラミング言語の意味論を実行可能とするフレームワークを用いて、 C言語プログラムの脆弱性検出を支援してみました。 最初に、簡単なプログラミング言語を定義しながら、K Frameworkが何たるかを説明します。 次に、RV-Matchという、K Framework上でC言語を定義したフレームワークを紹介し、動作確認として範囲外参照を検出してみます。 最後に、RV-MatchもといK Frameworkは脆弱性検出の場面で有用かもしれないことを示したいので、 ファジング（脆弱性検出の方法の一つ）で検出されたクラッシュの原因調査を効率化するデモをしてみます。