用例原始碼以及二進位制檔案連結：https://github.com/angr/angr-doc/tree/master/examples/defcon2016quals_baby-re

執行二進位制檔案，發現需要輸入13個字元，然後通過一系列計算判斷輸入字元是否滿足約束條件。

在IDA裡非常清晰可以看見輸入錯誤的字串及其呼叫地址：

所以avoid_addr=0x402941

而正確的字串以及地址為：

可以看出，flag將作為程式輸出，所以find_addr地址可以設定為0x40292c（親測有效）。

不過這一次就又對scanf函式進行了hook，用來建立13個符號變數。

這次是一定要hook scanf函式的。因為它預設會返回一個無約束的一個符號變數（是否是同一個符號變數還不確定），在scanf函式前面存在fflush函式，它的功能是清空緩衝區，將輸入寫入stream。

而且hook的函式，也出現了新的知識點：

	class my_scanf(angr.SimProcedure):
		def run(self, fmt, ptr):
			if 'scanf_count' not in self.state.globals:
				self.state.globals['scanf_count'] = 0
			c = self.state.globals['scanf_count']
			self.state.mem[ptr].dword = flag_chars[c]
			self.state.globals['scanf_count'] = c + 1
 

在符號執行的過程中，是可以建立變數的，儲存在state.globals裡面。這裡面就建立了一個變數scanf_count是記錄scanf函式的數目，使得第i個scanf函式的state.mem賦值第i個符號變數。

用例原始碼：

#!/usr/bin/env python2

"""
Author: David Manouchehri <[email protected]>
DEFCON CTF Qualifier 2016
Challenge: baby-re
Team: hack.carleton
Write-up: http://hack.carleton.team/2016/05/21/defcon-ctf-qualifier-2016-baby-re/
Runtime: ~8 minutes (single threaded E5-2650L v3 @ 1.80GHz on DigitalOcean)

DigitalOcean is horrible for single threaded applications, I would highly suggest using something else.
"""

import angr
import claripy

def main():
	proj = angr.Project('./baby-re',  load_options={'auto_load_libs': False})

	# let's provide the exact variables received through the scanf so we don't have to worry about parsing stdin into a bunch of ints.
	flag_chars = [claripy.BVS('flag_%d' % i, 32) for i in xrange(13)]
	class my_scanf(angr.SimProcedure):
		def run(self, fmt, ptr):
			if 'scanf_count' not in self.state.globals:
				self.state.globals['scanf_count'] = 0
			c = self.state.globals['scanf_count']
			self.state.mem[ptr].dword = flag_chars[c]
			self.state.globals['scanf_count'] = c + 1
	proj.hook_symbol('__isoc99_scanf', my_scanf(), replace=True)

	sm = proj.factory.simulation_manager()

	# search for just before the printf("%c%c...")
	# If we get to 0x402941, "Wrong" is going to be printed out, so definitely avoid that.
	sm.explore(find=0x4028E9, avoid=0x402941)

	# evaluate each of the flag chars against the constraints on the found state to construct the flag
	flag = ''.join(chr(sm.one_found.solver.eval(c)) for c in flag_chars)
	return flag

def test():
	assert main() == 'Math is hard!'

if __name__ == '__main__':
	print(repr(main()))