[DEFCONCTF Quals 2016]: baby-re – Static Analysis + z3

Challenge:

Get to reversing.

File.

 

Pertama, kita mulai dengan menjalankan file.

Terlihat bahwa program meminta 13 variabel.

Selanjutnya saya mendekompilasi program tersebut dengan menggunakan IDA:

Disitu terlihat ada function CheckSolution yang tidak dapat didekompilasi secara lengkap. Hal ini disebabkan karena return address yang hilang/ tidak ada dalam frame. Kita dapat memperbaiki ini dengan meng-undefine function tersebut (klik kanan > undefine):

Lalu kita meng-cast ulang function tersebut (klik kanan > Code), dan membuat ulang function (klik kanan > Create function). Setelah itu, saya mencoba melakukan dekompilasi ulang.

Di function tersebut terlihat constraint yang digunakan untuk mengecek input 13 variabel. Selanjutnya saya menggunakan constraint tersebut dan z3 untuk mendapatkan flag.

Hasilnya:

Flag:

[Math is hard!]

Leave a Reply

Your email address will not be published. Required fields are marked *