ヾノ*>ㅅ<)ノシ帳

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

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

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

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

今回は今年の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.scalaVerilogコードを生成する
    • ※本来はテストコードも書くファイルだが省略

/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-nameVerilogなど生成するファイルの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は脆弱性検出の場面で有用かもしれないことを示したいので、 ファジング(脆弱性検出の方法の一つ)で検出されたクラッシュの原因調査を効率化するデモをしてみます。

0ctf 2019 Quals の babyrsa (crypto) の Writeup

2019/3/23 ~ 3/24 ぐらいに開催された0ctf Qualsに参戦しました。

唯一解いたbabyrsa (crypto)のWriteupを残します。


babyrsa (crypto)

問題文

RSA challs are always easy, right? Even if N is not a integer.

暗号化関数(rsa.sage)はこちら。

#!/usr/bin/env sage
# coding=utf-8

from pubkey import P, n, e
from secret import flag
from os import urandom

R.<a> = GF(2^2049)

def encrypt(m):
    global n
    assert len(m) <= 256
    m_int = Integer(m.encode('hex'), 16)
    m_poly = P(R.fetch_int(m_int))
    c_poly = pow(m_poly, e, n)
    c_int = R(c_poly).integer_representation()
    c = format(c_int, '0256x').decode('hex')
    return c

if __name__ == '__main__':
    ptext = flag + os.urandom(256-len(flag))
    ctext = encrypt(ptext)
    with open('flag.enc', 'wb') as f:
        f.write(ctext)

RSA多項式環にも適用可能なことを使った問題のようです。 スクリプトsagemathを使ってますね。

アプローチ

元ネタは、学位論文(何…だと!!)の

Polynomial based RSA http://www.diva-portal.se/smash/get/diva2:823505/FULLTEXT01.pdf

でしょうね。13ページ目ぐらいから暗号化手順が説明されているので、N(x)(プログラム中ではn)を P(x), Q(x) に因数分解できれば90%勝ちです。 あとはrsa.sageとRSAの復号手順を参考にして復号すればフラグゲットです。

ソルバー

solve.sage:

# coding=utf-8

# ■ 参考文献
# 
# ◎元ネタ
# Polynomial based RSA
# http://www.diva-portal.se/smash/get/diva2:823505/FULLTEXT01.pdf
# 
# 多項式 — Sage チュートリアル v8.6
# http://doc.sagemath.org/html/ja/tutorial/tour_polynomial.html

from sage.all import GF, PolynomialRing

with open('flag.enc', 'rb') as f:
    ctext = f.read()
c_int = Integer(ctext.encode('hex'), 16)
print(c_int)

R.<a> = GF(2^2049)

