2024-04-30

baby_tree#

Swift底层进阶--001：Swift编译 & SIL分析 - 简书 (jianshu.com)

docker pull swift
docker run -it -v .\swift_docker:/swift_docker swift

swiftc -emit-ir baby_tree.ast -o baby_tree.ll

brace_stmt 表示花括号 {} 中的语句块

pattern_binding_decl 表示模式绑定声明，用于声明变量并将其与特定模式匹配的值绑定在一起。

binary_expr 表示二元表达式

(binary_expr
  (operand)
  (operator_token)
  (operand)
)

dot_syntax_call_expr 表示通过点语法调用的表达式，通常用于访问类型的属性或调用类型的方法。

(dot_syntax_call_expr
  (base_expr)      // 基础表达式，表示调用的对象或类型
  (dot_token)      // 点号（.）标记，用于表示点语法调用
  (name)           // 成员名称，表示被调用的属性或方法名
  (argument_list)  // 参数列表，表示方法调用时的参数
)

有个foreach

分析出来算法了，但是发现无法用z3解出来——这里要用16位，不能用8位，因为8位会有精度损失

data = [88,35,88,225,7,201,57,94,77,56,75,168,72,218,64,91,16,101,32,207,73,130,74,128,76,201,16,248,41,205,103,84,91,99,79,202,22,131,63,255,20,16]

from z3 import *
solver = Solver()

flag = [BitVec(f"bv_{i}", 16) for i in range(len(data))]

save = [f for f in flag]
[solver.add(And(f <= 0x7E, f >= 0x20)) for f in save]

k = b"345y"

for i in range(len(flag) - 3):
    r0 = flag[i]
    r1 = flag[i+1]
    r2 = flag[i+2]
    r3 = flag[i+3]

    flag[i+0] = r2 ^ ((k[0] + (r0 >> 4)) & 0xff)
    flag[i+1] = r3 ^ ((k[1] + (r1 >> 2)) & 0xff)
    flag[i+2] = r0 ^ k[2]
    flag[i+3] = r1 ^ k[3]

    k = bytes([k[1],k[2],k[3],k[0]])

for i in range(len(data)):
    solver.add(flag[i] == data[i])

if solver.check() == sat:
    m = solver.model()
    print(''.join(chr(m[save[i]].as_long()) for i in range(len(data))))
else:
    print("Damn!")