AIS3 Final-Exam Binary1

這題看到木棍用Pin炸，我都被嚇哭了啊...早知道就該學Pin惹Q___Q
題目長這樣：

分別給x86/x64各一種的Elf，可在Linux下跑起來測試
Pin的爆法/載點可以看木棍的Write-Up Sol.py
這邊我只把z3爆法的Code丟出來而已XD

先把x86的Elf丟給IDA Pro

題目只要求把傳入第一個參數（你的Key）丟給Verify函數檢測，如果正確就提示你Key正確
那麼可以看一下Verify怎麼寫的：
大致上可以從 i == 23推敲Key長度為23個ASCII（或者你可以從0x804A014得知第23個偏移為0x00得知Key長度為23個字）稍微整理一下可以得到底下這樣的函數：

bool verify(char* a1)
{
 for (int i = 0, j = 0, k = 0; i < 23; ++i)
 {
  j = *(char*)(0x804A014 + i);
  k = ((a1[i] ^ i) << (i ^ 9) & 3) | ((a1[i] ^ i) >> (8 - ((i ^ 9) & 3)))
  if (j!= k+ 8) return false;
 }
 return true;
}

所以最後可以根據我們手上資訊得知解題的要點：

1. Key有24個字（需要23個變量+已知結尾\x00來跑z3）

2. 0x804A014有一組char Array每個char - 8為ROR每個Key的ASCII才正確

接著可以去看0x804A014上保存的陣列資訊：

在IDA Pro中可透過Hex View看見0xCA為陣列起點，到0x63結尾，後面遇到0x00結束
最後就是把算法抄下來放進z3內用Python跑：

#!/usr/bin/env python2.7
#By aaaddress1.
from z3 import *

'''
IDA Pro F5
bool verify(char* a1)
{
  for (int i = 0, j = 0, k = 0; i < 23; i++)
  {
    j = *(char*)(0x804A014 + i);
    k = ((a1[i] ^ i) << (i ^ 9) & 3) | ((a1[i] ^ i) >> (8 - ((i ^ 9) & 3)))
    if (j!= k+ 8) return false;
  }
  return true;
}
'''

b = [ BitVec('b%d' % i, 32) for i in range(24)]
s = Solver()


cmparr = [ 0xca,0x70,0x93,0xc8,0x06,0x54,0xd2,0xd5,0xda,0x6a,0xd1,0x59,0xde,0x45,0xf9,0xb5,0xa6,0x87,0x19,0xa5,0x56,0x6e,0x63,00]
print(len(cmparr))
for i in range(24):
    tempChr = ((b[i] ^ i) << ((i ^ 9) & 3)) &0xff | ((b[i] ^ i)  >> (8 - ((i ^ 9) & 3)))
    s.add((cmparr[i] & 0xff) == tempChr +8)

print(s.check())
 
m = s.model()

res = ""
for i in range(24):
        g = m[b[i]]
        inta = int(str(g))
        res += chr(inta & 0xff)
 
print("Key is %s" % res)

終端機結果如下：