首页
社区
课程
招聘
问答 CTF 排行榜 知识库 工具下载 看雪峰会 看雪商城 证书查询
  1. 看雪社区
  2. CTF对抗
    3. 发新帖
2021 KCTF 秋季赛 第四题 偶遇棋痴
2021-11-25 11:38 20752

2021 KCTF 秋季赛 第四题 偶遇棋痴

kkHAIKE 活跃值
10
2021-11-25 11:38
20752

初看过程

  1. jni 直接调用 stringFromJNI 方法判断输入
  2. 将输入的 14个 字符，按 4bit 拆成 28个 作为 ipt
  3. 通过 boost::text_oarchive 反序列一个字符串到 t
  4. 执行 方法一(0x39910)，方法二(0x39614)
  5. 将最后得出的结果和一个 固定结果fxx 比较

推测结构

  1. 刚开始根据 方法一/方法二 能推出大概的结构是
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    // 名称可从 vptr 的 typeinfo 中看到
    struct term {
        int type
        union {
            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 演算

学废这两篇就能做题了

  1. 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
  2. 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 会崩溃所以要做修改
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
void
parse_dump_term(const struct term * t, FILE * stream)
{
    const struct term * pterm = t;
    int nparen = 0;
 
    for (;;)
        switch (pterm->type) {
        case Tlam: {
            // CHANGE
            if (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;

序列化源码

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
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. 找到两个特点：
    1. 一个比一个长
    2. 除 第一个 是 抽象化 之外，其他的都是 应用(app)
  4. 此时回到那个 lambda 演算库，所谓的演算，是指将 应用 套用并化简（至抽象化或变量）
  5. 将他们全部演算，发现刚好对应 邱奇数 的 0-15 自然数
  6. 使用 记事本替换大法，将 原始dump 的自然数全部替换
  7. 根据 邱奇数 页面，还可以替换，PLUS(ADD)，SUCC(INC)，MULT
  8. 最后还剩一个 双目运算 比较长，随便代入几个自然数，得出是 减法(SUB)
  9. 这个减法有个特点，必须满足，a-b>=0，要不结果是 0，这个后面会考

求解

  1. 此时应该可以手推出结果了，无奈函数太长，我还是选择求解器求解
  2. 将替换后的结果弄成 python 的样子，PP 是结合双目运算
    文本替换结果
  3. 本想直接去 python + w3 执行，发现会因为函数层级太多无法解析
  4. 故写了一个求解脚本
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
def _ADD(a, b):
    return a + b
def _MULT(a, b):
    return a * b
def _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+1
 
from z3 import *
x = IntVector('x', 28)
s = Solver()
 
def _SUB(a, b):
    # 一定要加，不加无解
    s.add(a>=b)
    return a - b
def 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), p
    elif p[0] == "A":
        p = p[4:]
        a, p = call(p)
        p = p[1:]
        return ADD(a), p
    elif p[0] == "S":
        p = p[4:]
        a, p = call(p)
        p = p[1:]
        return SUB(a), p
    elif p[0] == "I":
        p = p[4:]
        a, p = call(p)
        p = p[1:]
        return INC(a), p
    elif p[0] == "M":
        p = p[5:]
        a, p = call(p)
        p = p[1:]
        return MULT(a), p
    elif p[0] == "x":
        p = p[1:]
        c = 0
        while p[c]>='0' and p[c]<='9':
            c+=1
        r = int(p[:c])
        p = p[c:]
        return x[r], p
    else:
        c = 0
        while p[c]>='0' and p[c]<='9':
            c+=1
        r = int(p[:c])
        p = p[c:]
        return r, p
 
rr, _ = call(data)
s.add(rr==0)
s.check()
print(s.model())

阿里云助力开发者！2核2G 3M带宽不限流量！6.18限时价，开 发者可享99元/年，续费同价！

收藏
点赞・5
打赏
分享
最新回复 (1)
n00bzx
雪    币： 159
活跃值： (720)
能力值： ( LV3，RANK：29 )
在线值：
发帖
回帖
粉丝
私信
n00bzx 2023-4-9 15:24
2 楼
0
学到了
游客
登录 | 注册 方可回帖
　回帖　 表情 雪币赚取及消费
高级回复
返回