読者です 読者をやめる 読者になる 読者になる

by shigemk2

当面は技術的なことしか書かない

QEMUのDynamic Binary Translationがあってよかったねという話 #kernelvm

勉強会

QEMU

  • 伏魔殿
  • インシデントレスポンスごっこ
  • 謎のマクロ
  • C言語のくせにnewとかあるし
  • 仮想化技術について学びたい

QEMU

  • 異なるアーキテクチャのモードをサポートしている

TCGによってDBTを実現

  • ゲストのコードを逆アセ
  • 中間コードに変換
  • ホストのコードに変換
  • 実行

  • main()からcpu_exec()

実行コードをごにょごにょするのは大変

Basic Blockで切り分ける

なんかLLVMぽくない?

バイナリをLLVMに逆コンパイルするためにQEMUを研究している

semantic gapをどうするか

semantic gapの意味 - 英和辞典 Weblio辞書

高水準言語の言語要素とこれらを実現するためのコンピュータの機能構造との間には大きな隔りがあること.例えば,配列,データ型,文字列処理,手続き,ブロック構造などを取り扱うには,多数の機械語命令が必要になる.

KLEE

  • LLVMでビルド
  • テストケースを生成
  • 15年かけて書いた手動テストを89時間で達成

Symbolic execution

  • 記号実行と訳される
  • 変数に台数シンボルを与えて監視

SAT solver

DPLLアルゴリズム - Wikipedia

SMT solver 入門 - すえひろがりっっっっ!

続・今日も反省の色無し(masayangの日記): S2Eで内部記憶領域(mmcblk0)を開放

まとめ

  • LLVMbitcodeとx86にあるsemantic gapをQEMUで達成
  • OpticodeでバイナリをLLVM bitcodeに変換
  • LLVMへの逆コンパイルとsymbolic executionへの適用

  • QEMUのDBTがあってよかったね

モデルベーステスト - Wikipedia