P=PolynomialRing(GF(2),'x')
e = 31337
n = P('x^2048 + x^2046 + x^2043 + x^2040 + x^2036 + x^2035 + x^2034 + x^2033 + x^2031 + x^2029 + x^2025 + x^2024 + x^2022 + x^2019 + x^2018 + x^2017 + x^2012 + x^2007 + x^2006 + x^2004 + x^2000 + x^1999 + x^1998 + x^1997 + x^1993 + x^1992 + x^1991 + x^1986 + x^1982 + x^1981 + x^1979 + x^1978 + x^1977 + x^1975 + x^1970 + x^1964 + x^1963 + x^1962 + x^1961 + x^1960 + x^1959 + x^1958 + x^1955 + x^1954 + x^1952 + x^1951 + x^1949 + x^1947 + x^1942 + x^1939 + x^1938 + x^1936 + x^1934 + x^1933 + x^1932 + x^1930 + x^1928 + x^1927 + x^1923 + x^1922 + x^1919 + x^1918 + x^1915 + x^1914 + x^1913 + x^1912 + x^1911 + x^1910 + x^1908 + x^1903 + x^1902 + x^1900 + x^1899 + x^1897 + x^1893 + x^1891 + x^1890 + x^1886 + x^1881 + x^1880 + x^1879 + x^1878 + x^1875 + x^1874 + x^1873 + x^1872 + x^1871 + x^1870 + x^1869 + x^1865 + x^1863 + x^1862 + x^1860 + x^1856 + x^1855 + x^1853 + x^1852 + x^1845 + x^1841 + x^1839 + x^1837 + x^1836 + x^1835 + x^1833 + x^1832 + x^1829 + x^1828 + x^1827 + x^1826 + x^1824 + x^1823 + x^1822 + x^1821 + x^1820 + x^1819 + x^1818 + x^1817 + x^1813 + x^1812 + x^1810 + x^1809 + x^1808 + x^1807 + x^1803 + x^1799 + x^1797 + x^1796 + x^1794 + x^1792 + x^1790 + x^1786 + x^1783 + x^1782 + x^1779 + x^1778 + x^1776 + x^1775 + x^1774 + x^1772 + x^1767 + x^1766 + x^1765 + x^1764 + x^1763 + x^1762 + x^1759 + x^1757 + x^1756 + x^1754 + x^1753 + x^1752 + x^1750 + x^1749 + x^1741 + x^1734 + x^1730 + x^1729 + x^1726 + x^1725 + x^1723 + x^1722 + x^1721 + x^1716 + x^1714 + x^1713 + x^1712 + x^1710 + x^1709 + x^1706 + x^1705 + x^1703 + x^1702 + x^1700 + x^1698 + x^1693 + x^1692 + x^1691 + x^1690 + x^1683 + x^1682 + x^1681 + x^1680 + x^1679 + x^1677 + x^1672 + x^1670 + x^1669 + x^1666 + x^1663 + x^1662 + x^1661 + x^1659 + x^1655 + x^1653 + x^1651 + x^1649 + x^1648 + x^1647 + x^1646 + x^1644 + x^1643 + x^1642 + x^1640 + x^1639 + x^1638 + x^1634 + x^1633 + x^1628 + x^1620 + x^1619 + x^1618 + x^1616 + x^1614 + x^1611 + x^1610 + x^1608 + x^1605 + x^1604 + x^1603 + x^1599 + x^1597 + x^1595 + x^1594 + x^1590 + x^1588 + x^1587 + x^1585 + x^1583 + x^1580 + x^1579 + x^1577 + x^1574 + x^1573 + x^1572 + x^1568 + x^1566 + x^1565 + x^1563 + x^1562 + x^1560 + x^1555 + x^1554 + x^1552 + x^1550 + x^1549 + x^1548 + x^1545 + x^1544 + x^1542 + x^1540 + x^1538 + x^1537 + x^1536 + x^1535 + x^1534 + x^1533 + x^1532 + x^1531 + x^1528 + x^1526 + x^1525 + x^1523 + x^1522 + x^1521 + x^1519 + x^1517 + x^1515 + x^1510 + x^1509 + x^1506 + x^1504 + x^1502 + x^1499 + x^1498 + x^1497 + x^1488 + x^1483 + x^1480 + x^1477 + x^1472 + x^1471 + x^1469 + x^1468 + x^1467 + x^1466 + x^1464 + x^1462 + x^1457 + x^1456 + x^1455 + x^1454 + x^1453 + x^1452 + x^1448 + x^1446 + x^1444 + x^1443 + x^1442 + x^1441 + x^1440 + x^1436 + x^1435 + x^1431 + x^1428 + x^1425 + x^1424 + x^1422 + x^1420 + x^1415 + x^1414 + x^1411 + x^1410 + x^1408 + x^1406 + x^1405 + x^1403 + x^1402 + x^1399 + x^1397 + x^1396 + x^1395 + x^1394 + x^1393 + x^1391 + x^1388 + x^1385 + x^1377 + x^1376 + x^1372 + x^1371 + x^1370 + x^1369 + x^1367 + x^1363 + x^1361 + x^1357 + x^1355 + x^1354 + x^1349 + x^1343 + x^1339 + x^1338 + x^1337 + x^1336 + x^1335 + x^1332 + x^1329 + x^1327 + x^1326 + x^1324 + x^1321 + x^1315 + x^1314 + x^1312 + x^1310 + x^1309 + x^1305 + x^1304 + x^1303 + x^1302 + x^1299 + x^1298 + x^1296 + x^1295 + x^1293 + x^1291 + x^1290 + x^1289 + x^1284 + x^1283 + x^1282 + x^1281 + x^1280 + x^1278 + x^1277 + x^1276 + x^1275 + x^1272 + x^1270 + x^1269 + x^1268 + x^1267 + x^1259 + x^1257 + x^1254 + x^1252 + x^1251 + x^1249 + x^1247 + x^1246 + x^1244 + x^1240 + x^1238 + x^1233 + x^1232 + x^1229 + x^1222 + x^1219 + x^1217 + x^1211 + x^1209 + x^1208 + x^1205 + x^1204 + x^1203 + x^1202 + x^1200 + x^1197 + x^1196 + x^1195 + x^1193 + x^1192 + x^1189 + x^1187 + x^1186 + x^1185 + x^1184 + x^1183 + x^1182 + x^1181 + x^1177 + x^1176 + x^1173 + x^1170 + x^1167 + x^1166 + x^1162 + x^1161 + x^1160 + x^1159 + x^1158 + x^1156 + x^1155 + x^1154 + x^1153 + x^1151 + x^1146 + x^1143 + x^1141 + x^1139 + x^1138 + x^1137 + x^1135 + x^1131 + x^1129 + x^1128 + x^1125 + x^1124 + x^1122 + x^1116 + x^1115 + x^1114 + x^1112 + x^1111 + x^1107 + x^1106 + x^1105 + x^1104 + x^1103 + x^1102 + x^1098 + x^1097 + x^1095 + x^1094 + x^1092 + x^1088 + x^1087 + x^1085 + x^1077 + x^1076 + x^1075 + x^1072 + x^1069 + x^1068 + x^1061 + x^1060 + x^1059 + x^1057 + x^1055 + x^1054 + x^1053 + x^1050 + x^1047 + x^1046 + x^1044 + x^1043 + x^1042 + x^1036 + x^1029 + x^1025 + x^1024 + x^1023 + x^1022 + x^1019 + x^1016 + x^1013 + x^1012 + x^1010 + x^1008 + x^1007 + x^1006 + x^1004 + x^1000 + x^996 + x^995 + x^993 + x^992 + x^989 + x^985 + x^983 + x^978 + x^977 + x^975 + x^972 + x^971 + x^970 + x^969 + x^967 + x^963 + x^957 + x^956 + x^952 + x^950 + x^948 + x^945 + x^942 + x^941 + x^940 + x^938 + x^937 + x^936 + x^935 + x^932 + x^931 + x^930 + x^928 + x^927 + x^926 + x^923 + x^921 + x^918 + x^916 + x^914 + x^913 + x^909 + x^906 + x^905 + x^904 + x^902 + x^897 + x^895 + x^892 + x^889 + x^888 + x^887 + x^886 + x^885 + x^884 + x^882 + x^881 + x^879 + x^876 + x^870 + x^868 + x^867 + x^865 + x^862 + x^861 + x^859 + x^858 + x^856 + x^854 + x^848 + x^847 + x^846 + x^843 + x^839 + x^837 + x^836 + x^832 + x^831 + x^830 + x^829 + x^826 + x^823 + x^821 + x^820 + x^817 + x^815 + x^812 + x^809 + x^808 + x^805 + x^803 + x^802 + x^800 + x^799 + x^797 + x^795 + x^793 + x^792 + x^788 + x^786 + x^784 + x^780 + x^775 + x^774 + x^770 + x^768 + x^766 + x^764 + x^761 + x^760 + x^753 + x^752 + x^751 + x^750 + x^747 + x^744 + x^742 + x^741 + x^737 + x^734 + x^732 + x^728 + x^727 + x^724 + x^722 + x^721 + x^719 + x^717 + x^715 + x^714 + x^713 + x^710 + x^709 + x^705 + x^703 + x^701 + x^698 + x^697 + x^695 + x^690 + x^687 + x^685 + x^684 + x^682 + x^681 + x^680 + x^677 + x^676 + x^674 + x^673 + x^672 + x^671 + x^670 + x^669 + x^665 + x^663 + x^659 + x^652 + x^651 + x^650 + x^649 + x^648 + x^647 + x^646 + x^645 + x^642 + x^640 + x^638 + x^632 + x^631 + x^630 + x^629 + x^627 + x^626 + x^623 + x^622 + x^621 + x^620 + x^616 + x^615 + x^610 + x^605 + x^602 + x^601 + x^600 + x^599 + x^598 + x^596 + x^594 + x^593 + x^591 + x^583 + x^581 + x^579 + x^578 + x^577 + x^576 + x^575 + x^573 + x^572 + x^571 + x^570 + x^569 + x^565 + x^563 + x^562 + x^561 + x^559 + x^557 + x^555 + x^552 + x^551 + x^546 + x^544 + x^542 + x^541 + x^540 + x^539 + x^538 + x^537 + x^535 + x^533 + x^530 + x^527 + x^523 + x^522 + x^520 + x^519 + x^515 + x^513 + x^511 + x^509 + x^507 + x^505 + x^504 + x^503 + x^499 + x^497 + x^496 + x^495 + x^493 + x^492 + x^488 + x^486 + x^481 + x^480 + x^479 + x^478 + x^477 + x^472 + x^470 + x^468 + x^467 + x^464 + x^463 + x^460 + x^459 + x^455 + x^454 + x^453 + x^446 + x^445 + x^444 + x^443 + x^440 + x^438 + x^437 + x^432 + x^431 + x^428 + x^427 + x^426 + x^420 + x^419 + x^416 + x^415 + x^414 + x^413 + x^412 + x^411 + x^405 + x^404 + x^401 + x^396 + x^393 + x^392 + x^391 + x^388 + x^387 + x^383 + x^381 + x^380 + x^377 + x^376 + x^369 + x^364 + x^362 + x^358 + x^357 + x^356 + x^355 + x^353 + x^351 + x^349 + x^340 + x^339 + x^338 + x^337 + x^336 + x^335 + x^334 + x^332 + x^330 + x^328 + x^327 + x^326 + x^324 + x^320 + x^318 + x^316 + x^315 + x^309 + x^302 + x^298 + x^292 + x^291 + x^290 + x^289 + x^287 + x^286 + x^285 + x^284 + x^281 + x^279 + x^278 + x^276 + x^274 + x^273 + x^272 + x^271 + x^267 + x^266 + x^264 + x^263 + x^262 + x^260 + x^259 + x^256 + x^254 + x^253 + x^252 + x^251 + x^249 + x^248 + x^247 + x^245 + x^244 + x^241 + x^239 + x^235 + x^234 + x^233 + x^232 + x^231 + x^230 + x^226 + x^224 + x^221 + x^219 + x^218 + x^216 + x^215 + x^214 + x^209 + x^207 + x^206 + x^202 + x^201 + x^198 + x^197 + x^194 + x^193 + x^192 + x^191 + x^189 + x^188 + x^183 + x^182 + x^181 + x^180 + x^179 + x^178 + x^177 + x^175 + x^172 + x^169 + x^168 + x^166 + x^165 + x^164 + x^163 + x^158 + x^157 + x^153 + x^152 + x^149 + x^147 + x^146 + x^144 + x^140 + x^139 + x^136 + x^128 + x^127 + x^126 + x^124 + x^123 + x^122 + x^121 + x^116 + x^115 + x^113 + x^112 + x^109 + x^108 + x^107 + x^106 + x^104 + x^103 + x^102 + x^101 + x^100 + x^99 + x^97 + x^95 + x^94 + x^93 + x^92 + x^87 + x^84 + x^83 + x^82 + x^80 + x^79 + x^78 + x^76 + x^73 + x^70 + x^69 + x^68 + x^67 + x^66 + x^65 + x^63 + x^60 + x^59 + x^57 + x^55 + x^52 + x^51 + x^47 + x^46 + x^45 + x^43 + x^42 + x^40 + x^36 + x^35 + x^30 + x^29 + x^28 + x^27 + x^23 + x^20 + x^17 + x^14 + x^9 + x^7 + x^3 + 1')
f = n.factor()
# print(f)
p = list(f)[0][0]
q = list(f)[1][0]
# print(p, q)
s = (pow(2, q.degree()) - 1) * (pow(2, p.degree()) - 1) # 2はPの位数
# print(s)
_, _, d = xgcd(s, e)
if d < 0: d += s
print(d)

