Lambda-revenge CTF逆向题目完整技术解析
💡
原文中文，约16600字，阅读约需40分钟。
📝
内容提要
Lambda-revenge是XCTF 2022的一道高难度逆向题，基于Lambda演算实现复杂的矩阵乘法验证。通过分析源代码和Church编码，提取矩阵及结果，建立线性方程组求解，最终得到flag：XCTF{M4tRI1|i||l|Il|I1X_A5_YC0mb}。
🎯
关键要点
- Lambda-revenge是XCTF 2022的一道高难度逆向题目，基于Lambda演算实现复杂的矩阵乘法验证。
- 题目采用Lambda演算作为核心，通过Church编码和Y组合子实现验证系统。
- 程序需要一个33字节的字符串作为参数，验证失败会输出'Wrong flag!'。
- Flag被分成11组，每组3个字节，每组有独立的验证表达式。
- Church编码是Lambda演算中表示数据的方式，Church数字将自然数编码为函数应用的次数。
- 题目作者提供了完整的编译和反编译工具，帮助理解题目构造。
- 通过反编译器提取矩阵和结果，建立线性方程组求解输入向量。
- 每组数据的验证条件为chall_dot(M[i], X) == R[i]。
- 最终得到的Flag为XCTF{M4tRI1|i||l|Il|I1X_A5_YC0mb}。
- 题目实现了完整的Lambda演算解释器，包含惰性求值和引用计数内存管理。
- Y组合子是Lambda演算中实现递归的技巧，允许定义递归函数。
- 反编译器需要识别Church编码的模式，检查两个lambda表达式是否alpha等价。
- 解题步骤包括源代码分析、Church编码学习、反编译工具使用、数学建模与求解。
- 完整复现方法展示了对compiler.py算法的掌握，能够为任意flag生成有效的(M, R)对。
- Lambda-revenge结合了理论计算机科学和实践逆向工程，考察选手的多方面能力。
➡️
