更新日時で差をつけろ

もはや更新日時でしか差を付けられない

3/14

円周率の日。さすがにあんまり思い出せなくなってきた…
言語学オリンピック一次予選を通過したとの連絡が入った。とりあえずうれしい。一安心。
CombKansaiには行けないけどね。

昼から誘われて NACLOの過去問 を解いたが歯が立たなかった。
せめてWikipediaぐらいは読んで悪あがきをしようと思う。春休みの思い出〜

LSE CTF ではxPlatformとReduced Instruction Set Crackmeを解いた。両方ともSolved 27。
MIPSアセンブリがちょっとだけ読めるようになった。
常設CTFはwrite-upを書いてアウトプットできないのがツライ。

今日はルーター実装とか他のことを一切していない…rev始めると気になってやめられないんだなあ…

3/7

記号論理の本難しいけど、ちょくちょくCNFとか知ってる単語が出てきてモチベーションは維持されてる。ただ最終的に何が学べるかは未知数…SATソルバでどうこうするときに活きるとうれしいな〜程度で。

自作x86エミュの本はいよいよ、というよりもう最終章に入った。BIOSってカーネルを読むだけじゃないんだな、もっと知りたくなってきた。実機で動かすって書いてあるけれど、ブートローダがぐちゃぐちゃになってるこのMacで動くのか心配。 ModR/Mもだいぶわかるようになってきた。本が終わったらいろいろバイナリを与えてみてNot implementedな場所を埋めていきたい。

ルーター自作本はElixirでやるかCでやるか迷っていたが、いろいろ調べた末rawソケットの扱いが不安なので内容通りC言語で書いてみることにした。さらに、Twitterでpcapインターフェースというものの存在を教えてもらったので本を1周できたら使ってみたい。

「リンカ・ローダ実践開発テクニック」も読み始めた。BIOSの話はコッチにも少しだけ書いてある。ELFはCTFで使うので理解していたつもりだったけど、別の視点から見ると知らないことだらけだった。

熱の冷めないうちに進めてしまいたい。

3/6

x86エミュレータ本を今日も進めた。addとかpushとか実装してだんだん形になってきて楽しい。ModR/Mがちょっとややこしい。
(Elixirで)300行程度なのでまだまだわかる。
rm32r32をどこかで見たことがあると感じたが、pwnの最中にアセンブリの命令を調べているときにページに載っていたものだった。なるほど。

「バイナリで遊ぼう!」本を最後まで読み切った。
アセンブリ短歌をやってみようとした。が、自分でアセンブリを手打ちしたことがないので手が動かない…「Cで書いてアセンブルして読む」というのをやっぱりまずはやるべきなのかな。基礎。

Pony という言語を見つけた。アクターモデル?を採用していて、データロックという概念が存在しなかったりするらしい。マイナーかと思えばGitHubリポジトリには結構starがついている。楽しそう。

群論本はちょっと難しくなってきてあんまり進めなかった。

3/5

午前中はAtCoder Omedesを作っていた。Elixirのリハビリ。コンテストごとにレート色が上がった人を祝福してくれます。
午後からはx86エミュレータをElixirで作っていった。条件分岐をif-elseでやるか、ガードでやるか、もしくはループをEnumで実現するかパターンマッチ+再帰で書くか迷う。
HTTPoisonなどを読んでみるべきだろうか。コードリーディングは若干苦手だが…
The BEAM Bookというのもあるみたい。

群論なんかこわくない」「バイナリで遊ぼう」も100ページ弱まで進んだ。
アーベル群とか部分群とか出てきて本格的になってきた。
アセンブリ短歌が想像以上に面白い。でも自分では思いつかないなぁ…

本を読むのは楽しいけど、ちゃんと身につけるようにしたい。どうやったらいいのかわからないからとりあえず手を動かすようにはしている。
pwnもcryptoも最近してないしそれに関して言えばよくない。もっと集中してスピード上げたい。

IOLは書類をやっとポストに入れてきた。通るかな?

3/4

朝メールをチェックすると情報処理学会から電子図書館の案内が来ていたので見てみた。「認証基盤」とかいう堅苦しいページでログインして学会誌を開こうとするもロードが遅い遅い。どういうことなんだろう…

最新版のを見ると「LSI配線問題」というものについての特集があった。いかにうまくマス上に回路を配置するか、というものらしい。なんとなく制約充足問題っぽいな〜と思ってたらその通りで、SATソルバを使って解いていた。他にも機械学習や0-1整数計画法というものを使った解き方が紹介されていた。

