第二屆
Trend Micro CTF，題目一如去年風格很通靈
rev300 是當中少數正常的題目了
難得在 reverse 題中拿到首殺ＸＤ，小時候寫過 ActionScript 可能還是有點幫助(?)
這題是個動畫 (SWF) 題，題目提供一個檔案(game.swf)
動畫執行畫面先是個輸入名字：
打完名字後如同檔名是個遊戲：
遊戲方式是上下左右移動人物 (綠色的 S)，撞怪物可以殺怪，被怪物撞 9 次就死亡。但身為一個 reverse 題，遊戲本身肯定是不重要的，因此先找工具對動畫進行反編譯。
我使用的反編譯工具是 open source 的
JPEXS Free Flash Decompiler，賽中比較過其他工具但以這個解出來的最完整。
decompile 出來的目錄結構長得像這樣：
game
├── binaryData
│ ├── 1__el_-__-_--.bin
│ ├── 2__el_-__--__.bin
│ ├── 3__el_-_-___-.bin
│ ├── 4__el_-__--_-.bin
│ ├── 5__el_-__---_.bin
│ ├── 6__el_-__----.bin
│ ├── 7__el_-___--_.bin
│ └── 8__el_-__-__.bin
├── frames
│ ├── 1.png
│ └── 2.png
├── scripts
│ ├── KCS___Main.as
│ ├── mx
│ │ └── core
│ │ ├── ByteArrayAsset.as
│ │ ├── IFlexAsset.as
│ │ └── mx_internal.as
│ ├── §_el_-----_§.as
│ ├── §_el_--_--_§.as
│ ├── §_el_-_-___-§.as
│ ├── §_el_-_-____§.as
│ ├── §_el_-__----§.as
│ ├── §_el_-__---_§.as
│ ├── §_el_-__--_-§.as
│ ├── §_el_-__--__§.as
│ ├── §_el_-__-_--§.as
│ ├── §_el_-__-__§.as
│ ├── §_el_-__-_§.as
│ ├── §_el_-___--_§.as
│ └── §_el_-____-§.as
└── symbols.csv
scripts/ 中的那堆噁心檔名(.as) 就是主要的動畫函式，ActionScript 看起來跟 Java 有 7 成像，基本上閱讀不會有困難。不過變數名字跟檔名都被混淆過，可以手動或自動反混淆一下比較方便。
在 *.as 裡兜來兜去會發現感受不到任何一段程式碼在實作輸入名字或玩遊戲的地方。覺得必定有詐時注意到其中有幾個 .as 檔都只有簡單的幾行：
package
{
import mx.core.ByteArrayAsset;
public class §_el_-___--_§ extends ByteArrayAsset
{
public function §_el_-___--_§()
{
super();
}
}
}
接著發現這幾個檔案的檔名剛好會一一對應到 binaryData 底下的檔案們，因此猜測這幾個 class 應該是會分別 load 那些 bin 檔案成為 ByteArray。
file 一下 binaryData 的檔案們：
$ file *
1__el_-__-_--.bin: JPEG image data, JFIF standard 1.01
2__el_-__--__.bin: PNG image data, 50 x 50, 8-bit/color RGBA, non-interlaced
3__el_-_-___-.bin: PNG image data, 50 x 50, 8-bit/color RGBA, non-interlaced
4__el_-__--_-.bin: PNG image data, 50 x 50, 8-bit/color RGBA, non-interlaced
5__el_-__---_.bin: XML document text
6__el_-__----.bin: PNG image data, 50 x 50, 8-bit/color RGBA, non-interlaced
7__el_-___--_.bin: data
8__el_-__-__.bin: data
前幾個圖檔與 XML 感覺就不是很重要。 7 號檔案長度 16 byte，8 號檔案長度 344kb，直覺就覺得肯定是拿 7 號當 key 去解 8 號檔案會得到個什麼。於是就仔細去看程式碼中有用到 7 號與 8 號的部分，果然找到了一段在進行 decode 的程式碼(§_el_-__-_§.as)：
public function §_el_-_-_-_§(param1:int) : void
{
var _loc2_:int = 0;
while(_loc2_ < param1 && this.§_el_-______§ < this.§_el_-_-__§.length)
{
this.§_el_-_-__§[this.§_el_-______§++] =
this.§_el_-_-__§[this.§_el_-______§++] ^ this.§_el_----_-§();
_loc2_++;
}
}
有個 xor 看起來就超可疑ＸＤ所以其實滿容易感受到這裏在 decode 的。認真看 code 之後總之大約是個用 bin7 當作 random_shuffle 的 seed，產出 xor_key 之後跟 bin8 xor。照樣寫個一樣的 decoder 就能解出 bin8 真正的樣子 --
另一個動畫檔。
但其實也不是很意外，不然要怎麼弄出那個遊戲畫面ＸＤ
於是就開拓了另一個新世界，先來把 bin8.swf 丟 decompile T__T
目錄結構：
bin8
├── binaryData
│ ├── 1__e_--_-.bin
│ ├── 2__e_-----.bin
│ └── 3__e_-_-_--.bin
├── frames
│ └── 1.png
├── scripts
│ ├── mx
│ │ └── core
│ │ ├── ByteArrayAsset.as
│ │ ├── IFlexAsset.as
│ │ └── mx_internal.as
│ ├── §'§.as
│ ├── §_e_-----_§.as
│ ├── §_e_-----§.as
│ ├── §_e_--_--§.as
│ ├── §_e_--_-_§.as
│ ├── §_e_--_-§.as
│ ├── §_e_--_§.as
│ ├── §_e_-_---_§.as
│ ├── §_e_-_--_§.as
│ ├── §_e_-_-_--§.as
│ ├── §_e_-__-_-§.as
│ └── §_e_-____--§.as
└── symbols.csv
正當以為檔案少一些應該好多了的時候真正的痛苦就開始了
點開 *.as 會看到各種💩一般的慘 code
不過出題者很好心地留下了一些 Message：
public function §_e_--___-§() : String
{
return "aes" + 8 * this.§_e_---__§;
}
大約猜得出來是在 Implement AES 解密吧。
跟下去究竟哪裡在玩 AES 解密之後就發現他是在對前 2 個 binaryData 做各種運算與解密。這部分就比較容易看懂了，大略是在把 bin2 每 16 個字元切開依序當 AES-ECB 的 key 對依某種方式(不贅述)切開的 bin1 解密，script 如下
#!/usr/bin/ruby
#encoding: ascii-8bit
require 'openssl'
$data1 = IO.binread('1__e_--_-.bin')[4..-1]
data2 = IO.binread '2__e_-----.bin'
$bin2_scan_16 = data2[1..-1].chars.each_slice(16).map(&:join)
$decoded = []
def bin2_scan_16;$bin2_scan_16;end
def decode(data, key)
decipher = OpenSSL::Cipher::AES.new(128, :ECB)
decipher.decrypt
decipher.key = key
plain = decipher.update(data) + decipher.final
$decoded.push(plain)
end
def work
data1 = $data1
len = 27
j = 0
while(j < len)
length = data1[0, 4].reverse.unpack("L*")[0]
decode(data1[4, length], bin2_scan_16[j % bin2_scan_16.size])
data1 = data1[(length+4)..-1]
j+=1
end
end
work
puts $decoded
Output 結果為：
70d4a3aa
, Game Over :(
http://www.trendmicro.com/us/about-us/careers/portal/index.html
6e415968
, You're too leeeeeeeeet
####
1337
PRESS ANY KEY TO RESTART
1fac0e9c
555555
....
Hey,
Welcome, Input Your Name and Have Fun!
417cfdf3
FFFF
I think you got the flag :)
33
MMMM
02f02daa
center
6962723d
YOUR SCORE:
ad2a75a9
007
6ee2c371
Sorry,
Hope you can join TrendMicro :)
解出了程式碼中一直在用到的 constant 字串們。當中最吸睛的當然是 I think you got the flag :) 這句，回追哪裡用到這個字串後找到底下這段：
if(this.§?§ >= parseInt("1337"))
{
_loc4_.appendText("Hey, " + this.username + ", You're too leeeeeeeeet\n");
_loc4_.appendText("Hope you can join TrendMicro :)\n");
_loc4_.appendText("http://www.trendmicro.com/us/about-us/careers/portal/index.html\n\n");
_loc5_ = this.§@§(["6e415968","6ee2c371","02f02daa","417cfdf3"]);
_loc6_ = this.§@§(["6962723d","ad2a75a9","70d4a3aa","1fac0e9c"]);
if(Boolean(this.§3§(this.§8§,this.username,_loc5_)) &&
Boolean(this.§3§(this.§7§,this.username,_loc6_)))
{
_loc4_.appendText("I think you got the flag :)\n");
}
}
（constant 字串都是手動取代過了，原本都長得像是 §_e_-----_§.§_e_-_-__-§(-1820302803) 般的鬼東西）
條件是在遊戲通關 1337 次後會印出訊息。要印出 "I think.." 需要讓一開始輸入的 username 經過兩個函式運算後都回傳 true。兩個函式解釋起來有點麻煩... 總之我們最後用
z3py (Theorem Prover) 來解什麼樣的 username 會滿足條件，即可獲得 flag。對 z3 不太熟 T_T，外包給隊友。
from z3 import *
def fun_8(s):
_loc4_ = BitVecVal(5592405, 32)
for i in xrange(len(s)):
c = s[i]
_loc4_ = _loc4_ ^ ZeroExt(24, c)
_loc4_ = RotateLeft(_loc4_, 7)
_loc4_ = simplify(_loc4_)
return _loc4_
def fun_7(s):
_loc4_ = BitVecVal(1337, 32)
for i in xrange(len(s)):
c = s[i]
_loc4_ = _loc4_ * 33 + ZeroExt(24, c)
_loc4_ = simplify(_loc4_)
return _loc4_
solver = Solver()
ans1 = [0x6ee2c371, 0x02f02daa, 0x417cfdf3]
ans2 = [0xad2a75a9, 0x70d4a3aa, 0x1fac0e9c]
n = 22
flag = [BitVec('x%d' % i, 8) for i in xrange(n)]
known = 'TMCTF{'
for i in xrange(len(known)):
solver.add(flag[i] == ord(known[i]))
for i in xrange(6, len(flag) - 1):
x = flag[i]
#solver.add(Or(And(48 <= x, x <= 57), And(97 <= x, x <= 122)))
solver.add(And(32 <= x, x <= 126))
for i, val1, val2 in zip(xrange(0, len(flag), 8), ans1, ans2):
s = flag[i:i+8]
res = fun_8(s)
solver.add(res == val1)
res = fun_7(s)
solver.add(res == val2)
print solver.check()
m = solver.model()
s = ''
for x in flag:
if str(m[x]) == 'None': continue
c = chr(int(str(m[x])))
s += c
print c
print s
最後有一點小雷是其實看不太出來 flag 長度應該要多少，因為程式中有把 username 每 8 個 byte 切開做運算，因此猜長度 24，但 z3 一直表示無解。最後把長度隨意改成 22 後就找到了。
Flag:
TMCTF{f1ash_s0_4un!!!}
