Kao的toy project是一个非常棒的crackme，非常适合展示符号执行的力量。运行crackme提供了一个安装ID，我们需要输入一个解锁代码。 
这里的安装ID本来应该是XXXXXXXXXXXXXXXX-XXXXXXXXXXXXXXXX-XXXXXXXXXXXXXXXX-XXXXXXXXXXXXXXXX的形式，不知道为什么没有显示完整，可以下个断点查看完整的安装ID。安装ID由硬盘序列号计算生成，我们不会专注于生成安装ID的算法，而是开发在给定安装ID时计算解锁代码的keygen。crackme的核心在于下面这个检查给定的解锁代码是否有效的函数。 
.text:004010EC ; int __stdcall check(int part1, int part2)
.text:004010EC check proc near ; CODE XREF: DialogFunc+104p
.text:004010EC
.text:004010EC output = byte ptr -21h
.text:004010EC part1 = dword ptr 8
.text:004010EC part2 = dword ptr 0Ch
.text:004010EC
.text:004010EC push ebp
.text:004010ED mov ebp, esp
.text:004010EF add esp, 0FFFFFFDCh
.text:004010F2 mov ecx, 32
.text:004010F7 mov esi, offset installId
.text:004010FC lea edi, [ebp+output]
.text:004010FF mov edx, [ebp+part1]
.text:00401102 mov ebx, [ebp+part2]
.text:00401105
.text:00401105 encode: ; CODE XREF: check+23j
.text:00401105 lodsb
.text:00401106 sub al, bl
.text:00401108 xor al, dl
.text:0040110A stosb
.text:0040110B rol edx, 1
.text:0040110D rol ebx, 1
.text:0040110F loop encode
.text:00401111 mov byte ptr [edi], 0
.text:00401114 push offset String2 ; "0how4zdy81jpe5xfu92kar6cgiq3lst7"
.text:00401119 lea eax, [ebp+output]
.text:0040111C push eax ; lpString1
.text:0040111D call lstrcmpA
.text:00401122 leave
.text:00401123 retn 8
.text:00401123 check endp
.text:00401123
.text:00401126该函数需要两个dword(来自解锁代码)作为参数用于将安装ID(明文)加密到给定的输出缓冲区(密文)。对于被验证的我们输入的解锁代码，加密后的输出必须与硬编码的字符串0how4zdy81jpe5xfu92kar6cgiq3lst7匹配。
用Z3解决
from z3 import *
import binascii
import sys
# Calculates the installation id from the entered string
# This function just reverses the order of dwords in each quadword
def getInstallIdFromString(iid_string):
qword1, qword2, qword3, qword4 = iid_string.split('-')
dword1 = list(binascii.unhexlify(qword1))[3::-1]
dword2 = list(binascii.unhexlify(qword1))[7:3:-1]
dword3 = list(binascii.unhexlify(qword2))[3::-1]
dword4 = list(binascii.unhexlify(qword2))[7:3:-1]
dword5 = list(binascii.unhexlify(qword3))[3::-1]
dword6 = list(binascii.unhexlify(qword3))[7:3:-1]
dword7 = list(binascii.unhexlify(qword4))[3::-1]
dword8 = list(binascii.unhexlify(qword4))[7:3:-1]
return map(ord, dword1 + dword2 + dword3 + dword4 + dword5 + dword6 + dword7 + dword8)
def main():
sss=2
print ("He is %d years old"%(sss))
if len(sys.argv) < 2:
print ("Please provide the installation id as an argument")
return
# Sanity Check
assert len(sys.argv[1]) == 16*4+3
install_id = getInstallIdFromString(sys.argv[1])
# The install id must encode to this hardcoded string
target = map(ord, list('0how4zdy81jpe5xfu92kar6cgiq3lst7'))
s = Solver()
# The two parts of the unlock code
part1 = edx = BitVec('part1', 32)
part2 = ebx = BitVec('part2', 32)
for i in xrange(32):
# text:00401105 lodsb
byte = install_id[i]
# text:00401106 sub al, bl
byte -= Extract(7, 0, ebx)
# text:00401108 xor al, dl
byte ^= Extract(7, 0, edx)
# text:0040110B rol edx, 1
edx = RotateLeft(edx, 1)
# text:0040110D rol ebx, 1
ebx = RotateLeft(ebx, 1)
# Add constraint
s.add(byte == target[i])
# Solve the system
if s.check() == sat:
m = s.model()
print ('%08X-%08X' %(m[part1].as_long(), m[part1].as_long () ^ m[part2].as_long()))
if __name__ == '__main__':
main()这份代码把安装ID做为命令行参数，让我们详细看看。
install_id = getInstallIdFromString(sys.argv[1])这里我们将安装ID转换为正确的形式，即每个QWORD中的两个DWORD的顺序被反转，并作为整数列表返回。
target = map(ord, list('0how4zdy81jpe5xfu92kar6cgiq3lst7'))安装ID被加密之后必须与硬编码的字符串相匹配，在这里我们将该字符串转换为由每个字符ASCII值表示的字符列表。
part1 = edx = BitVec('part1', 32)
part2 = ebx = BitVec('part2', 32) 我们声明两个大小为32位的位向量，这两个位向量表示解锁码的两个DWORDS。
for i in xrange(32):
# text:00401105 lodsb
byte = install_id[i]
# text:00401106 sub al, bl
byte -= Extract(7, 0, ebx)
# text:00401108 xor al, dl
byte ^= Extract(7, 0, edx)
# text:0040110B rol edx, 1
edx = RotateLeft(edx, 1)
# text:0040110D rol ebx, 1
ebx = RotateLeft(ebx, 1)
# Add constraint
s.add(byte == target[i])上述的循环描述了编码过程，install_id的每个字符都被处理，该值必须与目标列表中的相应字符匹配。为此，我们使用约束。
# Solve the system
if s.check() == sat:
m = s.model()
print ('%08X-%08X' %(m[part1].as_long(), m[part1].as_long () ^ m[part2].as_long()))最后，我们让z3来解决这个问题并打印答案。 
用angr解决
让我们再次看看程序控制流。 
程序在40122A处将调用check函数，如果我们输入的解锁码是正确的check将返回1并将转到401234的绿色基本块显示成功的消息。现在我们看看check函数的程序控制流。 
我们将符号化地执行上述功能。由两部分组成的解锁代码作为参数传递给函数，由于我们孤立地执行这个函数，所以需要自己提供输入，这可以通过在4010FF(set_ebx_edx)设置一个hook来实现。在hook中，我们将代表解锁码两部分的符号值存储到ebx和edx寄存器中。最后在40111D调用了lstrcmpA，这个功能是从kernel32.dll导入的。我们的执行环境中没有加载这个dll，可以使用SimProcedures模拟lstrcmpA的行为。 
现在看看实现所有这些的代码。
import angr
import simuvex
import binascii
import sys
part1 = None
part2 = None
# Calculates the installation id from the entered string
# This function just reverses the order of dwords in each quadword
def getInstallIdFromString(iid_string):
qword1, qword2, qword3, qword4 = iid_string.split('-')
dword1 = list(binascii.unhexlify(qword1))[3::-1]
dword2 = list(binascii.unhexlify(qword1))[7:3:-1]
dword3 = list(binascii.unhexlify(qword2))[3::-1]
dword4 = list(binascii.unhexlify(qword2))[7:3:-1]
dword5 = list(binascii.unhexlify(qword3))[3::-1]
dword6 = list(binascii.unhexlify(qword3))[7:3:-1]
dword7 = list(binascii.unhexlify(qword4))[3::-1]
dword8 = list(binascii.unhexlify(qword4))[7:3:-1]
return ''.join(dword1 + dword2 + dword3 + dword4 + dword5 + dword6 + dword7 + dword8)
def set_ebx_edx(state):
global part1, part2
state.regs.edx = part1
state.regs.ebx = part2
def main(iid_string):
global part1, part2
angr.path_group.l.setLevel('DEBUG')
# Calculate the install id from the string
install_id = getInstallIdFromString(iid_string)
# Load the binary
proj = angr.Project('toyproject.exe', load_options={'auto_load_libs': False})
# Hook strcmp
proj.hook(0x40130E, simuvex.SimProcedures['libc.so.6']['strcmp'], length=5)
# Create a blank state at 0x40122A i.e where check function is called
initial_state = proj.factory.blank_state(addr=0x40122A)
# The two parts of the serial
part1 = initial_state.se.BVS('part1', 32)
part2 = initial_state.se.BVS('part2', 32)
# Store the install id in memory
initial_state.memory.store(0x4093A8, install_id)
# Hook to set ebx and edx registers
proj.hook(0x4010ff, set_ebx_edx, length=6)
pg = proj.factory.path_group(initial_state)
# Go, go
pg.explore(find=0x401234, avoid=0x401249)
found_state = pg.found[0].state
p1 = found_state.se.any_int(part1)
p2 = found_state.se.any_int(part2)
print ('%08X-%08X' %(p1, p1^p2))
if __name__ == '__main__':
if len(sys.argv) < 2:
print 'Please provide the installation id as an arguement'
else:
# Sanity check
assert len(sys.argv[1]) == 16*4+3
main(sys.argv[1])
原文地址：https://0xec.blogspot.jp/2016/04/solving-kaos-toy-project-with-symbolic.html