Dragon CTF 2018 Fast Storage Writeup // Swing'Blog 浮生若梦

BEGIN_PAYLOAD20181001

周末随意看了 Dragon CTF 2018 的题，主要看了两个 Pwn。两个都挺有意思的，但是这个题有个冷门知识。所以想稍微记录下。

0x01 abs(0x8000000) == 0x8000000

首先，我们先了解下 abs 这个函数。

NAME
       abs, labs, llabs, imaxabs - compute the absolute value of an integer

SYNOPSIS
       #include <stdlib.h>

       int abs(int j);
       long int labs(long int j);
       long long int llabs(long long int j);

       #include <inttypes.h>

       intmax_t imaxabs(intmax_t j);

   Feature Test Macro Requirements for glibc (see feature_test_macros(7)):

       llabs():
           _ISOC99_SOURCE || _POSIX_C_SOURCE >= 200112L

DESCRIPTION
       The  abs()  function  computes  the  absolute value of the integer argument j.  The labs(),
       llabs() and imaxabs() functions compute the absolute value of the argument j of the  appro-
       priate integer type for the function.

RETURN VALUE
       Returns the absolute value of the integer argument, of the appropriate integer type for the
       function.

我们可以知道， abs 返回的参数是 inter。

我们也知道 inter 的范围如下表：

类型	字节	范围
short int	2byte(word)	032767(00x7fff) -32768-1(0x80000xffff)
unsigned short int	2byte(word)	065535(00xffff)
int	4byte(dword)	02147483647(00x7fffffff) -2147483648-1(0x800000000xffffffff)
unsigned int	4byte(dword)	04294967295(00xffffffff)
long int	8byte(qword)	正: 00x7fffffffffffffff 负:0x80000000000000000xffffffffffffffff
unsigned long int	8byte(qword)	0~0xffffffffffffffff

int 的表示范围为 02147483647(00x7fffffff) -2147483648-1(0x800000000xffffffff) , 以 常理而言， abs 这个取绝对值的函数，返回的应该是正数吧…

然后这里的 asb(0x80000000) == 0x80000000 这是为什么？ （inter : 0x80000000 == -2147483648)

**Why? **

单纯从二进制来看：

bin(0x80000000)
‘0b10000000000000000000000000000000’

0x80000000 == 10000000000000000000000000000000

但是 32bit的 整型数实际上只以 31 位表示，最高位表示符号。换一句话说，0x80000000 溢出，覆盖到了 符号位。在 32bit 整型中，如果是负整数的话，则要将后面的31个二进制位取反加1之后才是其绝对值。

换一句话说 ~0 +1 == 0 。那么 abs(0x8000000)==0x8000000 并不是没有道理。

0x02 利用思路

_DWORD *__fastcall calculation(__int64 data, __int64 value)
{
  int v2; // ST1C_4
  char v3; // ST18_1
  char v4; // ST14_1
  int idx; // ST1C_4

  v2 = hash1(data);
  v3 = hahs2(data);
  v4 = hash3(data);
  idx = abs(v2) % 62;
  link(idx, data, value);
  return add_bitmap(idx, v3, v4);
}

如果 abs(v1 ) 返回 0x8000000 ，那么取模后， v4 的值实际上等于 -2

.bss:0000555555756040 ; _DWORD name_arrary[64]
.bss:0000555555756040 name_arrary     dd 40h dup(?)           ; DATA XREF: add_bitmap+D↑o
.bss:0000555555756040                                         ; add_bitmap+3D↑o ...
.bss:0000555555756140 ; _QWORD list[62]
.bss:0000555555756140 list  

这样我们可以 bitmap 和 list 重合。

0x3 code exploit

首先，我们得先得到一个 0x8000000。

➜  /tmp python solve.py
sat
[d = 169, c = 230, a = 161, b = 248]
➜  /tmp cat solve.py
#!/usr/bin/env python
# coding=utf-8
from z3 import *
s = Solver()
a = BitVec("a", 32)
b = BitVec("b", 32)
c = BitVec("c", 32)
d = BitVec("d", 32)
s.add(a<256,b<256,c<256,d<256)
s.add(a>0,b>0,c>0,d>0)
s.add((((0x1337*a+1)*b+1)*c+1)*d==0x7fffffff)
print(s.check())
print(s.model())
➜  /tmp python
Python 2.7.12+ (default, Sep 17 2016, 12:08:02)
[GCC 6.2.0 20160914] on linux2
Type "help", "copyright", "credits" or "license" for more information.
>>> a = 161
>>> b = 248
>>> c = 230
>>> d = 169
>>> hex((((0x1337*a+1)*b+1)*c+1)*d)
'0x6f17fffffff'
>>> hex((((0x1337*a+1)*b+1)*c+1)*d+1)
'0x6f180000000'

所以，我这里字符串 取 \xa1\xf8\xe6\xa9

剩下的利用 参考 https://xz.aliyun.com/t/2831#toc-2

EOFCHECKSUM_OK