TPCTF 2023 matrix wp (done after contest)

sol_and_wp.py

#from sage.all import *
import numpy as np
import sympy as sp
from sympy.abc import x

matrices=[[[16, 55, 40], [0, -39, -40], [0, 55, 56]], [[13, 41, 29], [3, -25, -29], [-3, 41, 45]], [[7, 13, 7], [9, 3, -7], [-9, 13, 23]], [[1, -15, -15], [15, 31, 15], [-15, -15, 1]], [[217, 728, 512], [39, -472, -512], [-39, 728, 768]], [[9341, 41833, 32493], [21635, 96663, 75027], [-29315, -130967, -101651]], [[10, 27, 18], [6, -11, -18], [-6, 27, 34]], [[28, 111, 84], [-12, -95, -84], [12, 111, 100]], [[266, 970, 705], [-10, -714, -705], [10, 970, 961]], [[1878, 4506, 2629], [2218, -410, -2629], [-2218, 4506, 6725]], [[253, 953, 701], [3, -697, -701], [-3, 953, 957]], [[1881, 4520, 2640], [2215, -424, -2640], [-2215, 4520, 6736]], [[233, 821, 589], [23, -565, -589], [-23, 821, 845]], [[1593, 3096, 1504], [2503, 1000, -1504], [-2503, 3096, 5600]], [[-7038, -35490, -28451], [-19586, -98654, -79069], [27266, 137310, 110045]], [[196, 695, 500], [60, -439, -500], [-60, 695, 756]], [[1590, 3082, 1493], [2506, 1014, -1493], [-2506, 3082, 5589]], [[166, 490, 325], [90, -234, -325], [-90, 490, 581]], [[149002, 670490, 521489], [375174, 1688246, 1313071], [-506214, -2277910, -1771695]], [[163, 546, 384], [93, -290, -384], [-93, 546, 640]], [[145, 457, 313], [111, -201, -313], [-111, 457, 569]], [[148969, 670341, 521373], [375207, 1688395, 1313187], [-506247, -2278059, -1771811]], [[178, 606, 429], [78, -350, -429], [-78, 606, 685]], [[9389, 42057, 32669], [21587, 96439, 74851], [-29267, -130743, -101475]], [[46, 195, 150], [-30, -179, -150], [30, 195, 166]], [[4, -1, -4], [12, 17, 4], [-12, -1, 12]], [[-7041, -35504, -28462], [-19583, -98640, -79058], [27263, 137296, 110034]], [[184, 579, 396], [72, -323, -396], [-72, 579, 652]], [[22, 83, 62], [-6, -67, -62], [6, 83, 78]], [[127, 368, 242], [129, -112, -242], [-129, 368, 498]], [[25, 97, 73], [-9, -81, -73], [9, 97, 89]], [[118, 289, 172], [138, -33, -172], [-138, 289, 428]], [[19, 69, 51], [-3, -53, -51], [3, 69, 67]], [[199, 639, 441], [57, -383, -441], [-57, 639, 697]], [[160, 517, 358], [96, -261, -358], [-96, 517, 614]]]
# 不知道怎么注意到这两矩阵，只能赛后看到提示
A = np.matrix([[2, 9, 7], [1, 5, 4], [1, 1, 1]])
B = np.matrix([[1, -2, 1], [3, -5, -1], [-4, 7, 1]])
m = [np.matrix(v) for v in matrices]
target = [84118752460105480846935836819753079271600697690686619664255230678276718877418958891792249030775786942317984652111184426018279427, 89173103422445447876715049689189652193176619520301916283899743110137112860432642548206151350732936688768966032976538813292605444, -132496067393083180057627771316425335059370948823049050270938486557240570794895542908205751446110117596540703704248469623120326662]
# 注意到 B*A=1
assert (B@A == np.matrix(np.identity(3, dtype=int))).all()
L = [A@v@B for v in m]
"""
可以看到L都形如
[16**x, 0, 0]
[0, 16**y, 0]
[a, b, 1]
如果vec的第三维为1；
vec * such matrix 意味着向量开头一个数字(看作16进制串)拼接上a，第二个拼接上b
"""
print(L)
vec = np.array([80+256*x,396+1280*x, 317+1024*x])
AI = np.round(A.I).astype(int)
BI = np.round(B.I).astype(int)
# 由于 B*A=1, 下面的内容等价
print(vec @ m[0] @ m[5] @ m[10] @ B)
print(vec @ AI @ L[0] @ L[5] @ L[10])
# 注意到初始向量 vec @ AI = [0 256*x + 79 1]
print(vec @ AI)
# 在所有 *L[x] 操作后, 结果等于乘如下列向量
# [c1=0x10**106, -1, c2=0xf1...1(length==106)]^T
BIt = (BI @ np.matrix(np.diag(target)))
BIts = np.sum(BIt, axis=1)
print(BIts)
# 拿到所有用来拼接的pads
pads = []
for i, v in enumerate(L):
    len1 = len(hex(v[0,0])) - 3
    len2 = len(hex(v[1,1])) - 3
    v1 = hex(v[2,0])[2:].zfill(len1)
    v2 = hex(v[2,1])[2:].zfill(len2)
    pads.append((v1, v2))
    print(chr(i + 65), v1.rjust(5), v2.rjust(5))

# 拿到c1 c2
c1 = BIts[0,0]
c2 = BIts[2,0]
sc2 = hex(c2)[2:]
print(hex(c1))
print(hex(c2))

"""
把前两个向量分量所有拼接的内容分别记作A和B
那么原本的判断条件等价于
int_concat(A, sc2) == int_cancat('23', FLAG, '4f', B)
下面是程序验证
"""
import random
selected = [random.randrange(0, len(m)) for _ in range(100)]

