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

PlaidCTF writeup

negainoidoというチーム名で2人で参加してました。
順位は912ptsで53位でした。チームで解いた問題は以下のとおりです。

  • sanity check (Misc 1)
  • echo (Web 200)
  • zipper (Misc 50)
  • logarithms are hard (Misc 10)
  • no_mo_flo (Rev 125)
  • pykemon (Web 151)
  • multicast(Crypto 175)
  • bigpicture(Pwnable 200)

私はlogarithms are hardとpykemon以外の問題を解きました。

Echo

ツイートを送ると、それらのツイートを読み上げた音声ファイルが生成されるウェブサービスをHackする問題。
ウェブサーバのソースは与えられるのでありがたかった。
詳細な仕様は以下のとおり
Location /

  • GETパラメータにtweet1...tweet4が入っているとその内容を改行でconcatして/tmp/{uuid}/inputに書き込む。
  • ついでにflagも伸長されて/tmp/{uuid}/inputにおいてくれる。
  • つぎに、dockerコマンドで/tmp/uuid/を/share/にマップしてpython run.pyを呼び出す。run.pyの中身はわからなかったが、実はdockerコンテナをホストするサイトを調べれば見つかったらしい。
  • その後、ffmpegを使って上のdockerコマンドによって生成した音声ファイルを/audio/{uuid}/1.wavなどに移す

exploit

与えられたウェブサーバのソース自体にはそれほど致命的な脆弱性は存在しなかったので、run.pyの中に脆弱性があるのだろうと推測した。run.pyに渡すことができるのはツイートの中身だけなので、そこに集中して色々実験したところ、OSコマンドインジェクションができることがわかった。
具体的には

tweet1=`ls`

などとするとウェブサーバのls結果を読み上げてくれた。楽しい!
フラグはdockerコマンド内からは/share/flagにあるので、アクセスはできるのだが、伸長されているためそのまま`cat /share/flag`としても長すぎて弾かれてしまう。
もとの文字列に戻すスクリプトを書かなければならないがシェル芸で行うには少々酷だったのでもうちょっと高機能な処理系を使うことにした。dockerコマンドでpythonを読んでいるのでpythonはdocker内にも存在しているはず。

tweet1=#`python /share/input`
tweet2=print('hoge')

こうすると"ハッシュ、ホージ"と言ってくれた。正しく動いているようだ。
フラグの各バイトを整数に変換して読み上げてもらった。

tweet1=#`python /share/input`
tweet2 = data = open('/share/flag','rb').read()
tweet3 = print(' '.join(map(lambda x: str(ord(x)),(reduce(lambda x,y: chr(ord(x)^ord(y)), data[65000*i:65000*(i+1)]) for i in range(0,38)))))

これでフラグを読み上げてくれる。

ここからがこの問題の一番難しいところだった。フラグの途中までの音声ファイルが残っていたので聞いてみてほしい。
soundcloud.com
聞き取れるだろうか、
私には無理だった。再生速度を遅くしたら幾つかは聞き取れるが、すぐにどこまで聞いたかわからなくなってしまう。
音声ファイルを空白で区切ってくれるツールを探してもよかったのだけれど、それはそれで面倒だったので、フラグを全部読み上げてもらうのでなく、数バイト読むスクリプトを何回もあげてちょっとずつ聞き取りをした。
flag: PCTF{Li5st3n_T0__reee_reeeeee_reee_la}*1

Zipper

zipファイルがもらえるのだけれど、そのまま展開しようとしてもエラーで上手くいかない。zipファイルの仕様を調べつつどこがおかしいのか調べた。
ZIP書庫ファイル フォーマット - 略して仮。
解析したところファイル名が入るべきところがヌルバイトになっていて、かつ、ファイル名の長さを表す変数が実際より大きい値担っていた。バイナリエディタで適切な値に直してみると展開に成功し、フラグが得られた。
flag: PCTF{f0rens1cs_yay}

no_mo_flo

バイナリファイルを解析して正しい入力を見つける問題。
radare2で大まかに解析すると以下のことがわかった。

  • 入力は32バイト
  • 入力の奇数番目のデータと偶数番目のデータをそれぞれint型の配列data1, data2に移す。
  • func1(data1) != 0 && func2(data2) != 0となれば正解

func1とfunc2の挙動を解析すればよいということがわかった。なのでそれぞれの挙動を解析した。

func1

func1の方は比較的簡単で、レジスタジャンプなどを用いてはいるが、原則的に一本道で、data1の特定の要素を読み、
それに何かしらの演算をしてから定数値と比較するコードであったので、分岐条件を一つずつ調べることで解析ができた。

func2

一方func2はややこしく、data2の特定の要素を読んで演算を行い比較するところまでは読めるのだが、その比較の結果をどう利用しているのかが複雑でよくわからなかった。
具体的には比較した後r11に分岐条件を表すと思われる定数値(1~6)を入れてその後0除算を行う。そうするとあらかじめ登録しておいたSIGFPEのシグナルハンドラが呼び出され、そこで分岐先が決定されていた。
r11の値が5の時はおそらく定数との比較で一致すれば成功だろうと推測できたが、r11が1の時の挙動はイマイチよくわからなかった。
幸いにも確定できない文字数は数文字程度だったので正しい文字列を探索することにした。各入力についてgdbでesiに格納されている成功フラグが折れる可能性のある場所全てにbreakpointを張って実行しどの地点で失敗したのかがわかるようにすると1文字だけ他の文字と挙動がことなるものがあったのでそれが正しいのだろうと推測した。
その途中でわかったが、r11が1の時は比較した定数値-1であれば正解だったようだ。
flag: PCTF{n0_fl0?_m0_like_ah_h3ll_n0}*2

multicast

RSAを破る問題。次のような暗号設定である

  • Parameters: \(a_i, b_i, n_i\) (1024 bits) (for \(i \in \{1\dots5\}\))
  • Constraints:
    • \(n_i = p q\) for some prime \(p, q\)
    • \(a_i\) and \(n_i\) are coprime
  • Plain: \(M\) ( 512 bits )
  • Encrypt: \(c_i = (a_i M + b_i)^5 \bmod n_i\)

与えられるのは\(a_i,b_i, c_i, n_i\)である、public exponentが5と小さいく5つ暗号結果がある。仮に\(c_i = M^5 \bmod n_i\)であったとすると、中国人剰余定理を用いて\(M^5 \bmod N\) (ここで\(N = n_1 * n_2 * \dots * n_5\))が計算できてあとは整数上での5乗根を取れば終わりなのだが、実際には\(c_i = (a_i * M + b_i)^5 \bmod n_i\)となっているのでそう簡単にはいかない。

