-
-
2021 KCTF 秋季赛 第四题 偶遇棋痴
-
2021-11-25 11:38 13961
-
初看过程
- jni 直接调用 stringFromJNI 方法判断输入
- 将输入的 14个 字符,按 4bit 拆成 28个 作为
ipt
- 通过
boost::text_oarchive
反序列一个字符串到t
- 执行 方法一(0x39910),方法二(0x39614)
- 将最后得出的结果和一个 固定结果fxx 比较
推测结构
- 刚开始根据 方法一/方法二 能推出大概的结构是12345678910
/
/
名称可从 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
会崩溃所以要做修改
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); } |
华点
- 此时 dump 出的表达式非常巨大 190 KB,找不到下手的地方
- 转变思路,找到作者提供的另外 16个term,都 dump 出来
- 找到两个特点:
- 一个比一个长
- 除 第一个 是 抽象化 之外,其他的都是 应用(app)
- 此时回到那个 lambda 演算库,所谓的演算,是指将 应用 套用并化简(至抽象化或变量)
- 将他们全部演算,发现刚好对应 邱奇数 的 0-15 自然数
- 使用 记事本替换大法,将 原始dump 的自然数全部替换
- 根据 邱奇数 页面,还可以替换,PLUS(ADD),SUCC(INC),MULT
- 最后还剩一个 双目运算 比较长,随便代入几个自然数,得出是 减法(SUB)
- 这个减法有个特点,必须满足,a-b>=0,要不结果是 0,这个后面会考
求解
- 此时应该可以手推出结果了,无奈函数太长,我还是选择求解器求解
- 将替换后的结果弄成 python 的样子,PP 是结合双目运算
- 本想直接去 python + w3 执行,发现会因为函数层级太多无法解析
- 故写了一个求解脚本
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()) |
【看雪培训】《Adroid高级研修班》2022年夏季班招生中!
赞赏
他的文章