# 新条件
A = ''
B = ''
for idx in selected:
    A += pads[idx][0]
    B += pads[idx][1]

lenB = len(B)
A = int(A, 16)
B = int(B, 16)
way1 = A * c1 + c2 - ((x * 0x100 + 0x4f) * 0x10**lenB + B)

# 旧条件
v = vec
for idx in selected:
    v = v @ m[idx]

way2 = np.dot(np.array(v), target)[0]
print(way1 - way2)
"""
注意到对pads做以下替换后
5 B0
6 B1
7 A0
8 A1

0 and 1 可以来就像符号一个可以传递了 0->0 01->01 01->10 as X, Y
invariant
    X     X
    2     2
    3     3
    4     4
   AX    AX
   BX    BX
    9     9
    f     f
transfer constants
   34    94
   29    23
transfer one var
  3X4   AX4
  BX4    4X
  2AX   23X
 23X4     X
   X9    9X
transfer double var
  BXY   YBX
  XAY   AYX
  3XY  X3BY
xy counts == 105, flag length=15
"""

## int_concat(A, sc2) == int_cancat('23', FLAG, '4f', B)

"""
注意到f只能变成f
那么把a和b用f分隔(两边数量一定相同)，可以得到
A1       f A2 f A3 ... sc2
23 flag 4f B1 f B2 ...
也就是A1与 23 flag 4 对应
然后由于A1 B1是同时pad的，所以是按上面规则对应的
注意这个串可以无限长，因为总是可以一直跑
但目标是把 234 全去掉，这样就可以和01串sc2对应了
"""
end = [(1, i) for i in range(105)]
start = [(0, 2), (0, 3), *end, (0, 4)]

def expr_to_list(expr):
    l = []
    la, lb = -1, -1
    for i, v in enumerate(expr):
        if v == 'X':
            l.append((1, 0))
            la = i
        elif v == 'Y':
            l.append((1, 1))
            lb = i
        else:
            l.append((0, int(v, 16)))
    return l, la, lb

def printv(v):
    return ''.join(hex(x[1])[2:] if x[0]==0 else '?' for x in v)


class Rule:
    def __init__(self, v):
        a, b = v
        self.left, self.posLA, self.posLB = expr_to_list(a)
        if self.posLA < 0:
            self.posLA = 0
        if self.posLB < 0:
            self.posLB = 0
        self.right, self.posRA, self.posRB = expr_to_list(b)

    def prefix(self):
        return self.left[0]

    def ok(self, x, pos):
        if len(x) - pos < len(self.left):
            return False
        for i, v in enumerate(self.left):
            if v[0] == 1 and x[i+pos][0] == 1:
                continue
            if v[0] == 1 or x[i+pos][0] == 1:
                return False
            if v[1] != x[i+pos][1]:
                return False
        return True

    def apply(self, x, pos, y):
        ly = len(y)
        y.extend(self.right)
        if self.posRA > -1:
            y[ly + self.posRA] = x[pos + self.posLA]
            if self.posRB > -1:
                y[ly + self.posRB] = x[pos + self.posLB]
        return pos + len(self.left)

    def change(self, x, pos):
        ta = x[pos + self.posLA]
        tb = x[pos + self.posLB]
        x = x[:pos] + self.right + x[pos+len(self.left):]
        #print(printv(x[:pos]), printv(self.right), printv(x[pos+len(self.left):]))
        if self.posRA > -1:
            x[pos + self.posRA] = ta
            if self.posRB > -1:
                x[pos + self.posRB] = tb
        return x

"""
我们把规则分组，理解清楚每个替换能干啥
for 9 把3弄到底可以变出个9来回传给开头的2，变回3
    (   '34',    '94'),
    (   'X9',    '9X'),
    (   '29',    '23'),
把3变到只剩一格的时候可以化作A，然后反序回传给2，再变回3
    (  '3X4',   'AX4'),
    (  'XAY',   'AYX'),
    (  '2AX',   '23X'),
3可以以前进一格为代价弄出B，B可以反序前进，B接近底部会使得4向前收紧
    (  '3XY',  'X3BY'),
    (  'BXY',   'YBX'),
    (  'BX4',    '4X'),
最终状态，4走到了开头
    ( '23X4',     'X'),
我们可以想到一个3走一次就把B发射完，直到和4碰上后3变成A或者9回到开头再前进，直到最终状态
为规则设置个优先级就能正常跑了
"""

readable_rules = [
# 碰到就结束了
    ( '23X4',     'X'),
# 优先前进B，其次3
    (  'BX4',    '4X'),
    (  'BXY',   'YBX'),
    (  '3XY',  'X3BY'),
# 回传版本1
    (  '2AX',   '23X'),
    (  'XAY',   'AYX'),
    (  '3X4',   'AX4'),
# 回传版本2
    (   '29',    '23'),
    (   'X9',    '9X'),
    (   '34',    '94'),
]
cnt = 0
rules = [Rule(v) for v in readable_rules]
while not all(v[0] == 1 for v in start):
    ok = False
    for idx, rule in enumerate(rules):
        for i in range(len(start)):
            if rule.ok(start, i):
                print('applied', readable_rules[idx])
                start = rule.change(start, i)
                ok = True
                break
        if ok:
            break
    if not ok:
        print('sad')
        exit()
    cnt += 1
    print(cnt, printv(start))
print('bingo', start)
# 还原flag
c = '111101101010100101001001110111011100101000010100011110001001000111100110101011001001101010111010010101001'
co = [0]*len(c)
for i, v in enumerate(start):
    co[v[1]] = c[i]
c = ''.join(co)
flag = 'flag{%s}' % bytes([int(c[x:x+7], 2) for x in range(0, len(c), 7)]).decode()
print(flag)
# flag{undec1dab1e_PcP}