3年分ぐらいの学会誌を漁ってみるとファイルシステムとかディジタルゲリマンダについての特集があり、ためになりそうなのでダウンロードした。ぼちぼち読んでいきたい。
論文も一部公開されているので見てみたけど、やっぱり難しく書かれててサクッと読むものではないと感じた。

「バイナリで遊ぼう!」を50ページぐらい読んだ。とはいってもプログラムを書くわけではないのでそんなに時間はかけていない。「バイナリ体操」を日々の生活に取り入れて健康なバイナリアンを目指します。
tarが無圧縮のフォーマットであるというのを今更知った。いや以前どこかで見たはずなんだけど忘れたんだよなあ。

群論なんかこわくない」もわずかに進めた。反復しながら読んでいくのが安全っぽい。

「自作エミュレータで学ぶx86アーキテクチャ」を読み始めた。親切なことにC言語でのソースコードが別途配布されている。が、それを動かすだけでは勉強にならない(かつ自己満足ができない)のでElixirなどで真似して書いてみることにした。
Elixirで書かれたエミュレータは他にもあるみたいだし、多分大丈夫。

IOLの書類を書き上げた。結構手こずった…
TOEICは単語音読に1時間半かけるよりリスニングをなんとかしたほうが良いと感じたので比率を調整した。英検1級の過去問を使ってやっていきたい。
フォロワーの人に THC CTF というのを紹介してもらったので一緒に出ることにした。楽しみ。

3/3: 閉寮

閉寮なので家に帰った。1ヶ月後には後輩ができるのか…
久しぶりに浴槽に浸かれた。素晴らしい。

