Excuse the ads! We need some help to keep our site up.
List
Information
Description
Get to reversing.
File
Source Code
Writeup
File information
lazenca0x0@ubuntu:~/CTF/DEFCON2016/baby's/baby-re$ file baby-re baby-re: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), dynamically linked (uses shared libs), for GNU/Linux 2.6.32, BuildID[sha1]=5d5783d23d78bf70b80d658bccbce365f7448693, not stripped lazenca0x0@ubuntu:~/CTF/DEFCON2016/baby's/baby-re$ checksec --file baby-re RELRO STACK CANARY NX PIE RPATH RUNPATH FORTIFY Fortified Fortifiable FILE Partial RELRO Canary found NX enabled No PIE No RPATH No RUNPATH Yes 0 2 baby-re
Binary analysis
Main
この問題は、ユーザーから13個の値を入力されています。
入力された値は、CheckSolution（）関数に渡されます。
この関数は、ユーザが入力した値が条件を満たせばFlagを出力するようになります。
main()
int __cdecl main(int argc, const char **argv, const char **envp)
{
int result; // eax@4
__int64 v4; // rbx@4
unsigned int v5[13]; // [rsp+0h] [rbp-60h]@1
__int64 v6; // [rsp+38h] [rbp-28h]@1
v6 = *MK_FP(__FS__, 40LL);
printf("Var[0]: ", argv, envp);
fflush(_bss_start);
__isoc99_scanf("%d", v5);
printf("Var[1]: ", v5);
fflush(_bss_start);
__isoc99_scanf("%d", &v5[1]);
printf("Var[2]: ", &v5[1]);
fflush(_bss_start);
__isoc99_scanf("%d", &v5[2]);
printf("Var[3]: ", &v5[2]);
fflush(_bss_start);
__isoc99_scanf("%d", &v5[3]);
printf("Var[4]: ", &v5[3]);
fflush(_bss_start);
__isoc99_scanf("%d", &v5[4]);
printf("Var[5]: ", &v5[4]);
fflush(_bss_start);
__isoc99_scanf("%d", &v5[5]);
printf("Var[6]: ", &v5[5]);
fflush(_bss_start);
__isoc99_scanf("%d", &v5[6]);
printf("Var[7]: ", &v5[6]);
fflush(_bss_start);
__isoc99_scanf("%d", &v5[7]);
printf("Var[8]: ", &v5[7]);
fflush(_bss_start);
__isoc99_scanf("%d", &v5[8]);
printf("Var[9]: ", &v5[8]);
fflush(_bss_start);
__isoc99_scanf("%d", &v5[9]);
printf("Var[10]: ", &v5[9]);
fflush(_bss_start);
__isoc99_scanf("%d", &v5[10]);
printf("Var[11]: ", &v5[10]);
fflush(_bss_start);
__isoc99_scanf("%d", &v5[11]);
printf("Var[12]: ", &v5[11]);
fflush(_bss_start);
__isoc99_scanf("%d", &v5[12]);
if ( (unsigned __int8)CheckSolution(v5) )
printf(
"The flag is: %c%c%c%c%c%c%c%c%c%c%c%c%c\n", v5[0], v5[1], v5[2], v5[3], v5[4], v5[5], v5[6], v5[7], v5[8], v5[9], v5[10], v5[11], v5[12]);
else
puts("Wrong");
result = 0;
v4 = *MK_FP(__FS__, 40LL) ^ v6;
return result;
}
CheckSolution
- この関数をHex-raysで開けると、次のようなErrorが発生します。
Warning
コード上にJunk codeが挿入されているのがエラーの原因です。
JUNK Code
- 除去しようとするコードを選択した後に"Edit"→"Patch program"→"Change byte..."機能を利用してJUNK Codeのbyte値を"00"に変更します。
JUNK Code変更前
JUNK Code変更後
- パッチの後Hex-Raysを利用して次のようなコードが確認できます。
- 当該関数は次のような機能をします。
- 渡された因子値を利用して与えられた演算を処理します。
- if()を利用して演算の結果値と条件値が同じかどうかを確認します。
- このような過程が13回反復されます。
- つまり、13つの条件文を満たすとFlag文字列を確認することができます。
CheckSolution(Remove JUNK Code)
__int64 __fastcall CheckSolution(_DWORD *a1)
{
__int64 result; // rax@2
__int64 v2; // rsi@26
if ( 39342 * a1[11]
+ 21090 * a1[10]
+ 14626 * a1[9]
+ 57693 * a1[8]
+ 16388 * a1[7]
+ 29554 * a1[6]
+ 43166 * a1[5]
+ 50633 * a1[4]
+ 37485 * *a1
- 21621 * a1[1]
- 1874 * a1[2]
- 46273 * a1[3]
+ 54757 * a1[12] == 21399379 )
{
if ( 22599 * a1[5]
+ 14794 * a1[4]
+ 38962 * a1[3]
+ 50936 * *a1
+ 4809 * a1[1]
- 6019 * a1[2]
- 837 * a1[6]
- 36727 * a1[7]
- 50592 * a1[8]
- 11829 * a1[9]
- 20046 * a1[10]
- 9256 * a1[11]
+ 53228 * a1[12] == 1453872 )
{
if ( 5371 * a1[11]
+ 42654 * a1[10]
+ 17702 * a1[8]
+ 26907 * a1[3]
+ -38730 * *a1
+ 52943 * a1[1]
- 16882 * a1[2]
- 44446 * a1[4]
- 18601 * a1[5]
- 65221 * a1[6]
- 47543 * a1[7]
- 33910 * a1[9]
+ 11469 * a1[12] == -5074020 )
{
if ( 8621 * a1[10]
+ 34805 * a1[7]
+ 10649 * a1[6]
+ 54317 * a1[4]
+ 57747 * *a1
- 23889 * a1[1]
- 26016 * a1[2]
- 25170 * a1[3]
- 32337 * a1[5]
- 9171 * a1[8]
- 22855 * a1[9]
- 634 * a1[11]
- 11864 * a1[12] == -5467933 )
{
if ( 15578 * a1[11]
+ 43186 * a1[9]
+ 28134 * a1[8]
+ 54889 * a1[4]
+ 34670 * a1[3]
+ 43964 * a1[2]
+ -14005 * *a1
+ 16323 * a1[1]
- 6141 * a1[5]
- 35427 * a1[6]
- 61977 * a1[7]
- 59676 * a1[10]
+ 50082 * a1[12] == 7787144 )
{
if ( 10305 * a1[11]
+ 29341 * a1[10]
+ 13602 * a1[7]
+ 39603 * a1[6]
+ 13608 * a1[2]
+ -40760 * *a1
- 22014 * a1[1]
- 4946 * a1[3]
- 26750 * a1[4]
- 31708 * a1[5]
- 59055 * a1[8]
- 32738 * a1[9]
- 15650 * a1[12] == -8863847 )
{
if ( 16047 * a1[9]
+ 55241 * a1[7]
+ 13477 * a1[2]
+ -47499 * *a1
+ 57856 * a1[1]
- 10219 * a1[3]
- 5032 * a1[4]
- 21039 * a1[5]
- 29607 * a1[6]
- 6065 * a1[8]
- 4554 * a1[10]
- 2262 * a1[11]
+ 18903 * a1[12] == -747805 )
{
if ( 41178 * a1[11]
+ 47909 * a1[7]
+ 53309 * a1[6]
+ -65419 * *a1
+ 17175 * a1[1]
- 9410 * a1[2]
- 22514 * a1[3]
- 52377 * a1[4]
- 9235 * a1[5]
- 59111 * a1[8]
- 41289 * a1[9]
- 24422 * a1[10]
- 23447 * a1[12] == -11379056 )
{
if ( 15699 * a1[10]
+ 58551 * a1[5]
+ 46767 * a1[4]
+ 33381 * a1[3]
+ 1805 * *a1
+ 4135 * a1[1]
- 16900 * a1[2]
- 34118 * a1[6]
- 44920 * a1[7]
- 11933 * a1[8]
- 20530 * a1[9]
- 36597 * a1[11]
+ 18231 * a1[12] == -166140 )
{
if ( 10788 * a1[10]
+ 18975 * a1[9]
+ 15033 * a1[8]
+ 42363 * a1[7]
+ 47052 * a1[6]
+ 41284 * a1[3]
+ -42941 * *a1
+ 61056 * a1[1]
- 45169 * a1[2]
- 1722 * a1[4]
- 26423 * a1[5]
- 33319 * a1[11]
+ 63680 * a1[12] == 9010363 )
{
if ( 30753 * a1[10]
+ 22613 * a1[9]
+ 58786 * a1[7]
+ 12587 * a1[6]
+ 12746 * a1[5]
+ -37085 * *a1
- 51590 * a1[1]
- 17798 * a1[2]
- 10127 * a1[3]
- 52388 * a1[4]
- 8269 * a1[8]
- 20853 * a1[11]
+ 32216 * a1[12] == -4169825 )
{
if ( 57612 * a1[11]
+ 47348 * a1[9]
+ 48719 * a1[8]
+ 9228 * a1[5]
+ 65196 * a1[4]
+ 36650 * *a1
+ 47566 * a1[1]
- 33282 * a1[2]
- 59180 * a1[3]
- 59599 * a1[6]
- 62888 * a1[7]
- 37592 * a1[10]
+ 40510 * a1[12] == 4081505 )
result = 25633 * a1[11]
+ 25252 * a1[9]
+ 28153 * a1[8]
+ 26517 * a1[7]
+ 59511 * a1[4]
+ 4102 * a1[3]
+ 51735 * *a1
+ 35879 * a1[1]
- 63890 * a1[2]
- 21386 * a1[5]
- 20769 * a1[6]
- 43789 * a1[10]
+ 7314 * a1[12] == 1788229;
else
result = 0LL;
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
}
else
{
result = 0LL;
}
v2 = *MK_FP(__FS__, 40LL) ^ *MK_FP(__FS__, 40LL);
return result;
}
structure of Exploit code
- "=="演算を満足する13つの値を入力します。
- 連立一次方程式(simultaneous linear equations)を利用して13つの値を探します。
Information for attack
"=="演算を満足する13つの値を探し("z3"Module(Python))
- 該当演算はMicrosoftで開発した"z3"Module(Python)を利用することができます。 まず、"z3"moduleのインストールが必要です。
z3 install
$ git clone https://github.com/Z3Prover/z3.git $ cd z3 $ python scripts/mk_make.py $ cd build $ make $ sudo make install
- 下記のように"z3"を利用して連立一次方程式問題を解いてみます。
z3 Example
from z3 import *
x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)
- 該当コードを実行すると、次のような結果を得ることができます。
python test2.py
lazenca0x0@ubuntu:~/CTF/DEFCON2016/baby's/baby-re$ python test2.py [y = 0, x = 7]
- このプログラムで使用された連立方程式も次のように解くことができます
test.py
from z3 import *
a1 = [Int("a1[%d]"%(i)) for i in range(0,13)]
s = Solver()
s.add(39342 * a1[11]
+ 21090 * a1[10]
+ 14626 * a1[9]
+ 57693 * a1[8]
+ 16388 * a1[7]
+ 29554 * a1[6]
+ 43166 * a1[5]
+ 50633 * a1[4]
+ 37485 * a1[0]
- 21621 * a1[1]
- 1874 * a1[2]
- 46273 * a1[3]
+ 54757 * a1[12] == 21399379)
s.add(22599 * a1[5]
+ 14794 * a1[4]
+ 38962 * a1[3]
+ 50936 * a1[0]
+ 4809 * a1[1]
- 6019 * a1[2]
- 837 * a1[6]
- 36727 * a1[7]
- 50592 * a1[8]
- 11829 * a1[9]
- 20046 * a1[10]
- 9256 * a1[11]
+ 53228 * a1[12] == 1453872)
s.add(5371 * a1[11]
+ 42654 * a1[10]
+ 17702 * a1[8]
+ 26907 * a1[3]
+ -38730 * a1[0]
+ 52943 * a1[1]
- 16882 * a1[2]
- 44446 * a1[4]
- 18601 * a1[5]
- 65221 * a1[6]
- 47543 * a1[7]
- 33910 * a1[9]
+ 11469 * a1[12] == -5074020)
s.add(8621 * a1[10]
+ 34805 * a1[7]
+ 10649 * a1[6]
+ 54317 * a1[4]
+ 57747 * a1[0]
- 23889 * a1[1]
- 26016 * a1[2]
- 25170 * a1[3]
- 32337 * a1[5]
- 9171 * a1[8]
- 22855 * a1[9]
- 634 * a1[11]
- 11864 * a1[12] == -5467933)
s.add(15578 * a1[11]
+ 43186 * a1[9]
+ 28134 * a1[8]
+ 54889 * a1[4]
+ 34670 * a1[3]
+ 43964 * a1[2]
+ -14005 * a1[0]
+ 16323 * a1[1]
- 6141 * a1[5]
- 35427 * a1[6]
- 61977 * a1[7]
- 59676 * a1[10]
+ 50082 * a1[12] == 7787144)
s.add(10305 * a1[11]
+ 29341 * a1[10]
+ 13602 * a1[7]
+ 39603 * a1[6]
+ 13608 * a1[2]
+ -40760 * a1[0]
- 22014 * a1[1]
- 4946 * a1[3]
- 26750 * a1[4]
- 31708 * a1[5]
- 59055 * a1[8]
- 32738 * a1[9]
- 15650 * a1[12] == -8863847)
s.add(16047 * a1[9]
+ 55241 * a1[7]
+ 13477 * a1[2]
+ -47499 * a1[0]
+ 57856 * a1[1]
- 10219 * a1[3]
- 5032 * a1[4]
- 21039 * a1[5]
- 29607 * a1[6]
- 6065 * a1[8]
- 4554 * a1[10]
- 2262 * a1[11]
+ 18903 * a1[12] == -747805 )
s.add(41178 * a1[11]
+ 47909 * a1[7]
+ 53309 * a1[6]
+ -65419 * a1[0]
+ 17175 * a1[1]
- 9410 * a1[2]
- 22514 * a1[3]
- 52377 * a1[4]
- 9235 * a1[5]
- 59111 * a1[8]
- 41289 * a1[9]
- 24422 * a1[10]
- 23447 * a1[12] == -11379056)
s.add(15699 * a1[10]
+ 58551 * a1[5]
+ 46767 * a1[4]
+ 33381 * a1[3]
+ 1805 * a1[0]
+ 4135 * a1[1]
- 16900 * a1[2]
- 34118 * a1[6]
- 44920 * a1[7]
- 11933 * a1[8]
- 20530 * a1[9]
- 36597 * a1[11]
+ 18231 * a1[12] == -166140)
s.add(10788 * a1[10]
+ 18975 * a1[9]
+ 15033 * a1[8]
+ 42363 * a1[7]
+ 47052 * a1[6]
+ 41284 * a1[3]
+ -42941 * a1[0]
+ 61056 * a1[1]
- 45169 * a1[2]
- 1722 * a1[4]
- 26423 * a1[5]
- 33319 * a1[11]
+ 63680 * a1[12] == 9010363)
s.add(30753 * a1[10]
+ 22613 * a1[9]
+ 58786 * a1[7]
+ 12587 * a1[6]
+ 12746 * a1[5]
+ -37085 * a1[0]
- 51590 * a1[1]
- 17798 * a1[2]
- 10127 * a1[3]
- 52388 * a1[4]
- 8269 * a1[8]
- 20853 * a1[11]
+ 32216 * a1[12] == -4169825)
s.add(57612 * a1[11]
+ 47348 * a1[9]
+ 48719 * a1[8]
+ 9228 * a1[5]
+ 65196 * a1[4]
+ 36650 * a1[0]
+ 47566 * a1[1]
- 33282 * a1[2]
- 59180 * a1[3]
- 59599 * a1[6]
- 62888 * a1[7]
- 37592 * a1[10]
+ 40510 * a1[12] == 4081505)
s.add(25633 * a1[11]
+ 25252 * a1[9]
+ 28153 * a1[8]
+ 26517 * a1[7]
+ 59511 * a1[4]
+ 4102 * a1[3]
+ 51735 * a1[0]
+ 35879 * a1[1]
- 63890 * a1[2]
- 21386 * a1[5]
- 20769 * a1[6]
- 43789 * a1[10]
+ 7314 * a1[12] == 1788229)
print s.check()
m = s.model()
for d in m.decls():
print "%s = %s" %(d.name(),m[d])
- 該当コードを実行すると、次のような結果が出力されます。
python test.py
lazenca0x0@ubuntu:~/CTF/DEFCON2016/baby's/baby-re$ python test.py sat a1[3] = 104 a1[7] = 32 a1[9] = 97 a1[6] = 115 a1[0] = 77 a1[10] = 114 a1[12] = 33 a1[11] = 100 a1[8] = 104 a1[1] = 97 a1[4] = 32 a1[5] = 105 a1[2] = 116
- 出力された結果を再整理すると、次のようです。
Flag string
| a1[0] | 77 | a1[7] | 32 |
|---|---|---|---|
| a1[1] | 97 | a1[8] | 104 |
| a1[2] | 116 | a1[9] | 97 |
| a1[3] | 104 | a1[10] | 114 |
| a1[4] | 32 | a1[11] | 100 |
| a1[5] | 105 | a1[12] | 33 |
| a1[6] | 115 |
"=="演算を満足する13つの値を探し(angr)
- 該当の問題はangrを利用しても問題を解決することができます。
- ソースコードは次のようです。
solve.py
#!/usr/bin/env python2
"""
Author: David Manouchehri <manouchehri@protonmail.com>
DEFCON CTF Qualifier 2016
Challenge: baby-re
Team: hack.carleton
Write-up: http://hack.carleton.team/2016/05/21/defcon-ctf-qualifier-2016-baby-re/
Runtime: ~8 minutes (single threaded E5-2650L v3 @ 1.80GHz on DigitalOcean)
DigitalOcean is horrible for single threaded applications, I would highly suggest using something else.
"""
import angr
def main():
proj = angr.Project('./baby-re', load_options={'auto_load_libs': False})
path_group = proj.factory.path_group(threads=4) # Doesn't really help to have more threads, but whatever.
path_group.explore(find=0x40294b, avoid=0x402941)
return path_group.found[0].state.posix.dumps(1) # The flag is at the end.
def test():
assert 'Math is hard!' in main()
if __name__ == '__main__':
print(repr(main()))
anrg Example
- 該当コードの主要内容は"path_group.explore()"です。
- 13個の全てのif()の条件が満たされれば、当該プログラムは"0x40294b"領域に移動します。
- 該当アドレスを"find"に保存しなければなりません。(find=0x40294b)
- if()の条件が満たされなければ、当該プログラムは"0x402941"領域に移動します。
- 該当アドレスを"avoid"に保存しなければなりません。(avoid=0x402941)
- 13個の全てのif()の条件が満たされれば、当該プログラムは"0x40294b"領域に移動します。
- 前のコードを実行すると、次のような結果を得ることができます。
python test3.py
$ mkvirtualenv angr New python executable in angr/bin/python Installing setuptools, pip...done. (angr)$ python test3. WARNING | 2016-08-08 00:37:13,869 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2016-08-08 00:37:15,772 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2016-08-08 00:37:18,286 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2016-08-08 00:37:22,451 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2016-08-08 00:37:28,217 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2016-08-08 00:37:36,537 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2016-08-08 00:37:49,255 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2016-08-08 00:38:06,851 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2016-08-08 00:38:28,900 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2016-08-08 00:38:57,506 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2016-08-08 00:39:29,892 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2016-08-08 00:40:20,124 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. WARNING | 2016-08-08 00:41:10,223 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing. 'Var[0]: Var[1]: Var[2]: Var[3]: Var[4]: Var[5]: Var[6]: Var[7]: Var[8]: Var[9]: Var[10]: Var[11]: Var[12]: The flag is: Math is hard!\n' (angr)$
Exploit Code
Exploit code
from pwn import *
p = process("./baby-re")
def CharInput(ch):
p.recvuntil(':')
p.sendline(str(ch))
CharInput(77)
CharInput(97)
CharInput(116)
CharInput(104)
CharInput(32)
CharInput(105)
CharInput(115)
CharInput(32)
CharInput(104)
CharInput(97)
CharInput(114)
CharInput(100)
CharInput(33)
print p.recvuntil("The flag is:") + p.recv()
Flag
| Flag |
|---|
Excuse the ads! We need some help to keep our site up.