数学43分男，携Ghidra & Angr，怒战超复杂公式！

官方公众号企业安全新浪微博

FreeBuf.COM网络安全行业门户，每日发布专业的安全资讯、技术剖析。

FreeBuf+小程序把安全装进口袋

活动

^{0
1
2
3
4
5
6
7
8
9
0
1
2
3
4
5
6
7
8
9
0
1
2
3
4
5
6
7
8
9}

数学43分男，携Ghidra & Angr，怒战超复杂公式！

虫一卜 2025-02-20 15:17:44 117330

所属地湖北省

本文由虫一卜创作，已纳入「FreeBuf原创奖励计划」，未授权禁止转载

大家好，又是我，虫一卜，long time no see。

事情是这样的，有一个CTF程序(every_bit_counts)需要一个长度52位的密码（flag），而这一条长度为52位的密码（flag），并不是某种形式硬编码在程序里面的，而是这长度为52位的密码（flag），必须要满足一个超长公式，想要破解这一条密码（flag），就必须求解出满足所有公式的值。那这条公式究竟有多长呢。请看下图中这条公式的长度，透过Ghidra提取出来的反编译代码。我们可以看到，呃..也就这么亿....点点长吧。

做为一个数学曾经考过43分的男人，心里可是惊慌的一批。不过做为一条赛博赌狗，循规蹈矩稳扎稳打，向来不是我的风格，投机取巧，以小博大才是向往。接下来就一起看一看，赛博赌狗如何挑战超长公式，破解公式中52位长度的密码（flag）。

0x1：信息收集

首先运行这个CTF程序，可以从下图中看到这个程序是需要flag作为密码的，程序首先会判断密码（flag）长度是否符合要求，不符则跳出长度不符的错误提示。长度符合要求，则开始判断密码（flag）正确与否。不对则跳出错误提示，反之正确提示，也就意味着flag正确，可以去页面提交flag。

接下来还是直接看这个程序的反编译代码，程序我已经导入了Ghidra，这个程序是有main函数的，直接搜索main函数前往main函数。前往main函数以后可以看到文章开头图中提到的超长公式。这里的main函数的伪代码，我已经提前进行了简单的优化。

透过伪代码可以看到，首先会判断程序是否有参数，也就是程序后面有没跟上的密码作为参数。如果用户运行程序的时候，加上了密码作为参数，则继续执行下面的密码长度判断，这里的16进制值0x34是十进制52。也就是说密码（flag）的长度必须是52位。

如果你输入的密码（flag）长度满足条件，接下来会判断密码（flag）中的各字符是否满足超长公式。如果满足则可以到下图这里，也就是我们需要的正确提示。如果不满足以上公式的话，则会跳出错误提示。下面还有一个打印密码（flag）长度不符的错误提示和一个未输入密码（flag）的提示。

大致分析了这个CTF程序的伪代码，接下来推测一下密码是如何套进公式里面的。假设有一个密码字符串，这一条字符串里面的每一个ASCII字符，都是一个字节，都会有一个字节值。将这一串密码字符串作为数组，每一个字符又都会有一个索引，通过索引指针调用这长串字符里面的每一个字符的字节值，然后带入超长公式里面进行判断，如果这52个字符完全满足公式里面的各个条件，那这一组52字符长度的字符串，就是这个程序的正确密码（flag）。这像极了一道数学求解题，公式已知，我们需要找到满足公式的密码。

0x2：符号执行&符号求解

做为一个数学考过43分的男人，是不可能跟这么长的公式硬刚的，这辈子都不可能的。至于这种脏活累活计算活，还得是脚本来干。实现鸽鸽不用动，脚本全自动。有请Angr 和 Claripy登场。Angr的安装比较简单，使用pip就可以安装，这里就不赘述了。

程序并不复杂，分支并不多，通过符号执行，是有很大的可能性到达正确提示分支的。如果符号执行可以到达正确提示分支，透过Angr一路上收集的约束条件，约束求解就可以算出正确密码。话不多说，上脚本代码。

#!/usr/bin/env python3

import angr
import claripy

project = angr.Project("every_bit_counts")
argv1 = claripy.BVS("happy", 52 * 8)
initial_state = project.factory.entry_state(args=["./every_bit_counts", argv1])
sm = project.factory.simulation_manager(initial_state)
sm.explore(find=0x4035C2)
found = sm.found[0]
solution = found.solver.eval(argv1, cast_to=bytes)
print(repr(solution))

首先导入angr和claripy，接下来新建一个angr工程，指向我们的可执行文件。工程文件新建以后，接下来构造位向量符号作为密码（flag），作为参数1传递给程序，这里使用claripy.BVS()来构造位向量符号。符号变量名称可以任意，这里使用happy。因为位向量使用的是最小单位比特，而密码为长度为52字节，所以这里需要乘8。

有了位向量作为程序的参数，接下来使用angr的初始化状态，来调用这个参数。这里使用project.factory.entry_state()方法，使用刚刚生成的位向量符号作为参数，传递给程序进行模拟运行。参数构造好以后，接下来我们就要使用模拟管理器，模拟运行这个程序。使用project.factory.simulation_manager()模拟运行刚刚的状态。

模拟执行程序以后，我们就需要让模拟器去探索，找到程序正确提示所在的地址分支。回到Ghidra可以看到程序打印正确提示的地址是在004035d1（如下图），也可以选择靠上一点的地址，我这里使用的004035c2，只要能确保符号执行探索到正确提示的分支即可。Ghidra里面给出的地址是16进制值，这里我们需要加上0x。

有超长公式的约束，再加上这是一道CTF的题目，flag应该有且仅有一个正确值，脚本如果找到满足约束条件的密码，索引0的值就是我们需要的密码。如果找到了密码，接下来需要把找到的值投射为字节，因为脚本中的solution变量是一个object对象，使用print打印之前需要使用repr()函数，将对象转化为字符串，代码写完以后，保存代码。