周末闲的无聊打了一下SSTF 2023的比赛，由于自己太菜啦，就做出来了一个题 PulpQuest，中间有很多的时间被Seven’s Game - Metal这个题卡住了，等官方的writeup了，最近有空会把剩下没做的题，做一下丢在这个writeup里

PulpQuest

打开后是pulp的游戏，有点类似于小时候玩的那种小型游戏机，直接开启了模拟器和ce快速过一下

image-20230821234612320

由于快速过一下，我直接搞了一下血量看看这个游戏是怎么玩的

image-20230821234931867

image-20230821235117419

需要reverse给的程序，大概看了一下 就一个data.json是有有用信息的

image-20230821235320047

只看到了这个id : 38是和上面图片中的Scroll是有关系的（其实自己的英语不是很好，我把Magic和Orbs都搜了一下 发现只有这里有相关的id 38）

整理一下相关的check

获取了A - P的后 call foo call bar

image-20230822135720389 

"data": {"abc": ["block",14],
         "bar": ["block",17],
         "baz": ["block",18],
         "boo": ["block",15],
         "foo": ["block",16],
         "ork": ["block",5],
         "qux": ["block",1],
         "fred": ["block",2],
         "thud": ["block",9],
         "corge":["block",13],
         "enter":["block",0],
         "plugh":["block",11]

block有点像数组，执行的函数是"__blocks": [ ] 括号中的哪个

image-20230822140600343

整理一下foo函数

image-20230822141410541 

 foo:
 A,B,C,D,36,23["call","boo"]B,C,D,A 
 E,F,G,H,23,181["call","boo"]F,G,H,E 
 I,J,K,L,181,177["call","boo"]J,K,L,I 
 M,N,O,P,177,36["call","boo"]N,O,P,M 
 A,B,C,D,69,193["call","boo"]B,C,D,A 
 E,F,G,H,193,10["call","boo"]F,G,H,E 
 I,J,K,L,10,99["call","boo"]J,K,L,I 
 M,N,O,P,99,69["call","boo"]N,O,P,M 
 A,B,C,D,246,149["call","boo"]B,C,D,A 
 E,F,G,H,149,183["call","boo"]F,G,H,E 
 I,J,K,L,183,75["call","boo"]J,K,L,I 
 M,N,O,P,75,246["call","boo"]N,O,P,M 
 A,B,C,D,181,94["call","boo"]B,C,D,A 
 E,F,G,H,94,185["call","boo"]F,G,H,E 
 I,J,K,L,185,250["call","boo"]J,K,L,I 
 M,N,O,P,250,181["call","boo"]N,O,P,M 
 A,B,C,D,179,79["call","boo"]B,C,D,A 
 E,F,G,H,79,77["call","boo"]F,G,H,E 
 I,J,K,L,77,56["call","boo"]J,K,L,I 
 M,N,O,P,56,179["call","boo"]N,O,P,M 
 A,B,C,D,107,54["call","boo"]B,C,D,A 
 E,F,G,H,54,201["call","boo"]F,G,H,E 
 I,J,K,L,201,203["call","boo"]J,K,L,I 
 M,N,O,P,203,107["call","boo"]N,O,P,M 
 A,B,C,D,243,64["call","boo"]B,C,D,A 
 E,F,G,H,64,48["call","boo"]F,G,H,E 
 I,J,K,L,48,121["call","boo"]J,K,L,I 
 M,N,O,P,121,243["call","boo"]N,O,P,M 
 A,B,C,D,173,95["call","boo"]B,C,D,A 
 E,F,G,H,95,231["call","boo"]F,G,H,E 
 I,J,K,L,231,47["call","boo"]J,K,L,I 
 M,N,O,P,47,173["call","boo"]N,O,P,M

整理一下boo函数

image-20230822142401951 

fred:

["set", "a2", ["get", "x2"]], ["set", "b2", ["get", "y2"]], ["set", "c2", 0], ["set", "d2", 1]
["set", "i2", 0], ["while", ["lt", "i2", 8], ["block", 3]]
["set", "x2", ["get", "c2"]]


["block", 3]：
["add", "i2", 1]
["set", "x1", ["get", "a2"]], ["set", "y1", 2], 
["call", "qux"], 
["set", "a2", ["get", "x1"]], ["set", "e2", ["get", "y1"]]
["set", "x1", ["get", "b2"]], ["set", "y1", 2], 
["call", "qux"], 
["set", "b2", ["get", "x1"]], ["set", "f2", ["get", "y1"]]
["add", "e2", ["get", "f2"]], 
["if", ["eq", "e2", 1], 
["block", 4]]
["mul", "d2", 2]


["call", "qux"]:
["set", "a1", ["get", "x1"]], ["set", "b1", ["get", "x1"]], ["div", "b1", ["get", "y1"]], ["set", "b1", ["floor", ["get", "b1"]]], ["set", "x1", ["get", "b1"]]
["mul", "b1", ["get", "y1"]], ["sub", "a1", ["get", "b1"]]
["set", "y1", ["get", "a1"]]

["block", 4]:
["add", "c2", ["get", "d2"]]
corge:

["set", "x1", ["get", "y6"]], ["set", "y1", 8], ["call", "qux"]
["set", "x4", ["get", "x6"]], ["set", "y4", ["get", "y1"]], ["call", "thud"]
["set", "d6", 8], ["sub", "d6", ["get", "y1"]]
["set", "x5", ["get", "x6"]], ["set", "y5", ["get", "d6"]], ["call", "plugh"]
["set", "x3", ["get", "x4"]], ["set", "y3", ["get", "x5"]], ["call", "ork"], ["set", "x6", ["get", "x3"]]

["call", "qux"]:
["set", "a1", ["get", "x1"]], ["set", "b1", ["get", "x1"]], ["div", "b1", ["get", "y1"]], ["set", "b1", ["floor", ["get", "b1"]]], ["set", "x1", ["get", "b1"]]
["mul", "b1", ["get", "y1"]], ["sub", "a1", ["get", "b1"]]
["set", "y1", ["get", "a1"]]

["call", "thud"]:
["set", "a4", ["get", "x4"]]
["set", "i4", 0], ["while", ["lt", "i4", ["get", "y4"]], ["block", 10]]
["set", "x4", ["get", "a4"]]

["block", 10]：
["add", "i4", 1], ["add", "a4", ["get", "a4"]]

["call", "plugh"]:
["set", "a5", ["get", "x5"]]
["set", "i5", 0], ["while", ["lt", "i5", ["get", "y5"]], ["block", 12]]
["set", "x5", ["get", "a5"]]

["block", 12]:
["add", "i5", 1], ["div", "a5", 2], ["set", "a5", ["floor", ["get", "a5"]]]

["call", "ork"]：
["set", "a3", ["get", "x3"]], ["set", "b3", ["get", "y3"]], ["set", "c3", 0], ["set", "d3", 1]
["set", "i3", 0], ["while", ["lt", "i3", 8], ["block", 6]]
["set", "x3", ["get", "c3"]]

["block", 6]：
["add", "i3", 1]
["set", "x1", ["get", "a3"]], ["set", "y1", 2], ["call", "qux"], ["set", "a3", ["get", "x1"]], ["set", "e3", ["get", "y1"]]
["set", "x1", ["get", "b3"]], ["set", "y1", 2], ["call", "qux"], ["set", "b3", ["get", "x1"]], ["set", "f3", ["get", "y1"]]
["if", ["neq", "e3", 0], ["block", 7], ["elseif", ["neq", "f3", 0], ["block", 8]]]
["mul", "d3", 2]

["block", 7]:
["add", "c3", ["get", "d3"]]

["block", 8]:
["add", "c3", ["get", "d3"]]
abc:
["set", "a7", ["get", "x7"]], ["add", "a7", ["get", "y7"]]
["set", "x1", ["get", "a7"]], ["set", "y1", 256], ["call", "qux"], ["set", "x7", ["get", "y1"]]

["call", "qux"]:
["set", "a1", ["get", "x1"]], ["set", "b1", ["get", "x1"]], ["div", "b1", ["get", "y1"]], ["set", "b1", ["floor", ["get", "b1"]]], ["set", "x1", ["get", "b1"]]
["mul", "b1", ["get", "y1"]], ["sub", "a1", ["get", "b1"]]
["set", "y1", ["get", "a1"]]

qux：做的是 x1与y1 已经了相余 -> y1 = x1 % 256

abc : y1 = ( x7 + y7 ) % 256

测试了如下的代码根据bar:的问题，推测出fred为xor

#include <iostream>
#include <math.h>
using namespace std;

void qux(double* x1, double* y1)
{
    double a1 = *x1;
    double b1 = *x1;
    b1 /= *y1;
    b1 = floor(b1);
    *x1 = b1;
    b1 *= *y1;
    a1 -= b1;
    *y1 = a1;
}

int main()
{
    double a2 = 9;
    double b2 = 4;
    double c2 = 0;
    double d2 = 1;
    double x1 = 0;
    double e2 = 0;
    double f2 = 0;
    double x2 = 0;
    double y1 = 0;
    for (double i2 = 0; i2 < 8; i2++)
    {
        x1 = a2;
        y1 = 2;
        qux(&x1 , &y1);
        a2 = x1;
        e2 = y1;
        x1 = b2;
        y1 = 2;
        qux(&x1, &y1);
        b2 = x1;
        f2 = y1;

        e2 += f2;
        if (e2 == 1)
        {
            c2 += d2;
        }
        d2 *= 2;
        x2 = c2;
    }
    
    printf("%lf", x2);

    return 0;
}

测试是左移x1 % 8

#include <iostream>
#include <math.h>
using namespace std;

void qux(double* x1, double* y1)
{
    double a1 = *x1;
    double b1 = *x1;
    b1 /= *y1;
    b1 = floor(b1);
    *x1 = b1;
    b1 *= *y1;
    a1 -= b1;
    *y1 = a1;
}

void thud(double* x4, double* y4)
{
    double a4 = *x4;
    for (int i4 = 0; i4 < *y4; i4++)
    {
        a4 += a4;
    }
    *x4 = a4;
}

void plugh(double* x5, double* y5)
{
    double a5 = *x5;
    for (int i5 = 0; i5 < *y5; i5++)
    {
        a5 /= 2;
        a5 = floor(a5);
    }
    *x5 = a5;
}

void ork(double* x3, double* y3)
{
    double a3 = *x3;
    double b3 = *y3;
    double c3 = 0;
    double d3 = 1;
    for (int i3 = 0; i3 < 8; i3++)
    {
        double x1 = a3;
        double y1 = 2;
        qux(&x1, &y1);
        a3 = x1;
        double e3 = y1;
        x1 = b3;
        y1 = 2;
        qux(&x1, &y1);
        b3 = x1;
        float f3 = y1;
        if (e3 != 0)
        {
            c3 += d3;
        }
        else if(f3 != 0)
        {
            c3 += d3;
        }
        d3 *= 2;
    }
    *x3 = c3;
}

int main()
{
    double x1 = 3;
    double y1 = 8;
    qux(&x1, &y1);
    double x4 = 9;
    double y4 = y1;
    thud(&x4, &y4);
    double d6 = 8;
    d6 -= y1;
    double x5 = 9; //保持和x4一样的值
    double y5 = d6;
    plugh(&x5, &d6);
    double x3 = x4;
    double y3 = x5;
    ork(&x3, &y3);
    double x6 = x3;
    printf("%lf", x6);
    return 0;
}
bar:
["set", "x2", ["get", "A"]], ["set", "y2", 36], ["call", "fred"], ["set", "a8", ["get", "x2"]]
["set", "x2", ["get", "B"]], ["set", "y2", 200], ["call", "fred"], ["add", "a8", ["get", "x2"]]
["set", "x2", ["get", "C"]], ["set", "y2", 122], ["call", "fred"], ["add", "a8", ["get", "x2"]]
["set", "x2", ["get", "D"]], ["set", "y2", 255], ["call", "fred"], ["add", "a8", ["get", "x2"]]
["set", "x2", ["get", "E"]], ["set", "y2", 146], ["call", "fred"], ["add", "a8", ["get", "x2"]]
["set", "x2", ["get", "F"]], ["set", "y2", 2], ["call", "fred"], ["add", "a8", ["get", "x2"]]
["set", "x2", ["get", "G"]], ["set", "y2", 160], ["call", "fred"], ["add", "a8", ["get", "x2"]]
["set", "x2", ["get", "H"]], ["set", "y2", 94], ["call", "fred"], ["add", "a8", ["get", "x2"]]
["set", "x2", ["get", "I"]], ["set", "y2", 80], ["call", "fred"], ["add", "a8", ["get", "x2"]]
["set", "x2", ["get", "J"]], ["set", "y2", 115], ["call", "fred"], ["add", "a8", ["get", "x2"]]
["set", "x2", ["get", "K"]], ["set", "y2", 51], ["call", "fred"], ["add", "a8", ["get", "x2"]]
["set", "x2", ["get", "L"]], ["set", "y2", 102], ["call", "fred"], ["add", "a8", ["get", "x2"]]
["set", "x2", ["get", "M"]], ["set", "y2", 105], ["call", "fred"], ["add", "a8", ["get", "x2"]]
["set", "x2", ["get", "N"]], ["set", "y2", 102], ["call", "fred"], ["add", "a8", ["get", "x2"]]
["set", "x2", ["get", "O"]], ["set", "y2", 167], ["call", "fred"], ["add", "a8", ["get", "x2"]]
["set", "x2", ["get", "P"]], ["set", "y2", 137], ["call", "fred"], ["add", "a8", ["get", "x2"]]

判定是不是成功结果的是在当前的模块的block 2和block 3

image-20230822182557864

整理上面的所有

from z3 import *

def boo(a0, b0, c0, d0, e0, f0):
    a8 = a0 ^ b0
    b8 = RotateLeft(a8, b0 % 8)
    a0 = (b8 + e0) % 256
    a8 = a0 ^ b0
    b8 = RotateLeft(a8, a0 % 8)
    b0 = (b8 + f0) % 256
    a8 = c0 ^ d0
    b8 = RotateLeft(a8, d0 % 8)
    c0 = (b8 + e0) % 256
    a8 = c0 ^ d0
    b8 = RotateLeft(a8, c0 % 8)
    d0 = (b8 + f0) % 256
    return a0, b0, c0, d0

def foo(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P):
    B, C, D, A = boo(A, B, C, D, 36, 23)
    F, G, H, E = boo(E, F, G, H, 23, 181)
    J, K, L, I = boo(I, J, K, L, 181, 177)
    N, O, P, M = boo(M, N, O, P, 177, 36)   
    B, C, D, A = boo(A, B, C, D, 69, 193)
    F, G, H, E = boo(E, F, G, H, 193, 10)
    J, K, L, I = boo(I, J, K, L, 10, 99)
    N, O, P, M = boo(M, N, O, P, 99, 69)    
    B, C, D, A = boo(A, B, C, D, 246, 149)
    F, G, H, E = boo(E, F, G, H, 149, 183)
    J, K, L, I = boo(I, J, K, L, 183, 75)
    N, O, P, M = boo(M, N, O, P, 75, 246)    
    B, C, D, A = boo(A, B, C, D, 181, 94)
    F, G, H, E = boo(E, F, G, H, 94, 185)
    J, K, L, I = boo(I, J, K, L, 185, 250)
    N, O, P, M = boo(M, N, O, P, 250, 181)    
    B, C, D, A = boo(A, B, C, D, 179, 79)
    F, G, H, E = boo(E, F, G, H, 79, 77)
    J, K, L, I = boo(I, J, K, L, 77, 56)
    N, O, P, M = boo(M, N, O, P, 56, 179)    
    B, C, D, A = boo(A, B, C, D, 107, 54)
    F, G, H, E = boo(E, F, G, H, 54, 201)
    J, K, L, I = boo(I, J, K, L, 201, 203)
    N, O, P, M = boo(M, N, O, P, 203, 107)    
    B, C, D, A = boo(A, B, C, D, 243, 64)
    F, G, H, E = boo(E, F, G, H, 64, 48)
    J, K, L, I = boo(I, J, K, L, 48, 121)
    N, O, P, M = boo(M, N, O, P, 121, 243)    
    B, C, D, A = boo(A, B, C, D, 173, 95)
    F, G, H, E = boo(E, F, G, H, 95, 231)
    J, K, L, I = boo(I, J, K, L, 231, 47)
    N, O, P, M = boo(M, N, O, P, 47, 173)    
    return A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P

check = [36, 200, 122, 255, 146, 2, 160, 94, 80, 115, 51, 102, 105, 102, 167, 137]

# 创建16个整数变量
A = BitVec('A', 8)
B = BitVec('B', 8)
C = BitVec('C', 8)
D = BitVec('D', 8)
E = BitVec('E', 8)
F = BitVec('F', 8)
G = BitVec('G', 8)
H = BitVec('H', 8)
I = BitVec('I', 8)
J = BitVec('J', 8)
K = BitVec('K', 8)
L = BitVec('L', 8)
M = BitVec('M', 8)
N = BitVec('N', 8)
O = BitVec('O', 8)
P = BitVec('P', 8)

# 创建求解器
solver = Solver()

# 添加函数等式约束
data = foo(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P)

for i in range(16):
    solver.add(data[i] == check[i])

# 求解并输出结果
if solver.check() == sat:
    model = solver.model()
    print(model)

    
#[F = 251, E = 201, L = 47, P = 185, M = 105, N = 79, I = 17, C = 55, D = 105, A = 121, G = 190, B = 81, J = 206, O = 235, H = 60, K = 36]

image-20230822102726340