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

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

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

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

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

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

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

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

背景

• 制約導出の困難さ
• 一般に目的の状態（本論文では特定箇所の脆弱性）が発現する地点に到達するのが難しい
• 例）複雑なループ
• 友利注：ループがn個あり1個のループが高々m回で抜けられるならば、状態数は 。基本無理ゲー
• 要はパス爆発（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) メモリ使用量が上限値に到達
• ニューロンモードでは入力は具体値。制約をニューラルネットワークで内包し、制約を満たす入力 （実行対象への入力）と出力 （制約式で拘束された変数）の組を学習する。
• 友利注：クラス分類問題ではない。あくまで関数 の表現方法を学習するだけ（回帰問題）。
• (2) シンボリック制約を多層パーセプトロンにより近似解で求める
• シンボリック制約は誤差関数に変換される
• 解の導出方法はニューロンモードで述べたとおり。

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

アプローチ詳細

Neural Modeの構成

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

Neural-symbolic制約の充足

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

SymSolv

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

NeuSolv

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

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

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

• 制約を充足するまでは が非ゼロ
• 下限が存在
• でないと探索が停止しない
• 友利注： 関数 について、 ロス関数の性質から、以下を満たす はCVPの制約を満たす。  （これは論文の式(5)） とすると、 ここで連鎖律により、 (*1)

であることに注意すると、  の定義（Table II）から導出可能であり、また であるから、 は計算可能。

(*1) ヤコビ行列

（本当にこれで合ってるのだろうか？ の計算方法の説明がどこにも無かったし…）

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

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

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

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

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

（友利注：書くの飽きてきた…。方針としては、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の探索モード）と比較するのは必須。

実験条件

• 機械学習フレームワークはTensorFlowを採用した。
• 活性化関数 は正規化線形関数（ReLU） を採用した。
• マシンは40-core 2.6GHz 64GB RAM Intel Xeon machine。

(a) KLEEに対する効率性

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

(b) Neural Modeの効用

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

(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％増加した。

所感

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  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はシンボリック実行に依存していないように見える。 を得られれば適用可能に見える。 はランタイムで得られ、 はCVPを元に機械的に計算可能。 ならシンボリック実行だけでなくファジングでも適用できるのでは？

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

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

まず多層パーセプトロンのネットワーク構成について復習する。  のように計算される。ここで、 は重み、 はバイアスとよばれ、 をこれらのパラメータすべてを成分に持つベクトルとする。

ネットワークの最終出力  と得る。

ネットワークのパラメータ の調整には を用いる。ここで をエポック、 を誤差関数とする。

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

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

Verilog編

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] をクリック。

Lチカコード

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

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

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

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
}

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

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

Implementationできなくて詰んだ。ナニコレ🤔 🤔 🤔 [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旅団 - BOOTH

はじめに

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

0ctf 2019 Quals の babyrsa (crypto) の Writeup

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

babyrsa (crypto)

問題文

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

#!/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を使ってますね。

アプローチ

でしょうね。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:
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)
q = list(f)
# 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 に登壇しました。

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

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

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

聴講した感想

その１）やっていき

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

その３）サイバーエージェントの人事

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