2021 KCTF 秋季赛第四题偶遇棋痴-CTF对抗-看雪论坛-安全社区|安全招聘|bbs.pediy.com

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

2021-11-25 11:38 13961

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

kkHAIKE

2021-11-25 11:38

13961

初看过程

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

推测结构

刚开始根据 方法一/方法二 能推出大概的结构是
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;
}
后根据 ·0x3B5EA· 处的 puts("Running out of free variables.");
找到原始项目 https://github.com/mpu/lambda
发现作者在原 term 基础上增加了 idx 成员
遂根据源码退出 方法二 为 eval_deep

序列化分析

下载 boost 源码，推出 0x39736 处调用 0x3ADB4 方法，应该像是 ar >> (term*)t
推出该方法应该是 load_pointer_type<term>::invoke，
因为该结构是链式结构，所以查看该方法的引用 0x3B018，为 serialize 函数
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

方法一细节

作者引入了一个特殊的 抽象化(绑定z)
他会从输入的 ipt，使用该抽象化的 idx（之前新增的成员），选择一个索引
从内置 16个term 选择一个替换掉该抽象化

打印

因为作者增加了一个 z抽象化，原来的 parse_dump_term 会崩溃所以要做修改

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;

序列化源码

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);
}

华点

此时 dump 出的表达式非常巨大 190 KB，找不到下手的地方
转变思路，找到作者提供的另外 16个term，都 dump 出来
找到两个特点：
1. 一个比一个长
2. 除第一个是抽象化之外，其他的都是 应用(app)
此时回到那个 lambda 演算库，所谓的演算，是指将应用套用并化简（至抽象化或变量）
将他们全部演算，发现刚好对应 邱奇数 的 0-15 自然数
使用记事本替换大法，将原始dump 的自然数全部替换
根据 邱奇数 页面，还可以替换，PLUS(ADD)，SUCC(INC)，MULT
最后还剩一个双目运算比较长，随便代入几个自然数，得出是 减法(SUB)
这个减法有个特点，必须满足，a-b>=0，要不结果是 0，这个后面会考

求解

此时应该可以手推出结果了，无奈函数太长，我还是选择求解器求解
将替换后的结果弄成 python 的样子，PP 是结合双目运算
本想直接去 python + w3 执行，发现会因为函数层级太多无法解析
故写了一个求解脚本

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())