なんとなく図書館に行った。x86エミュレータの本が目当てだったけど他にもいろいろ面白そうなのでついつい8冊借りてしまった…
割と薄めの本ばっかりだしルータ本と線形代数本とTOEICあってもなんとかなるでしょ!w

  • 自作エミュレータで学ぶx86アーキテクチャ Twitterでおすすめされているのを見た。著者の人すごい…。個人的に表紙にキャラクター載ってるとちょっとアレ。かわいいとはいえ。
  • 群論なんかこわくない 対話形式で進める群論の入門の本。適当に数学書の棚に行ったらあった。すでに60ページほど読んだ。
  • APIデザイン ケーススタディ Rubyのメソッドを作る際に考えられたことをコミッタの人が書いてる
  • リンカ・ローダ 実践開発テクニック 半年前だったらまず手に取らなかったであろう本。というか全部そう。実際にリンカを作るので楽しそう。
  • ソーシャル・エンジニアリング コミュ力を身に着けたい(誤った動機
  • バイナリで遊ぼう! どこかでおすすめされてた本。俳人になりてえ
  • Linuxカーネルソースコード」を読み解く たまたま見かけたので。ブートプロセスを取り上げた本もあったけどちょっと難しそうなのでこっちで慣れることにした。
  • インターネットフォレンジック 某氏に影響されて借りた。実例が載っているので良い。
  • 学んでみよう! 記号論 SAT/SMTソルバがここしばらくマイブームで、目次にCNFという文言があったので借りた。ポップなタイトルと表紙とは裏腹に中身はガチっぽい。

他にもシェル芸でCMSを作る本とか大じゃない方の熱血アセンブラ入門とかあったけど量が量なので見送り。

EasyCTF IV の MalDropper を解きたくてC#のデコンパイラを入れたいのにILSpyが動いてくれない。困った...

IOLの1次予選はとりあえず感想を紙に書き写して、解法も半分ぐらい書き終わった。これで伝わるといいんだけれど。
「1000字も書けねえ〜」とか言ってる割にはこの日記は1000字ぐらいあるんだよな。

Chocolate Cookie 解説

バレンタインの直前に思いついたので、チョコレートのパッケージに混入させてURL渡したりTwitterに投げてみたりしたんですが結局誰も解けなかった・解かなかったみたいです…難易度が高すぎただけなのか、はたまたエスパーだったのか…

問題

http://o0i.es/chocolate に置いてあります。

想定解法

開発者ツールなどでページのHTMLを見てみます。
まず<div id='message'>があり、<input type='checkbox'> が7x7のマスを構成しています。
その後に<span> が大量に配置されています。そしてその間に{が1つ配置されています。
checkboxをオンにすると色が濃くなってチョコチップっぽくなります。
適当にオンオフしていくと下の文字が変化したりしなかったりします。

しかし、ここには<script>が見当たりません。どのようにして<span>の文字を変えているのでしょうか?また、Here's a chocolate cookie...という文字列もHTMLファイルには記述されていません。どこから来ているのでしょうか?

ページタイトルに「CSS: Chocolate Sugoku Suki」とあることですし、CSSを見てみましょう。
style.cssrules.cssを読み込んでいるようです。

まずは前者から。先頭にいきなりFLAGの形式が書かれています。FLAG{s.........}ですね。
<div id='message'>の内容もここから来ています。
CSS--name: valueの形で変数を作ることができます。他のプロパティで参照するときはvar(--name)のようにして参照します。#0099ffなどだいたい何でも入れられます。

:root {
  --message: "Here's a chocolate cookie for you, find FLAG" /* FLAG{s.................} */ "!";
  --cacao: "C";
  --ushio: "h";
  --banana: "1";
}
 
...
 
#message::after {
  content: var(--message); 
}

続きを見てみましょう。

span:first-of-type::after {
  content: counter(f, upper-alpha);
}
 
span:first-of-type+*::after {
  content: counter(v, upper-alpha);
}
 
span:first-of-type+*+*::after {
  content: counter(j, upper-alpha);
}
 
span:first-of-type+*+*+*::after {
  content: counter(y, upper-alpha);
}
 
...
 
span:first-of-type+*+*+*+*+*+*+*+*+*+*+*+*+*+*+*+*+*+*::after {
  content: counter(e, lower-alpha) var(--banana);
}
 
...
 
span:first-of-type+*+*+*+*+*+*+*+*+*+*+*+*+*+*+*+*+*+*+*+*+*::after {
  content: '}';
}

span:first-of-typeでページ内の一番最初の<span>を選択し、隣接セレクタ+とユニバーサルセレクタ*を組み合わせて次の要素を取っています。
span:first-of-typeなら1番目、span:first-of-type+*なら2番目、span:first-of-type+*+*なら3番目…という感じです。
そしてそれの::after疑似要素・contentプロパティを使って何らかの文字を表示しています。実際に表示される文字はここで決定されるようです。

通常はcontent: "new!";のように文字列を使用することが多いですが、ここではcounter()を用いています。カウンタは、主に<li>でリスト表記をするときに番号を自動で割り振るために使われるものです。MDNが詳しいです。
デモも置いておきます。

たとえば1番目ではfカウンタの数値をupper-alpha、つまりアルファベットの大文字にして表示しています。何も指定しない場合は数字が出力されます。
途中でvar()を使ってはじめに定義した変数を表示している部分もあります。

これらを読んでいくと、<span>で表示されるそれぞれの文字は以下のカウンタの値と固定値で出来上がることになります。'で囲っているのが固定値です。

f v j y '{'(spanの間) g q(数値) h n l k(数値) c 'h'(--ushio) i o r 'C'(--cacao) p t d e '1'(--banana) s u(数値) '}'

fvjy{g.....}のカウンタの値を先程のFLAG{s......}と対応させることができればFLAGがわかるということです。

ゴールがわかったので、次にrules.cssを見てみましょう。
似たようなコードが繰り返されています。

input:nth-of-type(3):checked ~
input:nth-of-type(8):not(:checked) ~
input:nth-of-type(34):checked {
  counter-increment: h 3 g 1 r 3 f 1 k 2;
}
 
...

input:nth-of-type(N)でN番目のcheckboxを選択し、それぞれがON(:checked)かOFFかでスタイル(もはやスタイルではない)を適用するか決めています。
~はその要素以降の兄弟要素に対して適用されます。

この場合だと、「ONになっている3番目のcheckbox」の後ろに「OFFになっている8番目のcheckbox」があり、さらに後に「ONになっている34番目のcheckbox」がある場合に適用されます。
つまり、「3番目がON」かつ「8番目がOFF」かつ「34番目がON」ならば適用するという意味だとわかります(以降これをルールと呼びます)。

counter-incrementはその名の通りカウンタをインクリメントするのですが、後ろに数値を指定することで増加数を自由に変えられます。ここではh += 3, g += 1, r += 3, f += 1, k += 2という感じです(カウンタの中身はあくまで数値で、表示するときにアルファベットにしているだけです)。
試しに問題ページで3,8,34番目を操作してみると変化がわかりやすいと思います。

このrules.cssのすべてのルールに合うようにすればFLAGが出てくるのでしょうか?

…答えはNOです。
もういくつか見てみると以下のinput:nth-of-type(2)のように、互いに矛盾しているルールがあります。FLAG{sという文字列にするために使うルールと使わないルールがあり、その組み合わせを求める必要があります。

input:nth-of-type(2):not(:checked) ~
input:nth-of-type(39):checked ~
input:nth-of-type(44):not(:checked) {
  counter-increment: n 3 s 3 f 1 d 3;
}
 
input:nth-of-type(2):checked ~
input:nth-of-type(6):checked ~
input:nth-of-type(16):not(:checked) {
  counter-increment: p 2 f 1 k 2 j 3;
}

でもどうやって求めるのでしょうか?
全探索? O(249) = 562949953421312通りなので厳しいですね。

制約充足問題 で検索してみましょう! wikipediaを引用します。

制約充足問題(せいやくじゅうそくもんだい、英: Constraint satisfaction problem, CSP)は、複数の制約条件を満たすオブジェクトや状態を見つけるという数学の問題を指す

これの例としてよく挙げられるのは数独です。それぞれのマスを変数として、「ヨコの行・タテの列・3x3の正方形に1~9を1回ずつしか使えない」という制約を満たすような数字の入れ方を求める制約充足問題になります。
この数字を求める、つまり問題を解いてくれるスゴイものがSAT/SMTソルバと呼ばれるものです。
代表的なSATソルバにminisatがあります。SAT ソルバー 入門 がわかりやすいのでおすすめです。

ただ、SATソルバでは真偽の制約(aがtrue, bがfalse, かつcがfalse…)しか扱えないので直接扱うには大変な場合があります。対してSMTソルバは内部でSATソルバを呼び出しますが、整数の大小・「AならばB」などを制約として扱う構文を備えているのでSATよりもシンプルに書くことができます。
パズルをSugar制約ソルバーで解く も見てみると雰囲気がつかめると思います。

さて、それではこの問題にはどのような制約があるでしょうか?

  • 3つすべてのcheckboxが条件を満たしてはじめて、ルールが有効になり、それに応じてそれぞれのカウンタに加算する
    • 逆に、「ルールを使わないときは加算しない」「ルールで指定されていないカウンタには加算しない」(見落としがちです)
  • f v j y gカウンタの値はそれぞれF L A G sに対応する数値になる

この2つです。
1番目の制約は、たとえば以下のルールがあったとき

 input:nth-of-type(2):not(:checked) ~
 input:nth-of-type(39):checked ~
 input:nth-of-type(44):not(:checked) {
   counter-increment: n 3 s 3 f 1 d 3;
 }

このように変換できます(擬似コードです)。

rule_satisfied ← not(input[2]) and input[39] and not(input[44])
if rule_satisfied then n += 3, s += 3, f += 1, d += 3, (それ以外) += 0
if not rule_satisfied then (すべてのカウンタ) += 0

…と言いたいところですが、SMTソルバはtrue/falseで表現される制約を解くためのものなので、n += 3のように「変数に逐次値を足していってから比較する」ということができません。私もここで詰まり2日ほど考えた末「あとから全部まとめて和をとって比較する」ようにすればうまくいくことに気づきました。

具体的には以下のようにルールごとの増分を記録する配列を作り、制約をかけます(普通の代入とそっくりです)。

rule_satisfied ← not(input[2]) and input[39] and not(input[44])
if rule_satisfied then
  table[rule1][n] == 3, table[rule1][s] == 3, table[rule1][f] == 1, table[rule1][d] == 3,
  table[rule1][それ以外] == 0
if not rule_satisfied then table[rule1][すべてのカウンタ] == 0

そして、これを用いれば2番目の制約が表現できます。fカウンタの値はそれぞれのルールでの増分の和になるので、table[rule1][f] + table[rule2][f] + table[rule3][f] ... table[ruleN][f]として表現できます。

table[rule1][f] + table[rule2][f] + table[rule3][f] ... table[ruleN][f] == 'F'
table[rule1][v] + table[rule2][v] + table[rule3][v] ... table[ruleN][v] == 'L'
table[rule1][j] + table[rule2][j] + table[rule3][j] ... table[ruleN][j] == 'A'
table[rule1][y] + table[rule2][y] + table[rule3][y] ... table[ruleN][y] == 'G'
table[rule1][g] + table[rule2][g] + table[rule3][g] ... table[ruleN][g] == 's'

あとはこの2つをプログラムに落とし込むだけです!
私はz3というSMTソルバを使って解きました。GitHubにRubyでのコード例を載せています(あんまりきれいじゃないね…)。

実行するとFLAG{sという文字が現れるようなルールの組み合わせと、それらを満たすcheckboxのオンオフ、計算されたFLAGが出力されます。
実際のページでやってみると…うまくできました! FLAG{s0rry4Ch3apCh0co1at3}がFLAGです。

その他

  • 最初のバージョンではルールの数が20しかなく、O(220)で組み合わせるルールの全探索が可能でした
  • ルールを増やしたところ解が複数になってしまい削減できなかったため苦肉の策としてFLAGの1文字目を指定しました
    • これのせいで全探索の計算量減っちゃうかも?誰かおしえて
  • Xmas Contest 2017 I問題を解くために調べているときに思いつきました
  • CSSはチューリング完全