随缘做题 2333

程序带壳，用查壳工具没能查出来是什么壳，那这个应该是作者原创的，只能手工脱壳了，可是。。。。我不会脱壳，瞎捣腾一番，毫无结果。。。

在最后快要放弃的时候，尝试了一次投机的方法，运行程序，用OD附加，转到401000，然后dump，发现能dump！！！

这样就得到了疑似脱壳后的代码了，然后是字符串搜索，定位到sub_40679A()

其中sub_4074A3()如下

所以v0上的数据就是'Please enter the key: '

sub_40752A()的功能不清楚，不过看起来那么复杂，应该是库函数吧，根据实际就暂时把他当做printf之类的函数吧

找到调用sub_40679A的函数sub_407165()

这里的过程看上很怪。。。不过里面的函数有点特别，比如sub_40818E,sub_407918，sub_407E2F，他们的参数里都有一个函数地址，跟进分析这些函数地址，根据其代码，分析猜测其功能，然后推测出其验证过程：输入长度为12的字符串交由bf_vm验证。

bf_vm函数如下

这里输入的字符串会转成bit，然后程序根据预先准备好的bf代码生成字节码，然后再开始运行vm

bf_func函数如下

这里的功能跟bf的并没多大不同，只是case 5和case 6需要注意，case 5如下

case 6如下

试着把bf_data上的数据累加，发现和刚好为3600，那么综合分析可以知道，case 5的验证必须成功，而且次数刚好是bf_data的长度，不过当bit_add达到3600时，get_bf_input返回的数据有点变化，但现在还不知道有什么用，接下来就是对bf代码转义了

转义结果可以根据自己的语言习惯，我比较喜欢用Python，就按照python的格式来转义了

首先是常见的转义,代码如下

def cal(s):
	if '+' in s:
		return '+= %d'%len(s)
	else:
		return '-= %d'%len(s)
...
...
...
		pattern = re.compile(r'>+')
		match = pattern.match(s[p:])
		if match:
			p += len(match.group())
			ptr += len(match.group())
			continue
		pattern = re.compile(r'<+')
		match = pattern.match(s[p:])
		if match:
			p += len(match.group())
			ptr -= len(match.group())
			continue
		pattern = re.compile(r'\++')
		match = pattern.match(s[p:])
		if match:
			p += len(match.group())
			print tab+'mem[%d] %s'%(ptr,cal(match.group()))
			continue
		pattern = re.compile(r'-+')
		match = pattern.match(s[p:])
		if match:
			p += len(match.group())
			print tab+'mem[%d] %s'%(ptr,cal(match.group()))
			continue

然后是[]的转义

		c = s[p]
		if c == '[':
			stk = 1
			for i,v in enumerate(s[p+1:]):
				if v == '[':
					stk += 1
				elif v == ']':
					stk -= 1
				else:
					continue
				if stk == 0:
					print tab+'while mem[%d]:'%ptr
					ptr = bf2asm(s[p+1:p+1+i],ptr,tab+'\t')
					p += i+1
					break
			continue

这些比较好实现，这里[]的转义并不是正确的转义，只是根据实际情况简化了

然后是是.和,的转义，这个比较简单，根据程序来写就行了

执行代码，得到如下结果(部分)

while mem[144]:
	mem[144] -= 1
while mem[29]:
	mem[29] -= 1
while mem[51]:
	mem[51] -= 1
	mem[144] += 1
	mem[29] += 1
while mem[29]:
	mem[29] -= 1
	mem[51] += 1

虽然得到了转义代码，但是过程相对复杂，需要对其简化，比如上面的代码，仔细分析写就发现其过程就是

mem[144] = mem[51]
mem[29] = 0 #这部分可以不要

所以我们可以化简为

mem[144] = mem[51]

然后同样的对其他地方进行化简，我用到的化简如下

def sym2cal(s):
	if '>' in s:
		return len(s)
	else:
		return -len(s)