結局アイディアが浮かばなかったので1日寝かせた。
日曜日にもう一度考えるとcoppersmith's attackというものが使うのではないかと予想し、
Coppersmith's attack - Wikipedia
なんとかして\(M\)を解に持つ、\(N = n_1 * \dots * n_5\)上の多項式を求めるという方向性で攻めることにした。

話を簡単にするために次数が2で2本の方程式がある場合を考えよう。
いま、n,mを互いに素な整数とし2次の2本の多項式
\begin{align}
f(X) &= a X^2 + b X + c \bmod n \\
g(X) &= d X^2 + e X + f \bmod m
\end{align}
があるとする。拡張ユークリッドの互除法により\(u n + v m = 1\)となる\(u,v\)を得る。
ここで\(h(X) = v m f(X) + u n g(X) \bmod n m\)を考える。

  • \(\pmod n\)で考えると\(h(X) = v m f(X) + u n g(X) = 1 f(X) + 0 g(X) = f(X)\)
  • \(\pmod m\)で考えると\(h(X) = v m f(X) + u n g(X) = 0 f(X) + 1 g(X) = g(X)\)

となる。\(f(X) = 0 \bmod n)\)と\(g(X) = 0 \bmod m)\)が共通解 \(Z\)を持ったとすると、
\(h(Z) = 0 \bmod n, h(Z) = 0 \bmod m\)となるので\(h(Z) = 0 \bmod {n m}\)である。すなわち、\(Z\)は\(h(X) = 0 \bmod {n m}\)の解となっている。

これを五次の場合に拡張すれば\(N = n_1 * \dots * n_5\)上の多項式で平文Mを解に持つものが得られる。そうするとcoppersmithの攻撃の適用範囲になるので解が出てくる。

parigpで多項式の計算と解の計算を行った。

gist9f1e859748b04e9fe5dd5b36561cbc05

$ gp -q doit.gp 
[48256277589562736290346738984160936248669152041168006480231762961805279486041361025591223549819869423406508417405]
$ python3
>>> from Crypto.Util import number
>>> number.long_to_bytes(48256277589562736290346738984160936248669152041168006480231762961805279486041361025591223549819869423406508417405)
b'PCTF{L1ne4r_P4dd1ng_w0nt_s4ve_Y0u_fr0m_H4s7ad!}'

bigpicture

ありがたいことにCのソースコードがあたえられる。
大きなキャンバスがあたえられてその任意の場所に文字を書き込めるというプログラム
redditの今年のapril fool企画を思い出した。
When Pixels Collide

プログラムの挙動をまとめると以下のとおり

  • 最初にキャンバスのサイズW, Hをユーザが入力する
  • buf = calloc(W, H)とする
  • そこから任意の回数scanf("%d , %d , %c", x, y, c)してptr = &buf[x * H + y]とする。
    • もし*ptrがnullでないならその文字を出力する
    • そうでないならば*ptrにcを書き込む
  • ユーザがquitと入力すると最後にbufを描画し、free(buf)を呼ぶ。

scanf("%d, %d, %c", x, y, c)した値はx < Wかつy < Hでなければならないが負の値は弾かないので、実質的に任意のアドレスを読むことができる。
バイナリはPIEかつFULL RELROなのでアドレスをleakするところから攻めなくてはならない。gdbでheapのbuf周辺に何か書いてないかと調べたが何も書いてなかった。

いろいろ試していると、大きいサイズのキャンバスを作ったときにはheapではなくてmmap領域にアロケートされることがわかった。同じくmmap領域にはlibcも配置されているので、bufからlibcへの相対アドレスは常に一定となる。
1000 x 1000のキャンバスを用意し、gdbでbufがどこにアロケートされるか調べ、libcとの相対位置を調べてそのアドレス付近にクエリを投げると、libcのデータを読むことができた。したがってlibcの任意のアドレスに相対アドレスで書き込めることがわかった。
今回ripを奪うために__free_hookのアドレスにsystemのアドレスを書き込むことにした。(最近writeupを読んだEasiestPrintfと言う問題でも似たような手法が使われていたので覚えていた)そうすると、プログラム終了時にfree(buf) -> system(buf)と呼ばれてシェルを立ち上げることができる。そのためにはsystem関数の絶対アドレスをleakする必要がある。libcどこかにlibcの配置アドレスが書いてあるはずなので適当なアドレスを探したところ_IO_2_1_stderr_+0x8あたりに書いてあるのを見つけたのでそのアドレスを使うことにした。

ところが、exploitを作ったところローカルでの実行ではうまくいくのだが、remoteだと_IO_2_1_stderr+0x8を読むはずのところで別の部分のデータが帰ってきてうまくいかなかった。どうも手元の環境とリモートの環境で配置される順番か位置が異なっているようだった。向こうの環境でどう配置されるかは簡単にはわからないので、リモートでlibcがあると思われる付近のデータを読んできて、そのバイト列がlibcのバイナリのどこにあるかを調べることでlibcの配置位置を特定した。

exploit

最終的なexploitは以下のとおり。

gist84eb1d6b403e488dd2fc54318042979a
flag: PCTF{draw_me_like_one_of_your_pwn200s}

所感

各カテゴリ一問は解けたので結構満足している。他のcrypto問は時間がなくてあまり手をつけられなかったので復習したい。logarithms are hardはググり力が低くて自分では解けなかったのが悔しい。

*1:listenのスペルがちょっと違う気がするのは気のせいだろうか。

*2:実は未確定の文字を'?'として処理していたのだが、実際にフラグに'?'の文字が入っていたのでちょっと苦労した。

BCTF2017 writeup: babyuse

今週末はBCTFに参加してました。一人で参加してpwn一問だけ解けたので記録しておきます。

問題概要

配布されたzipファイルにはバイナリbabyuseとlibc.soがもらえます。

$ unzip -l e1b84982-14dc-45f3-a41b-fb80b4805bd1.zip 
Archive:  e1b84982-14dc-45f3-a41b-fb80b4805bd1.zip
  Length     Date   Time    Name
 --------    ----   ----    ----
        0  04-10-17 13:37   babyuse/
    13712  04-10-17 13:32   babyuse/babyuse
  1786484  04-10-17 13:34   babyuse/libc.so
 --------                   -------
  1800196                   3 files

バイナリを実行すると、AAのロゴ(Passion leads Amy?)が表示され、銃を買ったり売ったりできるみたいです。

$ ./babyuse 
 _                                         