c_poly = P(R.fetch_int(c_int))
m_poly = pow(c_poly, d, n)
m_int = R(m_poly).integer_representation()
m = format(m_int, '0256x').decode('hex')

print("====")
print(m)

フラグ

あとはソルバーを動かして、

$ sage solve.sage 
sys:1: RuntimeWarning: not adding directory '' to sys.path since it's writable by an untrusted group.
Untrusted users could put files in this directory which might then be imported by your Python code. As a general precaution from similar exploits, you should not execute Python code from this directory
23931938409134006846469410550487073743925192650755116938225541794524723083910240603620279453298714584321800170326063144616472531553643627071552202613402950579120189960424183462876292590831564884347025119938858471788053191321980663696621632084753893732784657023312407591768406322125753947265987815937165961039424015628319982913336402297718720925447102042668906173729998301139577468193468132305331072754842771657432484688590927575895743853584931297836925498250475231655832566787366689988158399203844420168837827423836936015638932385609040452870954522482255864355639427304567768665723098741671323173831781775755570779256
28371355076358206651880108899447906576372266284154280282347957145120170645734899523334978078067679493874344060469168599875633378810644150054152285167807343298071802254581411860744158353096011714907819564399402714709858337654437633205741705120012058022068404602368525225166892620782231104596296684392603977673442420869964883518757302131139464582403543008517510576759631853686083804876647805871645437996963908242523987920166730933950556409136138395339773872530985876082852299816804207673785130661047844641798164979597836577807048385040982943227701240014693785196556609759136982566512240594608088626862145862029373010104

