首页
社区
课程
招聘
问答 CTF 排行榜 知识库 工具下载 看雪峰会 看雪商城 证书查询
  1. 看雪社区
  2. CTF对抗
    3. 发新帖
[原创] KCTF2021 偶遇棋痴出题思路(Android)
2021-11-13 22:50 12216

[原创] KCTF2021 偶遇棋痴出题思路(Android)

无名侠 活跃值
12
2021-11-13 22:50
12216

战队名称: Syclover
参赛题目: KCTF2021 神秘的数学(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 演算结果，判断选手输入是否正确。

 

题目 lambda 编译脚本

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
import string
from 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 s
 
def 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 value
    return "(\\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 random
def 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 + d2
        print((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 表达式按规则进行化简
    a. 模式匹配数值表达式（1,2,...,n）
    b. 模式匹配加法、减法、乘法、比较等运算
    c. 化简比较表达式
    其中，比较运算比较难以理解，因为 lambda 中数值比较需要用两个 sub 实现，而不是一个 sub，即 a - b == 0 && b - a == 0 才能说明 a,b 相等。
  3. 编写解题脚本

题目答案(解题脚本):

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
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}


[培训]二进制漏洞攻防（第3期）；满10人开班；模糊测试与工具使用二次开发；网络协议漏洞挖掘；Linux内核漏洞挖掘与利用；AOSP漏洞挖掘与利用；代码审计。

最后于 2021-11-25 16:09 被无名侠编辑 ，原因：
上传的附件：
收藏
点赞・8
打赏
分享
最新回复 (2)
kanxue
雪    币： 29412
活跃值： (18675)
能力值： (RANK：350 )
在线值：
发帖
回帖
粉丝
私信
kanxue 8 2021-11-14 19:48
2 楼
0
第四题 偶遇棋痴
游客
登录 | 注册 方可回帖
　回帖　 表情 雪币赚取及消费
高级回复
返回