|_)_. _ _o _ ._  |  _  _. _| _  /\ ._ _    
| (_|_>_>|(_)| | |_(/_(_|(_|_> /--\| | |\/ 
                                        /  

Menu:
1. Buy a Gun
2. Select a Gun
3. List Guns
4. Rename a Gun
5. Use a Gun
6. Drop a Gun
7. Exit

解析

まず基本的な情報から確認します。バイナリは32-bit ELFでFull RELRO, Canary, NX, PIE全マシです。すごく厳しいです。

$ file babyuse/babyuse
babyuse/babyuse: ELF 32-bit LSB shared object, Intel 80386, version 1 (SYSV), dynamically linked (uses shared libs), for GNU/Linux 2.6.32, stripped
$ checksec.sh/checksec -f ./babyuse 
RELRO           STACK CANARY      NX            PIE             RPATH      RUNPATH      FORTIFY Fortified Fortifiable  FILE
Full RELRO      Canary found      NX enabled    PIE enabled     No RPATH   No RUNPATH   Yes     0               2       ./babyuse


PIEのバイナリはいままで読んだことなかったので解析に色々と苦労しました。
(callとかのアドレスはロード時に書き換えられるとか、ebxがgotセクションへのポインタになっているとか、初めて知りました。)

参考になったページ

Technovelty - PLT and GOT - the key to code sharing and dynamic libraries
ELF実行ファイルのメモリ配置はどのように決まるのか - ももいろテクノロジー

radare2を使って雰囲気でデコンパイルします。(ついでにalarmの時間を延ばすようバイナリを変更しました。)

ポイントは

  • 次のグローバル変数が存在する。
    • booleanの配列guns
    • gunの構造体のポインタを持っておくgun_data,
    • 現在選択した銃のインデックスselected_gun
  • いくつかのアクションが実行できる
    • Buy(type, n, str) : for( i = 0, i <= 3 && guns[i], i++ ); guns[i] := true; gun_data[i] = new Gun(type); gun_data[i]->name = new String(str)
    • Select(i): selected_gun := i (if guns[i] == true)
    • List(): show the list of current guns
    • Rename(i, str): if( guns[i] ) { gun_data[i]->name = new String(str); free(old_str); }
    • Use(): printf("...%s...", gun_data[selected_gun]->name)...
    • Drop(i): if(guns[i]) { free(gun_data[i]->name); free(gun_data[i]) }
  • gun構造体はmallocによってheapに置かれること。

です。入出力等でバッファオーバーランなどの脆弱性は見つかりませんでした。


gist537e607ab1fb1c8e0ad745b85f662487

脆弱性

とりあえず、セグフォらせる入力を探します。銃を持っていない状態で5. Use a Gunを選択したらどうなるでしょうか。

$ ./babyuse 
 _                                         
|_)_. _ _o _ ._  |  _  _. _| _  /\ ._ _    
| (_|_>_>|(_)| | |_(/_(_|(_|_> /--\| | |\/ 
                                        /  

Menu:
1. Buy a Gun
2. Select a Gun
3. List Guns
4. Rename a Gun
5. Use a Gun
6. Drop a Gun
7. Exit
5                                       
Segmentation fault (core dumped)

セグフォりました。Use a gunのコードを見てみます。

use_a_gun() {
	struct gun *gun = gun_data[selected_gun];
	printf("Select gun %s", gun->name);
	puts("1. Shoot");
	puts("2. Reload");
	puts("3. Info");
	puts("4. Main menu");
	char buf[0x20];
	while(true){
		read_until(stdin, buf, 0x20, '\n');
		int n = atoi(buf); 
		switch(n) {
			case 1:
				gun->vtable->op_shoot(gun);
				break;
			case 2:
				gun->vtable->op_reload(gun);
				break;
			case 3:
				gun->vtable->op_info(gun);
				break;
			case 4:
				return;
			default:
				puts("Wrong input");
		}
	}
}

gun_data[selected_gun]の初期値はNULLですからprintf("Select gun %s", gun->name);のところでセグフォったのだと推測できます。
本来ならばguns[selected_gun]がtrueであることを確かめなければならないはずです。
また、選択した銃を捨てた場合、その銃の構造体の領域はfreeされますが、gun_data[selected_gun]はそのままなのでfreeされた領域が参照できることがわかります。
gun->nameもmallocで管理された領域なので、文字列がfreeされた後にgun構造体として再利用されれば、その構造体のデータをleakできそうと言うことがわかります。

exploit

heapのアドレスleak

色々実験した結果、次のような入力でheapのアドレスがleakできることがわかりました。

$ cat exploit_1.txt
1
1
30
hogeeeeeeeeeeeeeeeee
1
1
15
01234
2
1
6
0
6
1
5
4
$ ./babyuse < exploit_1.txt | grep -a 'Select gun' | hexdump -C
00000000  53 65 6c 65 63 74 20 67  75 6e 20 08 3a 01 57 34  |Select gun .:.W4|
00000010  0a                                                |.|

トルエンディアンなので0x57013a08がheap上のアドレスです。
どうしてこの入力でleakできるのかはコンテスト時はわからなかったのですが、libcのfreeの実装を調べたところ、
freeされた領域にはlinked listになっていて、一つ前にfreeされた領域へのポインタが書き込まれるためのようです。
malloc(3)のメモリ管理構造 | VA Linux Systems Japan株式会社

executableアドレスのleak

今回のバイナリはPIEなので実行時にバイナリがどこに配置されているかがわかりません。なのでアドレスをleakさせます。
New(0,"hoge") -> New(0,"hoge") -> Select(1) -> Drop(1) -> Rename(0,data) とすると、Dropした銃の構造体があったheap領域に任意のdataを書き込むことが出来ます。
その領域に対してUse()を実行すると、gun_data[selected_gun]->nameが表示出来ます。
今、heapのアドレスはすでにleakされたので一番最初のNew()で作られたgun構造体のアドレスAが計算できます。
そこで、struct gun { vtable = DUMMY, name = A, ... }のようなデータを書き込むと、validなgun構造体のデータを表示させることができます。
したがって、t.vtableのアドレスとして実行バイナリのアドレスがleakできます。

f:id:autotaker:20170417182118p:plain

libcアドレスのleak

libcのアドレスは実行バイナリの.plt.gotセクションにあるはずなので適当なアドレスを上と同じ方法でleakさせます。
つまりstruct gun { vtable = DUMMY, name = free@plt, ... }とします。

f:id:autotaker:20170417182349p:plain

shellの起動

最後にshellを起動させます。Use()の後でShootを選択すると、gun_data[selected_gun]->vtable->op_shoot(gun_data[selected_gun])が実行できることを用います。
まず、{ op_shoot = system@libc, op_reload = ANY, op_info = ANY }となるデータをheap上に配置します。そのアドレスをAとします。
つぎに、{ vtable = A, name = A, max_bullets = "||sh", bullets = 0x0}となるデータをgun_data[selected_gun]のアドレスに再利用させます。
nameをAとしているのは、セグフォを防ぐためです。
するとsystem(&{ vtable = A, name = A, max_bullets = "||sh", bullets = 0x0})が実行できます。つまりsystem("~~~~||sh")のようなことになります。||の前の部分は不正な文字列ですが、コマンド名が見つからないだけなので特に困りません。
f:id:autotaker:20170417185604p:plain

exploit


gistbbc00350a0919027da07c8846de3515c

$ python3 exploit.py
....
RECV: b'/\n'
RECV: b'babyuse\n'
RECV: b'bin\n'
RECV: b'dev\n'
RECV: b'flag\n'
RECV: b'lib\n'
RECV: b'lib32\n'
RECV: b'lib64\n'
RECV: b'wrapper\n'
RECV: b'bctf{ec1c977319050b85e3a9b50d177a7746}\n'

0CTF Writeup: oneTimePad2

Japanese Version

Task

oneTimePad1と同じように暗号化スクリプトoneTimePad2.pyとciphertxtが入ったzipファイルがもらえる。
今度は\(GF(2^{128})\)のブロック暗号システムのようだ。

\begin{align}
C_i &= M_i + R_i \\
\begin{bmatrix}
R_{i+1} \\
1
\end{bmatrix} &=
\begin{bmatrix}
A & B\\
0 & 1\\
\end{bmatrix}^{N_i}
\begin{bmatrix}
R_{i} \\
1
\end{bmatrix} \\
N_{i+1} &= N_i^2\\
\end{align}
\(C_1 \dots, C_5 , M_1, \dots, M_4, A, B \)が既知である。\(M_5\)にフラグがあるようだ。
秘密鍵は\(N_1\)なのでこれを解読したい。

解析

まず、行列の累乗を計算する。
\begin{align}
\begin{bmatrix}
A & B\\
0 & 1\\
\end{bmatrix}^{n} &=
\begin{bmatrix}
A^n & A^{n-1} B + A^{n-2} B + \dots + B \\
0 & 1
\end{bmatrix} \\
&=
\begin{bmatrix}
A^n & \frac{(A^{n} - 1)B}{A - 1}\\
0 & 1
\end{bmatrix}
\end{align}
したがって
\[
R_{2} = A^{N_1} R_{1} + \frac{(A^{N_1} - 1)B}{A - 1}
\]
これを\(A^{N_1}\)について解くと
\[
A^{N_1} = (R_2 + B (A - 1)^{-1})(R_1 + B(A-1)^{-1})^{-1}
\]
よって\(A^{N_1}\)の値は計算できる。
\(N_1\)を計算するのは離散対数問題といって一般の体では計算するのは難しいが、少なくとも\(GF(2^{128})\)なら離散対数は現実的な時間で計算できるようだ。

解法

pari/gpで離散対数を計算する処理までを行った。

gistc2a4481d5f18d35e913503664320a016

$ gp -q doit.gp  
x^123 + x^117 + x^116 + x^114 + x^113 + x^112 + x^110 + x^109 + x^108 + x^107 + x^104 + x^99 + x^98 + x^97 + x^95 + x^93 + x^91 + x^89 + x^87 + x^84 + x^83 + x^82 + x^81 + x^80 + x^78 + x^74 + x^69 + x^68 + x^66 + x^62 + x^57 + x^53 + x^52 + x^51 + x^45 + x^43 + x^42 + x^41 + x^38 + x^37 + x^35 + x^33 + x^32 + x^31 + x^30 + x^29 + x^28 + x^25 + x^22 + x^19 + x^18 + x^17 + x^15 + x^14 + x^13 + x^12 + x^10 + x^8 + x^5 + x^2 + 1
76716889654539547639031458229653027958

10秒くらい待つと離散対数が計算できたので元のプログラムを改変して復号した。

gistedf58b1bf3484af727d98a7ebda023ff

$ python exploit.py
['\r\xa8\xe9\xe8J\x99\xd2M\x0fx\x8cqn\xf9\xe9\x9c', '\xc4G\xc3\xcf\x12\xc7\x16 m\xee\x92\xb9\xceY\x1d\xc0', 'r-BF)\x18b\x11 \xec\xe6\x8a\xc6NI:', 'A\xea:p\xdd\x7f\xe2\xb1\xd1\x16\xacH\xf0\x8d\xbf+', '&\xbdc\x83O\xa5\xb4\xcbu\xe3\xc6\rIg`\x92', '\x1b\x91\xdf^^c\x1e\x8e\x9eP\xc9\xd8\x03P$\x9c']
['One-Time Pad is ', 'used here. You w', "on't know that t", 'he flag is flag{']
One-Time Pad is used here. You won't know that the flag is flag{LCG1sN3ver5aFe!!}.��Y���+�]j�
 

flag文字列が自分の解法とあまり一致していない気がするので離散対数をもとめずとも計算できるのかもしれない。

English Version

Task

In the provided zip file, there are an encryption script 'oneTimePad2.py' and 'ciphertext'.
In this time, the crypt system is built on \(GF(2^{128})\)

\begin{align}
C_i &= M_i + R_i \\
\begin{bmatrix}
R_{i+1} \\
1
\end{bmatrix} &=
\begin{bmatrix}
A & B\\
0 & 1\\
\end{bmatrix}^{N_i}
\begin{bmatrix}
R_{i} \\
1
\end{bmatrix} \\
N_{i+1} &= N_i^2\\
\end{align}
We know \(C_1 \dots, C_5, M_1, \dots, M_4, A, B \).
The flag must be in \(M_5\).
We want to detect the value of \(N_1\) in order to break this system.

Analysis

First, let's compute the matrix power.
\begin{align}
\begin{bmatrix}
A & B\\
0 & 1\\
\end{bmatrix}^{n} &=
\begin{bmatrix}
A^n & A^{n-1} B + A^{n-2} B + \dots + B \\
0 & 1
\end{bmatrix} \\
&=
\begin{bmatrix}
A^n & \frac{(A^{n} - 1)B}{A - 1}\\
0 & 1
\end{bmatrix}
\end{align}
Therefore,
\[
R_{2} = A^{N_1} R_{1} + \frac{(A^{N_1} - 1)B}{A - 1}
\]
By solving this equation for \(A^{N_1}\),
\[
A^{N_1} = (R_2 + B (A - 1)^{-1})(R_1 + B(A-1)^{-1})^{-1}
\]
Then, we can conpute the value of \(A^{N_1}\).
Task to compute the value of \(N_1\) from \(A^{N_1}\) is called 'discrete logarithm problem', which is known to be difficult for general fields.
Fortunately, in this field \(GF(2^{128})\), the discrete logarithm is computable in a reasonable time.

Solution

We compute the descrete logarithm with PARI/GP.

gistc2a4481d5f18d35e913503664320a016

$ gp -q doit.gp  
x^123 + x^117 + x^116 + x^114 + x^113 + x^112 + x^110 + x^109 + x^108 + x^107 + x^104 + x^99 + x^98 + x^97 + x^95 + x^93 + x^91 + x^89 + x^87 + x^84 + x^83 + x^82 + x^81 + x^80 + x^78 + x^74 + x^69 + x^68 + x^66 + x^62 + x^57 + x^53 + x^52 + x^51 + x^45 + x^43 + x^42 + x^41 + x^38 + x^37 + x^35 + x^33 + x^32 + x^31 + x^30 + x^29 + x^28 + x^25 + x^22 + x^19 + x^18 + x^17 + x^15 + x^14 + x^13 + x^12 + x^10 + x^8 + x^5 + x^2 + 1
76716889654539547639031458229653027958

It took around ten seconds before we have the discrete logarithm.
Then, we decrypted the cipher text with a modified version of the encryption program.

gistedf58b1bf3484af727d98a7ebda023ff

$ python exploit.py
['\r\xa8\xe9\xe8J\x99\xd2M\x0fx\x8cqn\xf9\xe9\x9c', '\xc4G\xc3\xcf\x12\xc7\x16 m\xee\x92\xb9\xceY\x1d\xc0', 'r-BF)\x18b\x11 \xec\xe6\x8a\xc6NI:', 'A\xea:p\xdd\x7f\xe2\xb1\xd1\x16\xacH\xf0\x8d\xbf+', '&\xbdc\x83O\xa5\xb4\xcbu\xe3\xc6\rIg`\x92', '\x1b\x91\xdf^^c\x1e\x8e\x9eP\xc9\xd8\x03P$\x9c']
['One-Time Pad is ', 'used here. You w', "on't know that t", 'he flag is flag{']
One-Time Pad is used here. You won't know that the flag is flag{LCG1sN3ver5aFe!!}.��Y���+�]j�

Now, we have the flag, but there may be another solution which does not require to compute discrete logarithms, since our solution seems to be different from what the flag suggests.

0CTF Writeup: oneTimePad1

これは0CTFのoneTimePad1という問題のWriteupです。

Japanese Version

Task

zipファイルを開くと暗号化スクリプトoneTimePad.pyと暗号文ciphertextがある。
暗号化の仕組みはブロック暗号で\(GF(2^{256})\)上で次のように計算する。

\begin{align}
C_1 &= M_1 + R_1 \\
C_2 &= M_2 + R_2 \\
C_3 &= M_3 + R_3
\end{align}
ここで\(C_1, C_2, C_3\)が暗号文、 \(M_1, M_2, M_3\)が平文となる。
\(C_1, C_2, C_3, M_2, M_3\)は既知で\(M_1\)を復号するのが問題のようだ。

解析

もちろん、暗号化の肝は\(R_1, R_2, R_3\)という擬似乱数生成器の生成した数列にある。
擬似乱数生成器は、秘密鍵\(K\)と現在の乱数\(R_i\)から次の乱数\(R_{i+1}\)を次のように生成する。
\[
R_{i+1} = (R_{i} + K)^2
\]
今\(GF(2^{256})\)上で考えているので、\(2 = 0, X + Y = X - Y \)が成り立つことに注意すると、
\[
R_{i+1} = R_{i}^2 + K^2
\]
となる。\(C_2, C_3, M_2, M_3\)はわかっているので、\(K^2 = R_2 + R_1^2\)の右辺は計算できる。
これを\(R_1 = R_0^2 + K^2\)に代入すると
\[
R_0 = \sqrt{ R_1 + R_2 + R_1^2 }
\]
である。右辺の平方根は平方剰余というやつでPARI/GPというツールを使うと計算できる。

解法


gist8bcd0ce53f61a87c8742e697917cfae1

$ gp -q doit.gp 
52553756545437879763013576434186236591362916937163148104579268147006553551449
$ python
>>> hex(52553756545437879763013576434186236591362916937163148104579268147006553551449)[2:-1].decode('hex')
't0_B3_r4ndoM_en0Ugh_1s_nec3s5arY'

English Version

Task

There are an encryption script 'oneTimePad.py' and 'ciphertext' in the provided zip file.

The crypto system is described over \(GF(2^{256})\)
\begin{align}
C_1 &= M_1 + R_1 \\
C_2 &= M_2 + R_2 \\
C_3 &= M_3 + R_3
\end{align}
Here, \(C_1, C_2, C_3\) are cipher texts and \(M_1, M_2, M_3\) are plain texts.
We know \(C_1, C_2, C_3, M_2, M_3\), and the task of this problem is to decrypt \(C_1\).

Analysis

Of course, the clue of this crypto system is pseudo random numbers \(R_1, R_2, R_3\).
The random number generator generates the next number \(R_{i+1}\) from Secret key \(K\)
and the current number \(R_i\) in the following way:
\[
R_{i+1} = (R_{i} + K)^2
\]
We note that equations like \(2 = 0, X + Y = X - Y\) hold because the field is \(GF(2^{256})\).
Then, we have,
\[
R_{i+1} = R_{i}^2 + K^2
\]
The rhs of \(K^2 = R_2 + R_1^2\) is computable since we know \(C_2, C_3, M_2, M_3\).
By substituting it to \(R_1 = R_0^2 + K^2\), we have
\[
R_0 = \sqrt{ R_1 + R_2 + R_1^2 }
\]
The square root in its rhs is so called quadratic residue and it is computable with
tools like PARI/GP.

Solution


gist8bcd0ce53f61a87c8742e697917cfae1

$ gp -q doit.gp 
52553756545437879763013576434186236591362916937163148104579268147006553551449
$ python
>>> hex(52553756545437879763013576434186236591362916937163148104579268147006553551449)[2:-1].decode('hex')
't0_B3_r4ndoM_en0Ugh_1s_nec3s5arY'

State Monadと正格性について

今回の話題は、State MonadはStrictなものを使おうという話である。

StateT s m a

HaskellでState Monadを使う際、一番よく使うのは
transformer packageのStateT s m aだと思う。
transformers: Concrete functor and monad transformers
あるいは、そのwrapper libraryとしてmtlを使うかもしれない。
mtl: Monad classes, using functional dependencies
どちらにしろ実体は同じだ。
このStateTにはLazyなバージョンとStrictなバージョンの2種類がある。
二つともデータ型の定義は同じである。

newtype StateT s m a = StateT { runStateT :: s -> m (a, s ) }

違いはMonad (StateT s m)のインスタンス宣言である。

-- Strict
instance Monad m => Monad (StateT s m) where
    return x = StateT (\s -> return (x, s))
    StateT mv >>= f = StateT $ \s -> do
        (v,s1) <- mv s
        runStateT (f v) s1
-- Lazy
instance Monad m => Monad (StateT s m) where
    return x = StateT (\s -> return (x, s))
    StateT mv >>= f = StateT $ \s -> do
        ~(v,s1) <- mv s
        runStateT (f v) s1

Lazyの方は~(チルダ)パターンという見慣れないものが使われているが、これは概ね以下と同じだ。

    p <- mv s
    let (v,s1) = p

違いは、mv sの結果をバインドするときに、タプルのWHNFまで簡約するか、あるいは遅延させるかという点である。

正格性

ここでState MonadのExampleとして、状態を使って1からnまでの和を求めるプログラムを書いてみよう。

-- Main.hs
import Data.Functor.Identity
import Control.Monad.Trans.State.Lazy (StateT(..), get, put)
main :: IO ()
main = do
  n <- readLn
  let (_,s) = runIdentity (runStateT (sumState n) 0)
  print s

sumState :: Monad m => Int -> StateT Int m ()
sumState n = mapM_ (\i -> modify (+i)) [1..n]

modify :: Monad m => (s -> s) -> StateT s m ()
modify f = do
    v <- get
    put (f v)

しかし、このプログラムをコンパイルして実行してみると非常に遅いことがわかる。

$ ghc -O Main.hs
$ echo 10000000 | time ./Main
50000005000000
        2.27 real         1.41 user         0.72 sys

これはなぜかというと、modify fが正格でないため、Stateに(...((0 + 1) + 2) + ... + n)というthunkが積まれてしまうからである。
この現象はControl.Monad.Trans.State.LazyとControl.Monad.Trans.State.Strictの両方で発生する。
状態を正格に評価するために、modifyの定義を少し変更する。

modify f = do
    v <- get
    put $! f v

($!)は正格な関数適用演算子である。こうすることで、modify (+i)の部分が実行されるたびにStateを正格評価するように思える。
実際、この関数はControl.Monad.Trans.State.(Strict | Lazy).modfy'としてライブラリにも定義されている。

実際、Control.Monad.Trans.State.Strict.StateTではこの変更で期待通りに動く。

$ echo 10000000 | time ./Main
50000005000000
        0.02 real         0.01 user         0.00 sys

しかし、残念ながら、Control.Monad.Trans.State.Lazy.StateTでは上手くいかない。

echo 10000000 | time ./Main
50000005000000
        1.94 real         1.27 user         0.50 sys

また、奇妙なことだが、LazyなStateTでも、baseモナドをIdentityからIOに変えたりすると状態が正格に計算される。

import Control.Monad.Trans.State.Lazy (StateT(..), get, put)
main :: IO ()
main = do
  n <- readLn
  (_,s) <- runStateT (sumState n) 0
  print s
$ echo 10000000 | time ./Main 
50000005000000
        0.02 real         0.01 user         0.00 sys

謎解き

これはなぜだろうか、この謎を解くためにはmodify fがどのようにコンパイルされるかをみていく必要がある。

 modify f 
== get >>= (\v -> put $! (f v)) -- unfold "modify"
== StateT (\s -> return (s,s)) >>= (\v -> put $! (f v))  -- unfold "get"
== StateT (\s -> do  -- unfold (>>=)
            ~(a,s1) <- return (s,s)
            runStateT ((\v -> put $! (f v)) a) s1)
== StateT (\s -> do  -- beta reduction
            ~(a,s1) <- return (s,s)
            runStateT (put $! (f a)) s1)
== StateT (\s -> do -- unfold ($!) and "put"
            ~(a,s1) <- return (s,s)
            runStateT (let !v = f a in StateT (\_ -> return ((),v))) s1)
== StateT (\s -> do -- simplify
            ~(a,s1) <- return (s,s)
            (let !v = f a in return ((),v)))
== StateT (\s -> return (s,s) >>= (\p -> -- desugar do notation
                 let (a, s1) = p in
                 let !v = f a in
                 return ((),v)))
== StateT (\s -> let (a, s1) = (s,s) in -- apply monad law (left identity)
                 let !v = f a in
                 return ((),v)))
== StateT (\s -> let !v = f s in return ((),v)) -- simplify

今の所、特に問題のある部分はない。
しかし、baseモナドによっては問題が明らかになる。
その前にIdentity Monadの定義を復習しておく。

newtype Identity a = Identity { runIdentity :: a }
instance Monad Identity where
  return x = Identity x
  m >>= f = f (runIdentity a)

さて、次の項をIdentityモナド上で簡約してみよう。

(modify f) >> action :: StateT s Identity a
== StateT (\s -> let !v = f s in return ((),v)) >> action 
== StateT (\s -> let !v = f s in return ((),v)) >>= (\_ -> action) -- unfold (>>)
== StateT (\s -> do  -- unfold (>>=)
            ~(_,s1) <- let !v = f s in return ((),v)
            runStateT action s1)
== StateT (\s -> -- desugar do notation
           (let !v = f s in return ((),v)) >>= (\p ->
           let (_,s1) = p in
           runStateT action s1))
== StateT (\s -> -- unfold (>>=)
           (\p ->
           let (_,s1) = p in
           runStateT action s1) (let !v = f s in return ((),v)))
== StateT (\s -> -- beta reduction
           let (_,s1) = let !v = f s in return ((),v) in
           runStateT action s1)

さて、簡約結果を見てみると、 let !v = f s in return ((),v)の部分がさらにlet (_,s1) = ... in ...でくるまれているため、
評価が遅延されていることがわかると思う。この問題はbaseモナドがIOの場合は発生しない。
なぜなら、IO a は RealWorld -> (# RealWorld, a #)という型として評価されるわけだが、(# RealWolrd, a #)というタプルはthunkになり得ないからだ。

ちなみに、Control.Monad.Trans.State.Strictの場合は、以下のようになる。

(modify f) >> action :: StateT s Identity a
== StateT (\s -> let !v = f s in return ((),v)) >> action
== StateT (\s -> let !v = f s in return ((),v)) >>= (\_ -> action)
== StateT (\s -> do
            (_,s1) <- let !v = f s in return ((),v)
            runStateT action s1)
== StateT (\s -> 
           (let !v = f s in return ((),v)) >>= (\(_,s1) ->
           runStateT action s1))
== StateT (\s -> 
           (let !v = f s in Identity ((),v)) >>= (\(_,s1) ->
           runStateT action s1))
== StateT (\s ->
           (\(_,s1) ->
           runStateT action s1) (let !v = f s in Identity ((),v)))
== StateT (\s ->
           case (let !v = f s in Identity ((),v)) of
             (_,s1) -> runStateT action s1)
== StateT (\s ->
           case f s of
             v -> case Identity ((),v) of
               (_,s1) -> runStateT action s1)
== StateT (\s ->
           case f s of
             v -> runStateT action v)

従ってf sの評価はactionの評価より前に行われる。

結論

LazyなStateモナドでmodify'を使うべきではない。使う必要が出てきた場合にはStrictなStateモナドを使おう。

普通はStrictなものを使っておけば良いと思う。LazyなStateモナドが役に立つ場面は本当にあるのだろうか。甚だ疑問である。

僕の考えたさいきょうの抽象構文木データ型

あらすじ

プログラミング言語処理系を作成しようとすると避けては通れないのが、構文木データ型の設計である。
言語処理系では構文解析、アルファ変換、脱糖、正規化など構文木を変換するパスがいくつか存在して、それらの構文ごとにデータ型を設計しなければならない。今回はHaskellの依存型機能を使って、拡張のしやすい構文木データ型の構築方法を示す。

はじめに

今回の記事では単純な型なし関数型言語インタープリタを実装していく。コード全体はgithubに上げている。
github.com

今回のお題

今回は次のような構文の関数型言語を題材にする。評価戦略は値呼びである。

<expr> ::= <id> | <int_literal> | <bool_literal>
        |  <prefix_op> <expr> 
        |  <expr> <infix_op> <expr>
        | "let" <id> "=" <expr> "in" <expr>
        | "fun" <id> "->" <expr>
        | <expr> <expr>
        | "if" <expr> "then" <expr> "else" <expr>
        | "if" <expr> "then" <expr>
        | <expr> "&&" <expr> | <expr> "||" <expr>
<id> ::= [a-zA-Z][a-zA-Z0-9'_]*
<int_literal> ::= [0-9]+
<bool_iteral> ::= "true" | "false"
<prefix_op> ::= "+" | "-"
<infix_op> ::= "*" | "/" | "+" | "-" | "<" | ">" | "=" | "<>" | "<=" | ">="

素朴な実装

このような構文をHaskellのデータ型で表現する際、最も素朴なのは代数的データ型を用いるものだろう。
例えばこんな感じ。

data Expr = Id Id | IntL Int | BoolL Bool 
          | PrefixOp POp Expr | InfixOp IOp Expr Expr
          | Let Id Expr Expr 
          | Fun Id Expr
          | App Expr Expr
          | IfThenElse Expr Expr Expr
          | IfThen Expr Expr
          | Cond CondOp Expr Expr
data CondOp = And| Or
type Id = String
data POp = Plus | Minus
data IOp = Mul | Div | Add | Sub | ...

ただし、この定義には二つの問題点がある。

  • どの構文ノードにも共通して存在するデータを埋め込むのが面倒、例えば、構文木ノードにユニークなラベルを貼ったり、ソースコード上での位置を表すデータなどのメタデータを埋め込みたいとき、全てのコンストラクタに書かなければならない。
  • 拡張性に乏しい。例えば"e0 && e1"は"if e0 then e1 else false"の糖衣構文であるので、脱糖後のデータ構造にはそのような構文は許されないが、脱糖後のデータ型でそのことを表現するためにはほぼ同じ代数的データ型を定義する必要がある。コンストラクタの名前を考えるのが面倒だし、名前空間が汚くなる。

僕の考えたさいきょうの抽象構文木データ型

ここで本記事の目的であるデータ型を紹介しよう。
まず、DataKinds拡張を使って構文木のコンストラクタのラベルを表すConstカインドと
そのシングルトン型SConstをGADTとして定義する。

{-# Language DataKinds, GADTs #-}
module Language.ToyML.Syntax.Base where
import Data.Void(Void)
import Data.Kind(Constraint)

data Const = Var | Literal | Infix | Prefix 
           | App | Abs | Let  
           | IfT | IfTE
           | Cond

data SConst (c :: Const) where
    SVar     :: SConst 'Var
    SLiteral :: SConst 'Literal
    SInfix   :: SConst 'Infix
    SPrefix  :: SConst 'Prefix
    SApp     :: SConst 'App
    SAbs     :: SConst 'Abs
    SLet     :: SConst 'Let
    SIfT     :: SConst 'IfT
    SIfTE    :: SConst 'IfTE
    SCond    :: SConst 'Cond

そして構文木のデータ型はこれだ。

data Exp where
    Exp :: WellFormed c Exp arg => SConst c -> arg -> Exp

つまり、構文木はExp op argという二つ組でopはSConst c型、つまりコンストラクタの種類を表している、
一方argの型はこの定義からはわからないが、WellFormed c Exp argという制約がargの型を定めてくれる。
カギはWellFormed c e argという制約にあるわけだが、これはtype familyという仕組みで次のように定義している。

type family WellFormed (c :: Const) e arg :: Constraint where
    WellFormed 'Var e arg     = arg ~ Ident e
    WellFormed 'Literal e arg = arg ~ Literal e
    WellFormed 'Infix e arg   = arg ~ (InfixOp e,e,e)
    WellFormed 'Prefix e arg  = arg ~ (PrefixOp e, e)
    WellFormed 'App e arg     = arg ~ (e,e)
    WellFormed 'Abs e arg     = arg ~ (Ident e, e)
    WellFormed 'Let e arg     = arg ~ (Ident e, e, e)
    WellFormed 'IfT e arg     = arg ~ (e, e)
    WellFormed 'IfTE e arg    = arg ~ (e, e, e)
    WellFormed 'Cond e arg    = arg ~ (CondOp, e, e)

type family Ident e
type family Literal e
type family InfixOp e
type family PrefixOp e

この定義によると、例えばExp SApp argの場合、argは(Exp, Exp)型となり、またExp SVar argの場合はargはIdent Exp型になる。
Ident Exp型がどのような型になるかもtype familyによって定めており、具体的にはStringになるように次のように定めている。

type instance Ident Exp = String
type instance Literal Exp = Lit
type instance InfixOp Exp = Op
type instance PrefixOp Exp = Op
data Lit = CInt Integer | CBool Bool
data Op = Op { headChar :: Char, opName :: String }

この定義に従うと構文解析後のデータとして"正しい"データ構造を表現できている。例えば次のような例があり、間違ったデータ構造はコンパイルエラーとなる。

exp1 :: Exp
exp1 = Exp SVar "x"

exp2 :: Exp
exp2 = Exp SAbs ("x", Exp SApp (Exp SVar "x", Exp SVar "x")) -- fun x -> x x

exp3 :: Op -> Exp
exp3 op = Exp SPrefix (op, Exp SVar "x") 


-- これはコンパイルエラー(前置演算子なのに二つ子のExpを持つため)
-- exp3bug :: Op -> Exp
-- exp3bug op = Exp SPrefix (op, Exp SVar "x", Exp SVar "x")

このパターンで構文木データ型を定義すると共通するデータを埋め込むのも容易である。
例えば、ソースコード上の位置を埋め込みたければ

data Exp where
    Exp :: WellFormed c Exp arg => SConst c -> arg -> SourcePos -> Exp

と変えるだけで良い。

次に拡張も簡単であることを示すために脱糖後のデータ型をこのパターンを用いて定義してみよう。

data Exp where
    Exp :: (WellFormed c Exp arg, Desugared c Exp arg) => 
           SConst c -> arg -> SourcePos -> Exp

type family Desugared (c :: Const) e arg :: Constraint where
    Desugared 'Infix e arg = Impossible 'Infix
    Desugared 'Prefix e arg = Impossible 'Prefix
    Desugared 'IfT e arg = Impossible 'IfT
    Desugared 'Cond e arg = Impossible 'Cond
    Desugared c e arg = ()

これだけである。
先ほど定義したWellFormed c e argという制約に加えて脱糖後にはInfix, Prefix, IfT, Condのコンストラクタが使えないことをDesugared c e argという制約で表現している。
ここでImpossibleという制約があるわけだが、この制約はこのように定義する。

import Data.Void
class Impossible (c :: Const) where
    impossible :: SConst c -> Void

つまりImpossibleは型クラスであり、そのインスタンスは存在しない。したがって、Impossible制約を持つコンストラクタを使うことはできないようになっている。逆にパターンマッチでこのパターンが来たらData.Void.absurd :: Void -> aという最強関数で安全に型を合わせてしまうことができる。

終わりに

今回紹介したパターンを使えばこのように柔軟な型コンストラクタをHaskellでも実装することができる。パターンマッチの部分もなかなか面白いので興味のある人はレポジトリのコードを読んでみてほしい。
github.com

OS Xにおける共有ライブラリについてのメモ

最近Z3のインストールに複数の意味でハマっていて、その過程で動的ライブラリに対する理解が深まったのでメモしておく。
autotaker.hatenablog.com

動的ライブラリとは

動的ライブラリは静的ライブラリと異なり、実行時にリンクされる。
今まで誤解していたのだが、ライブラリを使用する側からはライブラリが静的か動的かは関係がない。
コンパイラソースコードをオブジェクトファイルにする段階ではライブラリのヘッダファイルさえあればよくて、リンカが実行形式ファイルを出力する段階で初めてシンボルを静的に解決するか動的に解決するかが決まる。

覚えておくと便利なコマンド

環境はOS Xを想定している。

  • 実行形式ファイルあるいは動的ライブラリからそれが参照する動的ライブラリの一覧を取得する。
otool -L ファイル
  • 実行形式ファイルあるいは動的ライブラリからload commandsの一覧を取得する。
otool -l ファイル
  • 動的ライブラリがexportしている関数の一覧を取得する。
gobjdump -T ファイル

動的リンクの仕組み

ところで、動的リンカはどのようにして実行時に動的ライブラリの実体を見つけてくるのだろうか?

例えば、手元にある適当な動的ライブラリが使用する動的ライブラリを見てみよう。

/Users/autotaker/.cabal/lib/x86_64-osx-ghc-7.10.2/z3-4.1.0-CQEXZ6rXqZX8ei09CJh4x5/libHSz3-4.1.0-CQEXZ6rXqZX8ei09CJh4x5-ghc7.10.2.dylib:
	@rpath/libHSz3-4.1.0-CQEXZ6rXqZX8ei09CJh4x5-ghc7.10.2.dylib (compatibility version 0.0.0, current version 0.0.0)
	libz3.dylib (compatibility version 0.0.0, current version 0.0.0)
	@rpath/libHSmtl-2.2.1-2BzSpTumj4ZLLPrpLUWDdr-ghc7.10.2.dylib (compatibility version 0.0.0, current version 0.0.0)
	@rpath/libHStransformers-0.4.2.0-3eG64VdP2vzGjP6wJiCp5X-ghc7.10.2.dylib (compatibility version 0.0.0, current version 0.0.0)
	@rpath/libHScontainers-0.5.6.2-LKCPrTJwOTOLk4OU37YmeN-ghc7.10.2.dylib (compatibility version 0.0.0, current version 0.0.0)
	@rpath/libHSdeepseq-1.4.1.1-LbCWUlehDDeLxurARKDH5o-ghc7.10.2.dylib (compatibility version 0.0.0, current version 0.0.0)
	@rpath/libHSarray-0.5.1.0-E0sTtauuKsGDLZoT7lTbgZ-ghc7.10.2.dylib (compatibility version 0.0.0, current version 0.0.0)
	@rpath/libHSbase-4.8.1.0-GDytRqRVSUX7zckgKqJjgw-ghc7.10.2.dylib (compatibility version 0.0.0, current version 0.0.0)
	@rpath/libHSinteger-gmp-1.0.0.0-2aU3IZNMF9a7mQ0OzsZ0dS-ghc7.10.2.dylib (compatibility version 0.0.0, current version 0.0.0)
	@rpath/libHSghc-prim-0.4.0.0-8TmvWUcS1U1IKHT0levwg3-ghc7.10.2.dylib (compatibility version 0.0.0, current version 0.0.0)
	/usr/lib/libiconv.2.dylib (compatibility version 7.0.0, current version 7.0.0)
	/usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1226.10.1)

このライブラリではライブラリの指定の仕方に以下の3種類が用いられている。(一般にはもう何種類かあるらしいが説明は割愛)

  • 絶対パス(例:/usr/lib/libiconv.2.dylib )
  • 相対パス(例:libz3.dylib)
  • @rpathで始まるパス(例:@rpath/libHSz3-4.1.0-CQEXZ6rXqZX8ei09CJh4x5-ghc7.10.2.dylib)

この書き方にしたがって実行時に動的ライブラリを探してくる仕組みが異なる。

絶対パスの場合

この場合は特に難しいことはなくそのパスで指定された動的ライブラリをリンクする。

相対パスの場合

この場合はまず、DYLD_LIBRARY_PATHという環境変数に指定されたパスからライブラリを探索する。
そこで見つからなかった場合は、DYLD_FALLBACK_LIBRARY_PATHを探索する。DYLD_FALLBACK_PATHのデフォルト値は$(HOME)/lib:/usr/local/lib/:/lib/:/usr/libとなっている。

@rpathの場合

実行ファイルおよび動的ライブラリにはrpathと呼ばれる、実行時に動的ライブラリを探索するパスのリストが埋め込まれている。動的リンカはそのリストに含まれるパスから動的ライブラリを探索する。

rpathの追加

ldコマンドに-rpath というオプションを渡すと、実行ファイルにそのパスがrpathとして埋め込まれる。
clangでコンパイルする場合は-Wl,-rpath -Wl,とする。

install name

そもそも上記の3種類の指定はどのように決定されるのか?
その答えがinstall nameと呼ばれるものである。動的ライブラリを生成するときにldに-install_name というオプションを渡すことで指定できる。あるいは、install_name_toolというコマンドで生成された動的ライブラリのinstall nameを後から変更することができる。
ldが実行ファイルを生成するとき、動的ライブラリを見つけてきて、そのライブラリのinstall nameを実行ファイルの動的ライブラリのパスとして埋め込む。

以上調べたことをまとめて、実際にいろいろ試せるように共有ライブラリのビルドを行うレポジトリをgithubに公開しておいた。
github.com

OS Xにおける動的リンクのまとめは以下のサイトを参考にした。
mikeash.com: Friday Q&A 2009-11-06: Linking and Install Names