grepして、

flag{P1ea5e_k33p_N_as_A_inTegeR~~~~~~}

はい終了。プログラミングが久々で午後丸々溶けましたorz。

情報科学若手の会冬の陣2019 で登壇しました

2019/01/20(日) に開催された情報科学若手の会冬の陣2019 #wakate2019w に登壇しました。

wakate.connpass.com

情報科学若手の会は、シンポジウムの要領で毎年秋頃に2泊3日の合宿する会のようですが、まだ参加したことがありません。 今回の冬の陣はその非公式出張版のような立ち位置のようです。 話すネタはあり、参加者を見ると話が通じそうな人がちらほらいそうだったので、友利奈緒のコスプレをしつつ登壇してみました。 コスプレをしても会場にいる人達は反応しないのがデフォになってきました。

発表内容は相も変わらずシンボリック実行に関するものです。2018年5月ごろにWeakest Preconditionを用いるシンボリック実行(Symbolic Backward Execution)があることを知り、実装してみたいとは思っていました。 2018年春の Kernel/VM探検隊 に登壇したときに、ntddk先生にBackwardを実装して欲しいみたいな言われ方をしたのも理由の一つです。 表紙のキャラはオリキャラの二木双葉ちゃんです。登壇前日に夜更かしして描きました。

speakerdeck.com

