SycLang 出题思路
本题目提供了中间代码和编译器前端，要求将中间代码逆向回C，自行编译后解出 flag（当然也可以直接通过中间代码分析 flag）
首先，本程序有3个陷阱：
1 2 3 4 5 6 7 8 9 10 11 12 13 #!tempa := {#8}*{var16<+64>} var12<+32> := var22(@exp.key[0])<+8><+488><+tempa> temp84 := #1 temp85 := var15<+56> + temp84 var18<+80> := temp85 #!tempa := {#8}*{var18<+80>} var13<+40> := var22(@exp.key[0])<+8><+488><+tempa> temp86 := #0 var13<+40> := temp86 temp87 := var12<+32> ^ var13<+40> var14<+48> := temp87 #!tempa := {#8}*{var16<+64>} var22(@exp.key[0])<+8><+488><+tempa> := var14<+48>
var13<+40> 在异或前会赋值“0”，因此对 e1.key(var22(@exp.key[0])<+8><+488><+tempa>) 的异或加密失效
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 77 78 79 80 LABEL label59 : temp89 := #0 var24(@exp.L[0])<+200><+1256> := temp89 temp91 := #12 var24(@exp.R[0])<+264><+1256> := temp91 temp93 := #0 ...... var24(@exp.key[23])<+192><+1256> := temp195 temp196 := #23 var15<+56> := temp196 LABEL label118 : temp198 := #0 IF var15<+56> > temp198 GOTO label117 GOTO label116 LABEL label117 : var18<+80> := var15<+56> #!tempa := {#8}*{var18<+80>} var19<+88> := var24(@exp.key[0])<+8><+1256><+tempa> temp199 := #1 temp200 := var15<+56> - temp199 var16<+64> := temp200 #!tempa := {#8}*{var16<+64>} var17<+72> := var24(@exp.key[0])<+8><+1256><+tempa> temp201 := var19<+88> - var17<+72> var21<+104> := temp201 #!tempa := {#8}*{var15<+56>} var24(@exp.key[0])<+8><+1256><+tempa> := var21<+104> temp197 := #1 var15<+56> := var15<+56> - temp197 GOTO label118 LABEL label116 : temp202 := #0 var15<+56> := temp202 LABEL label126 : temp204 := #8 IF var15<+56> < temp204 GOTO label125 GOTO label124 LABEL label125 : #!tempa := {#8}*{var15<+56>} var16<+64> := var24(@exp.L[0])<+200><+1256><+tempa> #!tempa := {#8}*{var15<+56>} var18<+80> := var24(@exp.R[0])<+264><+1256><+tempa> #!tempa := {#8}*{var15<+56>} var20<+96> := var24(@exp.X[0])<+328><+1256><+tempa> #!tempa := {#8}*{var16<+64>} var17<+72> := var24(@exp.key[0])<+8><+1256><+tempa> #!tempa := {#8}*{var18<+80>} var19<+88> := var24(@exp.key[0])<+8><+1256><+tempa> var17<+72> := var17<+72> + var20<+96> var19<+88> := var19<+88> - var20<+96> #!tempa := {#8}*{var16<+64>} var24(@exp.key[0])<+8><+1256><+tempa> := var17<+72> #!tempa := {#8}*{var18<+80>} var24(@exp.key[0])<+8><+1256><+tempa> := var19<+88> temp203 := #1 var15<+56> := var15<+56> + temp203 GOTO label126 LABEL label124 : temp207 := #1 var15<+56> := temp207 LABEL label137 : temp209 := #24 IF var15<+56> < temp209 GOTO label136 GOTO label135 LABEL label136 : #!tempa := {#8}*{var15<+56>} var17<+72> := var24(@exp.key[0])<+8><+1256><+tempa> temp210 := #1 temp211 := var15<+56> - temp210 var16<+64> := temp211 #!tempa := {#8}*{var16<+64>} var20<+96> := var24(@exp.key[0])<+8><+1256><+tempa> var17<+72> := var17<+72> + var20<+96> #!tempa := {#8}*{var15<+56>} var24(@exp.key[0])<+8><+1256><+tempa> := var17<+72> temp208 := #1 var15<+56> := var15<+56> + temp208 GOTO label137
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 LABEL label168 : temp263 := #24 IF var15<+56> < temp263 GOTO label167 GOTO label166 LABEL label167 : var16<+64> := var15<+56> #!tempa := {#8}*{var16<+64>} var17<+72> := var23(@exp.key[0])<+8><+872><+tempa> var18<+80> := var15<+56> #!tempa := {#8}*{var18<+80>} var19<+88> := var24(@exp.key[0])<+8><+1256><+tempa> temp264 := var17<+72> ^ var19<+88> var21<+104> := temp264 #!tempa := {#8}*{var15<+56>} var23(@exp.key[0])<+8><+872><+tempa> := var21<+104> temp262 := #1 var15<+56> := var15<+56> + temp262 GOTO label168
对 e3.key(var24(@exp.key[0])<+8><+1256><+tempa>) 的前缀和差分加密会导致 e3.key 全为 “0”，进而对 e2.key(var23(@exp.key[0])<+8><+872><+tempa>) 的异或加密失效
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 LABEL label271 : #!tempa := {#8}*{var15<+56>} var16<+64> := var25(@exp.L[0])<+200><+1640><+tempa> #!tempa := {#8}*{var15<+56>} var18<+80> := var25(@exp.R[0])<+264><+1640><+tempa> #!tempa := {#8}*{var15<+56>} var20<+96> := var25(@exp.X[0])<+328><+1640><+tempa> #!tempa := {#8}*{var16<+64>} var17<+72> := var25(@exp.key[0])<+8><+1640><+tempa> #!tempa := {#8}*{var18<+80>} var19<+88> := var25(@exp.key[0])<+8><+1640><+tempa> var17<+72> := var17<+72> - var20<+96> var19<+88> := var19<+88> + var20<+96> #!tempa := {#8}*{var16<+64>} var25(@exp.key[0])<+8><+1640><+tempa> := var17<+72> #!tempa := {#8}*{var18<+80>} var25(@exp.key[0])<+8><+1640><+tempa> := var19<+88> temp369 := #1 var15<+56> := var15<+56> + temp369 GOTO label272 LABEL label270 : temp373 := #1 var15<+56> := temp373 LABEL label283 : temp375 := #24 IF var15<+56> < temp375 GOTO label282 GOTO label281 LABEL label282 : #!tempa := {#8}*{var15<+56>} var17<+72> := var25(@exp.key[0])<+8><+1640><+tempa> temp376 := #1 temp377 := var15<+56> - temp376 var16<+64> := temp377 #!tempa := {#8}*{var16<+64>} var20<+96> := var25(@exp.key[0])<+8><+1640><+tempa> var17<+72> := var17<+72> + var20<+96> #!tempa := {#8}*{var15<+56>} var25(@exp.key[0])<+8><+1640><+tempa> := var17<+72> temp374 := #1 var15<+56> := var15<+56> + temp374 GOTO label283
对 e4.key(var25(@exp.key[0])<+8><+1640><+tempa>) 的前缀和差分加密最后会得到一个 fake flag
程序有效部分的核心逻辑如下：
程序读取 flag 存入 e1.key 进行第一次前缀和差分，区间修改的操作数在 e1.L，e1.R，e1.X 中（已知）
将第一轮计算的结果间隔取8个存入 e2.X，当做第二次前缀和差分的操作数
第二次使用 e1.L，e1.R，e2.X 对 e2.key（已知）进行前缀和差分
最后对比 e1.key 和 e2.key 完全相同则 success
前缀和差分相当于对 [L，R) 的所有数字 +X：
由于第一次前缀和的操作数已知，得到结果 e1.key[i] 为 INPUT[i] + C[i]
由于第二次前缀和差分需要用到第一次前缀和差分的结果，此时的 X[i] 已经变成 INPUT[i*3] + C[i*3]，结果 e2.key[i] 表达为 INPUT[j1] + INPUT[j2] ...... INPUT[jn] + C[j]
由于 e2.key 的初始值已知，常数 C[j] 可通过 e1.L，e1.R，e1.X 算出，加密后的 e1.key[i] 可以由含有 INPUT[j] 的式子来表示，加密后的 e2.key[i] 也可以用含有 INPUT[j] 的式子来表示，两者结合可以得到 24 组一次方程
通过中间代码提取出来的C代码样例如下：
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 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 for (i=0 ;i<24 ;i++){ key1 = 0 ; x = i; key1 = flag[x]; y = 23 - i; e1.key[y] = key1; } for (i=23 ;i>0 ;i--){ y = i; ky = e1.key[y]; x = i - 1 ; kx = e1.key[x]; kz = ky - kx; e1.key[i] = kz; } e1.L[0 ] = 0 ; e1.R[0 ] = 8 ; e1.X[0 ] = 11 ; e1.L[1 ] = 15 ; e1.R[1 ] = 23 ; e1.X[1 ] = 0 -13 ; e1.L[2 ] = 2 ; e1.R[2 ] = 11 ; e1.X[2 ] = 17 ; e1.L[3 ] = 10 ; e1.R[3 ] = 20 ; e1.X[3 ] = 0 -19 ; e1.L[4 ] = 6 ; e1.R[4 ] = 13 ; e1.X[4 ] = 23 ; e1.L[5 ] = 9 ; e1.R[5 ] = 21 ; e1.X[5 ] = 0 -29 ; e1.L[6 ] = 1 ; e1.R[6 ] = 19 ; e1.X[6 ] = 31 ; e1.L[7 ] = 4 ; e1.R[7 ] = 17 ; e1.X[7 ] = 0 -37 ; for (i=0 ;i<8 ;i++){ x = e1.L[i]; y = e1.R[i]; z = e1.X[i]; kx = e1.key[x]; ky = e1.key[y]; kx += z; ky -= z; e1.key[x] = kx; e1.key[y] = ky; } for (i=1 ;i<24 ;i++){ kx = e1.key[i]; x = i-1 ; z = e1.key[x]; kx += z; e1.key[i] = kx; } e2.key[0 ]=252 ; e2.key[1 ]=352 ; e2.key[2 ]=484 ; e2.key[3 ]=470 ; e2.key[4 ]=496 ; e2.key[5 ]=487 ; e2.key[6 ]=539 ; e2.key[7 ]=585 ; e2.key[8 ]=447 ; e2.key[9 ]=474 ; e2.key[10 ]=577 ; e2.key[11 ]=454 ; e2.key[12 ]=466 ; e2.key[13 ]=345 ; e2.key[14 ]=344 ; e2.key[15 ]=486 ; e2.key[16 ]=501 ; e2.key[17 ]=423 ; e2.key[18 ]=490 ; e2.key[19 ]=375 ; e2.key[20 ]=257 ; e2.key[21 ]=203 ; e2.key[22 ]=265 ; e2.key[23 ]=125 ; for (i=0 ;i<8 ;i++){ x = i + i + i; kx = e1.key[x]; e2.X[i] = kx; } for (i=23 ;i>0 ;i--){ y = i; ky = e2.key[y]; x = i; x -= 1 ; kx = e2.key[x]; kz = ky - kx; e2.key[i] = kz; } for (i=0 ;i<8 ;i++){ x = e1.L[i]; y = e1.R[i]; z = e2.X[i]; kx = e2.key[x]; ky = e2.key[y]; kx -= z; ky += z; e2.key[x] = kx; e2.key[y] = ky; } for (i=1 ;i<24 ;i++){ kx = e2.key[i]; x = i-1 ; z = e2.key[x]; kx += z; e2.key[i] = kx; }
下面是公式推导的过程：
通过 z3 即可求解 flag：
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 from z3 import *s = [] for i in range (24 ): s.append(Int('S' +str (i))) x = Solver() x.add(s[0 ]+s[0 ]+22 == 252 ) x.add(s[0 ]+s[18 ]+s[1 ]+23 == 352 ) x.add(s[0 ]+s[18 ]+s[6 ]+s[2 ]+85 == 484 ) x.add(s[0 ]+s[18 ]+s[6 ]+s[3 ]+85 == 470 ) x.add(s[0 ]+s[18 ]+s[6 ]+s[21 ]+s[4 ]+35 == 496 ) x.add(s[0 ]+s[18 ]+s[6 ]+s[21 ]+s[5 ]+35 == 487 ) x.add(s[0 ]+s[18 ]+s[6 ]+s[21 ]+s[12 ]+s[6 ]+27 == 539 ) x.add(s[0 ]+s[18 ]+s[6 ]+s[21 ]+s[12 ]+s[7 ]+27 == 585 ) x.add(s[18 ]+s[6 ]+s[21 ]+s[12 ]+s[8 ]+5 == 447 ) x.add(s[18 ]+s[6 ]+s[21 ]+s[12 ]+s[15 ]+s[9 ]-91 == 474 ) x.add(s[18 ]+s[6 ]+s[21 ]+s[12 ]+s[15 ]+s[9 ]+s[10 ]-105 == 577 ) x.add(s[18 ]+s[21 ]+s[12 ]+s[15 ]+s[9 ]+s[11 ]-167 == 454 ) x.add(s[18 ]+s[21 ]+s[12 ]+s[15 ]+s[9 ]+s[12 ]-167 == 466 ) x.add(s[18 ]+s[21 ]+s[15 ]+s[9 ]+s[13 ]-159 == 345 ) x.add(s[18 ]+s[21 ]+s[15 ]+s[9 ]+s[14 ]-159 == 344 ) x.add(s[18 ]+s[21 ]+s[15 ]+s[9 ]+s[3 ]+s[15 ]-113 == 486 ) x.add(s[18 ]+s[21 ]+s[15 ]+s[9 ]+s[3 ]+s[16 ]-113 == 501 ) x.add(s[18 ]+s[15 ]+s[9 ]+s[3 ]+s[17 ]-63 == 423 ) x.add(s[18 ]+s[15 ]+s[9 ]+s[3 ]+s[18 ]-63 == 490 ) x.add(s[15 ]+s[9 ]+s[3 ]+s[19 ]-64 == 375 ) x.add(s[15 ]+s[3 ]+s[20 ]-50 == 257 ) x.add(s[3 ]+s[21 ]+46 == 203 ) x.add(s[3 ]+s[22 ]+46 == 265 ) x.add(s[23 ] == 125 ) if (x.check()==sat): model = x.model() print (model) model = x.model() flag = [0 ]*24 for i in str (model).split(',' ): pos, val = i.split('=' )[:2 ] pos = int ('' .join([i for i in pos if i.isdigit()])) val = int ('' .join([i for i in val if i.isdigit()])) flag[pos] = chr (val) flag = '' .join(flag) print (flag)
