专家点评
出题团队简介
战队成员如下：
赛题设计思路
参赛题目：神秘的数学（Android）
计算机科学领域，尤其是编程语言，经常倾向于使用一种特定的演算：Lambda演算（Lambda Calculus）。这种演算也广泛地被逻辑学家用于学习计算和离散数学的结构的本质。现在流行的大部分编程语言中都可以找到 Lambda 的影子，例如 Python、Java，它还是函数式编程的理论基础。Lambda 演算具有图灵完备的性质，因此可以用 Lambda 演算实现任何程序。
本题设计思路是将验证逻辑使用 Lambda 演算实现，选手需要学习 Lambda 演算基础知识，例如 Lambda 演算如何实现数值计算、逻辑计算、currying、α-conversion、Beta Reduction、Church Boolean、Church Numberals等知识才能得心应手的解出本题。
在题目设计过程中，提前对 Lambda 表达式进行预编译，并通过 Boost 的序列化组件对预编译表达式序列化，正式题目对表达式反序列化后得到 Lambda 语法树，选手需要通过各种调试技巧从内存中分离 Lambda 语法树。
选手输入验证码后，程序对选手输入的数据进行编译得到对应的 Lambda 表达式，并插入到预编译的语法树上，以便进行数据演算。
最后，根据 Lambda 演算结果，判断选手输入是否正确。
import stringfrom pwn import *def L_TRUE():return "(\x \y x)"def L_FALSE():return "(\x \y y)"def L_ZERO():return "(\f \x x)"def L_SUCC():return "(\n \f \x n f (f x))"def L_NUM(n):s = L_ZERO()for _ in range(n):s = "("+ L_SUCC() + " " + s + ")"return sdef L_FLAG_NODE(i):return ("(z %d )" % i)def L_SUB():return "(\m\n n " + L_PRE() + " m)"def L_PRE():return "(\n\f\x " + L_CDR() + " (n (" + L_PREFN() + " f) (" + L_CONS() + " x x)))"def L_CDR():return "(\p p " + L_FALSE() + ")"def L_CONS():return "(\x \y \f f x y)"def L_PREFN():return "(\f \p " + L_CONS() +" (f (" + L_CAR() + " p)) (" + L_CAR() + " p))"def L_CAR():return "(\p p " + L_TRUE() + ")"def L_ADD():return "(\m \n \f \x m f (n f x))"def L_IF():return "(\p \x \y p x y)"def L_NOT():return "(\p \a \b p b a)"def L_XOR(): # only works for boolean valuereturn "(\a \b a (" + L_NOT() + " " + "b" + ") b)"def L_MULT():return "(\m \n \f m (n f))"def H_ADD(l, r):return "(" + L_ADD() + " " + l + " " + r + ")"def H_MULT(l, r):return "(" + " ".join([L_MULT(), l , r]) + ")"def H_SUB(l, r):return "(" + " ".join([L_SUB(), l , r]) + ")"def H_XOR(l, r):return "(" + " ".join([L_XOR(), l , r]) + ")"def H_ABSDIFF(l, r):return H_ADD(H_SUB(l, r), H_SUB(r, l))import randomdef challenge(flag, seed):random.seed(seed)sub_eq = []flag_seq = []for c in bytes(flag):flag_seq.append(c & 0xf)flag_seq.append(c >> 0x4)s = L_NUM(0)for i in range(len(flag_seq)):l1 = random.randint(1, 10)d2 = random.randint(1, 10)target = flag_seq[i] * l1 + d2print((l1, d2, target), ",")sub_eq.append(H_ABSDIFF(H_ADD(H_MULT(L_FLAG_NODE(i), L_NUM(l1)), L_NUM(d2)), L_NUM(target)))for exp_i in range(len(sub_eq)):s = H_ADD(s, sub_eq[exp_i])return s#print()def compile_data(text):p = process(["lambda/lambda", 'xxxx'])p.sendline(text)return p.recvall().decode('utf-8')def data2array(name, data):return "char " + name +"[] = {" + ",".join([hex(c) for c in data.encode("ASCII")]) + ", 0x0};"def gen_text_arr(t):return ("char * arr[] = {" + ",".join(['"%s"' % x for x in t]) + "};").replace("\","\\")ts = [L_NUM(i) for i in range(16)]ts.append(challenge(b"pediy{Lambda6}", 2))rr = gen_text_arr(ts)open("lambda/text_chall.h", "w").write(rr)input("step2")l = []for i in range(16):r = open("tests/enc/data_" + str(i) + ".txt", "r").read()l.append(data2array("num_%d" % i, r))open("lambda/nums.h", "w").write("n".join(l))open("lambda/chall.h", "w").write(data2array("chall", open("tests/enc/data_16.txt", "r").read()))
1、从内存提取 Lambda 表达式(反序列化之后)。
2、对 Lambda 表达式按规则进行化简。
b. 模式匹配加法、减法、乘法、比较等运算
c. 化简比较表达式
其中，比较运算比较难以理解，因为 lambda 中数值比较需要用两个 sub 实现，而不是一个 sub，即 a – b == 0 && b – a == 0 才能说明 a,b 相等。
3、编写解题脚本。
题目答案（解题脚本）：
data = [(1, 2, 2) ,(2, 6, 20) ,(3, 5, 20) ,(5, 10, 40) ,(4, 10, 26) ,(1, 10, 16) ,(3, 7, 34) ,(7, 9, 51) ,(6, 9, 63) ,(8, 9, 65) ,(5, 1, 56) ,(1, 6, 13) ,(8, 6, 102) ,(7, 7, 35) ,(9, 3, 12) ,(9, 3, 57) ,(4, 4, 56) ,(1, 3, 9) ,(6, 3, 15) ,(3, 9, 27) ,(9, 6, 42) ,(9, 9, 63) ,(3, 8, 11) ,(7, 9, 51) ,(6, 10, 46) ,(6, 6, 24) ,(8, 3, 107) ,(7, 8, 57) ,]flag_l = []flag = ''for d in data:flag_l.append((d[2] - d[1]) // d[0])for i in range(len(flag_l) // 2):flag += chr((flag_l[i * 2 + 1] << 4 )| flag_l[i * 2])print(flag)
编译版本flag：pediy{Lambda6}
赛题解析（方式1）
本赛题解析由看雪论坛kkHAIKE给出：
初看过程：
1、jni 直接调用 stringFromJNI 方法判断输入
2、将输入的 14个 字符，按 4bit 拆成 28个 作为 ipt
3、通过 boost::text_oarchive 反序列一个字符串到 t
4、执行方法一(0x39910)，方法二(0x39614)
5、将最后得出的结果和一个 固定结果fxx 比较
推测结构：
1、刚开始根据方法一/方法二能推出大概的结构是：
// 名称可从 vptr 的 typeinfo 中看到struct term {int typeunion {char ch;term *other;}term *next;int idx;}
2、后根据 ·0x3B5EA· 处的 puts(“Running out of free variables.”);
3、找到原始项目 https://github.com/mpu/lambda；
4、发现作者在原 term 基础上增加了idx成员；
5、遂根据源码退出方法二为 eval_deep。
序列化分析
1、下载 boost 源码，推出 0x39736 处调用 0x3ADB4 方法，应该像是 ar >> (term*)t；
2、推出该方法应该是 load_pointer_type<term>::invoke；
3、因为该结构是链式结构，所以查看 该方法 的引用 0x3B018，为 serialize 函数；
4、PS：我是通过找vptr找到的，感觉上面这样推简单就这样说了。
lambda 演算
学废这两篇就能做题了：
https://zh.wikipedia.org/wiki/%CE%9B%E6%BC%94%E7%AE%97#lambda%E6%BC%94%E7%AE%97%E8%88%87%E7%B7%A8%E7%A8%8B%E8%AA%9E%E8%A8%80
https://zh.wikipedia.org/wiki/%E9%82%B1%E5%A5%87%E6%95%B0
方法一细节
1、作者引入了一个特殊的 抽象化(绑定z)；
2、他会从输入的 ipt，使用 该抽象化 的 idx（之前新增的成员），选择一个索引；
3、从内置 16个term 选择一个替换掉该抽象化。
打印
1、因为作者增加了一个z抽象化，原来的parse_dump_term会崩溃所以要做修改。
voidparse_dump_term(const struct term * t, FILE * stream){const struct term * pterm = t;int nparen = 0;for (;;)switch (pterm->type) {case Tlam: {// CHANGEif (pterm->data.lam.var == 'z') {fprintf(stream, "[x%d]", pterm->idx);goto Close_paren;}fprintf(stream, "Lam (%c, ", pterm->data.lam.var);pterm = pterm->data.lam.body;nparen++;continue;
序列化源码
template<class Archive>void serialize(Archive& ar, term &t, const unsigned int version) {ar& t.type;switch (t.type) {case Tlam:ar& t.data.lam.var;ar& t.idx;if (t.data.lam.var != 'z') {ar& t.data.lam.body;}break;case Tapp:ar& t.data.app.left;ar& t.data.app.right;break;case Tvar:ar& t.data.var;break;}}term* parse_term_in(std::istream &in) {boost::archive::text_iarchive ar(in);term *ret = nullptr;ar >> ret;return ret;}term* parse_term_s(const char* s) {std::istringstream ss(s);return parse_term_in(ss);}
华点
1、此时 dump 出的表达式非常巨大 190 KB，找不到下手的地方
2、转变思路，找到作者提供的另外 16个term，都 dump 出来
3、找到两个特点：
-
一个比一个长；
-
除第一个是抽象化之外，其他的都是应用(app)
4、此时回到那个 lambda 演算库，所谓的演算，是指将应用套用并化简（至抽象化或变量）
5、将他们全部演算，发现刚好对应 邱奇数0-15自然数
6、使用 记事本替换大法，将原始dump的自然数全部替换
7、根据 邱奇数 页面，还可以替换，PLUS(ADD)，SUCC(INC)，MULT
8、最后还剩一个双目运算比较长，随便代入几个自然数，得出是 减法(SUB)
9、这个减法有个特点，必须满足，a-b>=0，要不结果是 0，这个后面会考。
求解
1、此时应该可以手推出结果了，无奈函数太长，我还是选择求解器求解；
3、本想直接去 python + w3 执行，发现会因为函数层级太多无法解析；
4、故写了一个求解脚本。
def _ADD(a, b):return a + bdef _MULT(a, b):return a * bdef _bind(f, a):return lambda b: f(a,b)def ADD(a):return _bind(_ADD, a)def MULT(a):return _bind(_MULT, a)def INC(a):return a+1from z3 import *x = IntVector('x', 28)s = Solver()def _SUB(a, b):# 一定要加，不加无解s.add(a>=b)return a - bdef SUB(a):return _bind(_SUB, a)with open("ctf4.txt", "rt") as f:data = f.read()def call(p):if p[0] == "P":p = p[3:]a, p = call(p)p = p[2:]b, p = call(p)p = p[1:]return a(b), pelif p[0] == "A":p = p[4:]a, p = call(p)p = p[1:]return ADD(a), pelif p[0] == "S":p = p[4:]a, p = call(p)p = p[1:]return SUB(a), pelif p[0] == "I":p = p[4:]a, p = call(p)p = p[1:]return INC(a), pelif p[0] == "M":p = p[5:]a, p = call(p)p = p[1:]return MULT(a), pelif p[0] == "x":p = p[1:]c = 0while p[c]>='0' and p[c]<='9':c+=1r = int(p[:c])p = p[c:]return x[r], pelse:c = 0while p[c]>='0' and p[c]<='9':c+=1r = int(p[:c])p = p[c:]return r, prr, _ = call(data)s.add(rr==0)s.check()print(s.model())
赛题解析（方式2）
本赛题解析由看雪论坛xym给出：
果然，界面直接导入了kctf2021这个动态库并声明了stringFromJNI这个native函数，并且直接用它对输入进行了判断。
用IDA打开libkctf2021.so，定位到目标函数。
看来关键算法就在sub_39998这个函数里了。在ida里看到这个函数这么清晰明白的显示出来，我的第一感觉是哪里又藏着hook会修改这个函数，于是先简单检查了一下，确定so没有预加载可疑的函数。
关键函数逻辑很清楚，当输入字符串长度为14时，初始化一个表（这个表对我解题并没有用，下面略过不说），然后将输入每4bit转成一个dword，变成一个长为28的数组。
然后调用sub_39658处理一个固定字符串，根据字符串的首行搜索可以得知是这是boost的一个序列化。为了弄清楚反序列化后的对象是什么东西，我这里有两个选择：1是下载boost开发库开发实验一下，2是找个东西模拟运行一下。
因为unidbg比boost更快下载完，因此我最终模拟运行了这个反序列化函数并打印了对象的内存。
序列化后的对象v13继续使用sub_39910进行处理。
首次看这个函数并没有看懂，只能推断他应该是一个很多层的递归处理，并且会根据输入去反序列化其他16个序列化对象中的一个。
结合sub_39614函数可以分析出v13这个对象应该是一个比较大的类似二叉树一样的结构，具有非常多的节点，但是每个节点非常简单，只占16个字节内存。这里发现了一个比较复杂的函数sub_39570（但是这个函数同样对我解题并没有用，下面略过不说……因为我最后都没看懂这个函数）。
最后看一下本题check的逻辑：结尾虽然有一堆的判断跳转，实际归纳起来就是判断最终的v13是不是只有3个特定节点了。
因此梳理一下这道题的思路：作者定制了一棵非常大的二叉树，然后用sub_39910把拆为4bit后的28个输入转为16棵小树中的一颗并插入到二叉树值为122的对应节点中，形成一棵不带122节点的树。然后使用sub_39614对这个树的所有节点进行删减，如果最后只剩3个节点就算成功（3个节点应该是这道题理论上能删减到的最少节点吧）。
那么这道题的破题之处就在于，因为用户输入选择的分支必然是散布到整棵树的不同部位，那对其中某分支能独自占据的最大分支来说，其删减结果其实都与其他输入无关。因此用户的每个输入相对其他输入很可能都是独立的，整个大题可以拆分成为28道相同的小题，而每道小题的解合起来就是整个大题的解。因此我们的目标转换为了在保持27个输入不变时，求剩下那个输入能使最终节点数最少的值。
因为unidbg在运行UXTB16指令时会报错，因此模拟执行的办法在这里就中断了。
幸好整个程序可以转为等效的C代码，通过查询arm汇编指令集，把clz和UXTB16转为相应的函数或代码，实现了每个输入的暴力破解。实际代码中分成两次，第一次是所有的低4bit，第二次是所有的高4bit（因为可见字符最高位为0，所以其实只有3bit），实际使用的指标也不是节点数最少，而是二叉树层数最少（从结果看应该是等效的）。
往期解析
1、看雪·众安 2021 KCTF 秋季赛 | 第二题设计思路及解析
第五题《拔刀相向》正在火热进行中，
球分享
球点赞
球在看
原文始发于微信公众号（看雪学苑）：看雪·众安 2021 KCTF 秋季赛 | 第四题设计思路及解析
