Page History

Panel

Excuse the ads! We need some help to keep our site up.

List

Table of Contents

outline	true

Information

Description

Panel

Get to reversing.

baby-re

File

Panel
baby-re

Source Code

Panel
https://github.com/legitbs/quals-2016/tree/master/baby-re

...

Writeup

File information

Code Block

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を出力するようになります。

Code Block

language	cpp
title	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が発生します。

Panel

title	Warning

Image Modified

コード上にJunk codeが挿入されているのがエラーの原因です。

Panel

title	JUNK Code

Image Modified

除去しようとするコードを選択した後に"Edit"→"Patch program"→"Change byte..."機能を利用してJUNK Codeのbyte値を"00"に変更します。

Panel

title	JUNK Code変更前

Image Modified

Panel

title	JUNK Code変更後

Image Modified

パッチの後Hex-Raysを利用して次のようなコードが確認できます。
当該関数は次のような機能をします。
- 渡された因子値を利用して与えられた演算を処理します。
- if()を利用して演算の結果値と条件値が同じかどうかを確認します。
  - このような過程が13回反復されます。
- つまり、13つの条件文を満たすとFlag文字列を確認することができます。

Code Block

language	cpp
title	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

Panel
"=="演算を満足する13つの値を入力します。連立一次方程式(simultaneous linear equations)を利用して13つの値を探します。

...

Information for attack

"=="演算を満足する13つの値を探し("z3"Module(Python))

該当演算はMicrosoftで開発した"z3"Module(Python)を利用することができます。まず、"z3"moduleのインストールが必要です。

Code Block

title	z3 install

$ git clone https://github.com/Z3Prover/z3.git
$ cd z3
$ python scripts/mk_make.py
$ cd build
$ make
$ sudo make install

Info

title	Github

https://github.com/Z3Prover/z3

下記のように"z3"を利用して連立一次方程式問題を解いてみます。

Code Block

language	py
title	z3 Example

from z3 import *

x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)

該当コードを実行すると、次のような結果を得ることができます。

Code Block

title	python test2.py

lazenca0x0@ubuntu:~/CTF/DEFCON2016/baby's/baby-re$ python test2.py 
[y = 0, x = 7]

Info

title	Z3 API in Python

http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/guide-examples.htm

このプログラムで使用された連立方程式も次のように解くことができます

Code Block

language	py
title	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])

該当コードを実行すると、次のような結果が出力されます。

Code Block

title	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

出力された結果を再整理すると、次のようです。

Panel

title	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を利用しても問題を解決することができます。
ソースコードは次のようです。
- 該当コードはhttps://docs.angr.io/docs/examples.htmlに公開されたコードです。

Code Block

title	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()))

Info

title	anrg Example

該当コードの主要内容は"path_group.explore()"です。
- 13個の全てのif()の条件が満たされれば、当該プログラムは"0x40294b"領域に移動します。
  - 該当アドレスを"find"に保存しなければなりません。(find=0x40294b)
- if()の条件が満たされなければ、当該プログラムは"0x402941"領域に移動します。
  - 該当アドレスを"avoid"に保存しなければなりません。(avoid=0x402941)

Panel
Image Modified

前のコードを実行すると、次のような結果を得ることができます。

Code Block

title	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

Code Block

language	py
title	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

...

Panel

...

Excuse the ads! We need some help to keep our site up.

Related Site

...

Page tree

Versions Compared

Old Version 3

New Version Current

Key

List

Information

Description

File

Source Code

Writeup

File information

Binary analysis

Main

CheckSolution

structure of Exploit code

Information for attack

"=="演算を満足する13つの値を探し("z3"Module(Python))

"=="演算を満足する13つの値を探し(angr)

Exploit Code

Flag

Related Site