質疑応答&フィードバック:

  • SBEのユースケースは?→特定地点に至るパスの解析が得意なことから、例えばマルウェアのシェルコード解析に役立つと思う。
  • CFGの解析は2018の若手の会でだでぃこさんが言ってたLLVMのやつが良さそう。
  • PythonのSBEのフルサポートが大変そう→オブジェクトなど動的生成が多いものはトラックが大変かも。今回はプログラミング言語に最低限必要なコード(四則演算、代入、関数)をサポートするSBEはエンジンを実装するモチベーションでやってるので、Pythonのフルサポートは求めない。
  • コンパイラに興味があり、Weakest Preconditionの計算により最適化できると嬉しいと思った。

keenさん、質問タイムとそれ以外でたくさんフィードバックありがとうございました。発表した後に個人的に接触してもらえるのは嬉しいです。

冒頭で、写真撮影と公開OK、って言えば良かったです。

SBEの今後の展開として、コンパイル時セキュリティ検査なんてのも面白いかも知れませんね。潜在的なDouble Free脆弱性があるとか。

聴講した感想

その1)やっていき

@mkt_kwnさん(慶応大の博士課程の方)がスマートシティのために一つの市を巻き込んでいたり、ぱろっくくん(セキュキャン2015年の同期)が会社を立ち上げしてたりして、作りたい世界のためにでかいアクションを取っていて刺激を受けました。私も作りたい世界があるのでやっていくしかないですね~(時期が来たらまた話します)。

その2)コスプレはネタTシャツに勝る

その3)サイバーエージェントの人事

@masagotty さん(ゴッティさん)から圧がすごい発表。熱血本がセキュリティ界隈だと有名なのは知っていますが、普通のエンジニアも手にとっていたとは知りませんでした…(私はKindle版を持っています)。

会社が、エンジニアが楽しく働けることをケアしてくれるのは大事なファクターなので、就活中の学生エンジニアの皆さん、ちゃんと見定めてくださいね。(現職はこの前提が成り立って無くて、しんどいよー。)

UnityCamをビルドしようとしたら __imp__snprintf エラーでビルドできなかった

UnityCamをVisual Studioでビルドしようとしたら、

LNK2001 外部シンボル "impvsnwprintf" は未解決です。

というエラーが出た。

以下対処方法。

  1. Visual Studioのソースツリーにある、UnityCamServiceプロジェクトを右クリックして、「プロパティ」をクリック
  2. 「リンカ▶入力」タブを開き、「追加の依存ファイル」欄に「;legacy_stdio_definitions.lib」を追加。

f:id:katc:20180813144314p:plain

なお、ソースツリー内のソリューションを右クリックして現れる「ソリューションの再ターゲット」は済ませてある。

参考資料