...
...
...
		pattern = re.compile(r'([><]*)\[-([><]*)\[-\]([><]+)\[-\]([><]+)\[-([><]+)\+([><]+)\+([><]+)\]([><]+)\[-([><]+)\+([><]+)\]([><]*)\[-([><]+)\+([><]+)\]([><]*)\]')
		match = pattern.match(s[p:])
		if match:
			p += len(match.group())
			groups = match.groups()
			ptr1 = ptr + sym2cal(groups[0])
			ptr2 = ptr1
			for i in xrange(1,4):
				ptr2 += sym2cal(groups[i])
			ptr3 = ptr2
			for i in xrange(4,12):
				ptr3 += sym2cal(groups[i])
			# print tab+'if mem[%d]:'%ptr1
			# print tab+tab+'mem[%d] sub 1'%ptr1
			# print tab+tab+'add mem[%d] mem[%d]'%(ptr3,ptr2)
			print tab+'mem[%d] += mem[%d]*mem[%d]'%(ptr3,ptr2,ptr1)
			for v in groups:
				ptr += sym2cal(v)
			continue
		
		pattern = re.compile(r'([><]*)\[-\]([><]+)\[-\]([><]+)\[-([><]+)\+([><]+)\+([><]+)\]([><]+)\[-([><]+)\+([><]+)\]([><]*)\[-([><]+)\+([><]+)\]')
		match = pattern.match(s[p:])
		if match:
			p += len(match.group())
			groups = match.groups()
			ptr1 = ptr
			for i in xrange(3):
				ptr1 += sym2cal(groups[i])
			ptr2 = ptr1
			for i in xrange(3,11):
				ptr2 += sym2cal(groups[i])
			# print tab+'add mem[%d] mem[%d]'%(ptr2,ptr1)
			print tab+'mem[%d] += mem[%d]'%(ptr2,ptr1)
			for v in groups:
				ptr += sym2cal(v)
			continue
		pattern = re.compile(r'([><]*)\[-\]([><]+)\[-\]([><]+)\[-([><]+)\+([><]+)\+([><]+)\]([><]+)\[-([><]+)\+([><]+)\]([><]+)')
		match = pattern.match(s[p:])
		if match:
			p += len(match.group())
			groups = match.groups()
			ptr1 = ptr + sym2cal(groups[0])
			ptr2 = ptr1 + sym2cal(groups[1])
			ptr3 = ptr2 + sym2cal(groups[2])
			# print tab+'mov mem[%d] mem[%d]'%(ptr1,ptr3)
			print tab+'mem[%d] = mem[%d]'%(ptr1,ptr3)
			for v in groups:
				ptr += sym2cal(v)
			continue
			
		pattern = re.compile(r'\[-\]')
		match = pattern.match(s[p:])
		if match:
			p += len(match.group())
			# print tab+'mov mem[%d] 0'%(ptr)
			print tab+'mem[%d] = 0'%(ptr)
			continue

这样得到的转义代码就好读多了，然后是算法分析，转义代码里有一段这样的代码

	mem[51] = 0
	mem[51] += 2
	mem[21] = mem[55]
	mem[20] = mem[51]
	mem[50] = mem[21]
	while mem[21]:
		mem[21] -= 1
		mem[20] -= 1
		mem[19] = mem[20]
		mem[18] += 1
		while mem[19]:
			mem[19] = 0
			mem[18] -= 1
		while mem[18]:
			mem[18] -= 1
			mem[50] = mem[21]
			mem[20] = mem[51]
	mem[55] = mem[50]
	cmp mem[55] data[data_ptr]

其实这个就是mem[55] %= 2，既然结果mod2，那么前面的一些操作都可以简化为mod2上的操作，比如加可以简化为异或，乘可以简化为与，这样分析出其验证过程，然后是用z3来求解了，求解代码见附件

得到flag

ToBeOrNot2Be

[CTF入门培训]顶尖高校博士及硕士团队亲授《30小时教你玩转CTF》，视频+靶场+题目！助力进入CTF世界