汽车安全 | 33分钟
Automotive CTF 2024 Writeup
八月 18, 2025
CAN RSA签名 UDS JWT ICSim 伪随机数 安全访问 Reverse

之前了解到了2024的汽车安全CTF，去搜了一下，发现官方提供了汽车安全的学习课程、还有靶场，这里记录靶场题解，还有学习过程中的内容，目前课程前面不少法律法规，很无聊

这个比赛的词条很多：VSEC 2024和

VicOne and Block Harbor’s Automotive CTF

2025年的汽车安全CTF在8 月 22 日至 25 日和 8 月 29 日至 9 月 1 日开启，希望在这之前能刷完这些题目，去今年的比赛上做出一两道

注意，由于2024的靶场已关闭，并且许多题目尚未迁移到BlockHarbor靶场（比如OSINT），所以我也做不了24年的题目，我是根据 Proving Grounds Walkthrough 的课程做的，目前课程里的题目全部做完，但是靶场里VSEC 的题目还差一些，后续会补充

Getting Started

Can you find the interface?

打开UDS的模拟器，输入ifconfig 或者ip link都能找到vcan0的网卡名称

实际操作中应该是can0之类，v一般代表虚拟设备，用来调试、仿真

Arbitration

candump vcan0

输出：vcan0 59E [2] 9E 10

vcan0是接口名称，表示 CAN 帧的来源接口

59E就是标识符（仲裁ID），CAN ID 可以是 11 位（标准帧）或 29 位（扩展帧）。这里 59E 是 11 位标准帧（因为值在 0x000 到 0x7FF 范围内）。ID 决定了消息的优先级（数值越低，优先级越高）。具体含义取决于应用程序协议（如汽车中的 ECU 通信）

[2]: 数据长度代码（DLC），表示 CAN 帧中 数据字段的字节数，范围是 0 到 8。

9E 10: 数据字段， 这是 CAN 帧的 实际传输数据，以十六进制字节序列表示。

Data Field 1

2

Data Field 2

9E10

Message Frequency

赫兹是每秒发送的次数

candump -t a vcan0，-t a的意思是显示精确时间戳

可以看到每次都隔了一秒左右，计算下来大约是1赫兹

Crypto

pow pow!

给了

txt
1I signed my flag, thats pretty much the same as encryption, right?
2
3pub_e: 65537
4pub_n: 27130058966678375728118690628915085193505679921867847648180394177280300520851322209827953313677610995977175396855400115719997248093217978788791475794191309606741245965521564249520758557425707716276357612383008262150259072257782913410617175802499340022388447047629022386881255413171331856263374853843961598744215379945538726953506454859112787839466674350352298690863753069032704210896554984332177790093120515590458961735089368466550753534317073220559703261053361251093853868715391272704827131460657841223647599202717920842362378900859386228898179814271143542598798022604629591665790726585192070387959726079579927264339
5flag: 4172204809297405811985500677636732349089473540889855289757337736512303070584208009356148963914969296139250262532036044670829787749340381486502259003934029518250084291211843615602473277568939725661998743287881104315586743909166094376545879628924755210696938802618107247235991939968132055218667508994013042802832653274036857030938271120371493508056689333496510130233288415153533743215499505779621204995381781585793891494891361783339201260743345041742788508748141553059420124837675803038062487182700364305742864198416705040747639989644160240694540025745969599421913149372250571544665491768421384384768919101583170066211

RSA签名，最简单的RSA了，我不懂密码，但是deepseek思考这个居然死机了，其他AI脚本都给我生成好了

python
1e = 65537
2n = 27130058966678375728118690628915085193505679921867847648180394177280300520851322209827953313677610995977175396855400115719997248093217978788791475794191309606741245965521564249520758557425707716276357612383008262150259072257782913410617175802499340022388447047629022386881255413171331856263374853843961598744215379945538726953506454859112787839466674350352298690863753069032704210896554984332177790093120515590458961735089368466550753534317073220559703261053361251093853868715391272704827131460657841223647599202717920842362378900859386228898179814271143542598798022604629591665790726585192070387959726079579927264339
3flagc = 4172204809297405811985500677636732349089473540889855289757337736512303070584208009356148963914969296139250262532036044670829787749340381486502259003934029518250084291211843615602473277568939725661998743287881104315586743909166094376545879628924755210696938802618107247235991939968132055218667508994013042802832653274036857030938271120371493508056689333496510130233288415153533743215499505779621204995381781585793891494891361783339201260743345041742788508748141553059420124837675803038062487182700364305742864198416705040747639989644160240694540025745969599421913149372250571544665491768421384384768919101583170066211
4
5flag = pow(flagc, e, n)
6print(bytes.fromhex(hex(flag)[2:]))

bh{signing_is_not_encryption!}

UDS Challenge

为了做这题，我学习了一点点UDS基础，赶紧记下来做题。

首先感谢yichen大佬（小熊猫），然后推荐的文章是：

https://zhuanlan.zhihu.com/p/37310388

Simulation VIN

既然要读取VIN，我们需要知道VIN存储在哪个地方，这个地方就用DID表示，比如DID里面F190就是存储VIN的地方，为什么是F190呢？因为是国际标准的规定，当然也有一些段是留给车厂自己自定义的。

0xF190 VINDataIdentifier 该值应用于参考VIN号码。 记录数据内容和格式应由车辆制造商指定。

我们要通过DID读取里面的数据，而这个功能则是SID为22的服务

根据前面CAN帧的学习，我们的数据已经构造好了就是简单的22F190，总共三个字节长，首部加上长度，0322F190，现在我们需要一个CAN ID，通常使用7DF，这个ID非常重要，是功能寻址，也就是广播消息，他会向所有ECU发送数据

现在我们的CAN帧就是7DF#0322F190

先执行candump -l vcan0 &，他会在后台保存所有日志

然后发送上面构造的消息

cansend vcan0 7DF#0322F190

查看日志

1(1755797512.727185) vcan0 59E#9E10
2(1755797513.588803) vcan0 7DF#0322F190
3(1755797513.589071) vcan0 7E8#101462F190666C61
4(1755797513.728328) vcan0 59E#9E10
5(1755797514.729405) vcan0 59E#9E10

0x7E8 到 0x7EF 通常预留给ECU用于响应诊断请求。0x7E8 通常是第一个ECU的响应地址。

第一个字节10表示这是一个“首帧”，就是要返回的数据很长，一次发不完，它先发你第一个帧，这些帧叫连续帧。

第二个字节14代表长度，与前面的0构成帧的总长度，014转十进制代表长度是20个字节

第三个字节62代表肯定的响应。肯定的响应（Positive Response），首字节回复**[SID+0x40]，比如我发送的SID是0x22，这里加上0x40就是0x62。否定的响应（Negative Response），首字节回复0x7F**，第二字节回复刚才询问的SID。

第四、五个字节F190代表回显的DID，以便诊断工具知道这个响应对应哪个请求

第六、七、八个字节就是实际数据，当然只是第一部分。

所以我们现在需要问它要剩下的帧，这里需要发送一个叫做“流控制帧”的东西

7E0#3000000000000000

7E8实际上是7E0的rsp，所以我们需要向7E0发帧

第一个字节30，是流控制帧的标识符，3代表这是流控帧

第二个字节00是块大小，告诉ECU，在等待下一个流控制帧之前，可以连续发送多少个连续帧。00表示ECU可以一次性发送所有剩余的连续帧，无需等待新的流控帧。如果写01，就代表它每发一个连续帧，就要等我发一个流控帧。

第三个字节00代表连续帧的最小间隔时间（毫秒），00代表没有延迟，立即发送

剩余字节都是00，是用来填充的，没有意义

发送流控帧：cansend vcan0 7E0#3000000000000000

这里不知道为什么收不到消息，所以使用Arahat0师傅的方法，终端分屏，使用

candump vcan0,780:780监听0x7E8、0x7DF、0x7E0等消息，重复之前的发包

收到

1vcan0  7E8   [8]  21 67 7B 76 31 6E 5F 42
2vcan0  7E8   [8]  22 48 6D 61 63 68 33 7D

第一个字节21里的2是标识符，代表它是连续帧，1代表它是第一个帧

第二行同上

之前的三个字节，和这边的14个字节，总共17个字节，hex转ascii

flag{v1n_BHmach3}

Startup Message

重启ECU，这里用0x11服务的0x01子功能

Service ID: 0x11

子功能 (Sub-function)：

  • 0x01 → Hard Reset（硬复位，相当于掉电重启 ECU）
  • 0x02 → Key Off On Reset（模拟点火关闭再开启）
  • 0x03 → Soft Reset（软件复位，类似 MCU reset）
  • 0x04 → Enable Rapid Power Shutdown
  • 0x05 → Disable Rapid Power Shutdown

所以执行

cansend vcan0 7DF#0211010000000000

监听结果是

1candump vcan0,780:780
2vcan0  7DF   [8]  02 11 01 00 00 00 00 00
3vcan0  7E8   [8]  02 51 01 00 00 00 00 00
4vcan0  7DF   [8]  07 67 30 47 72 65 33 6E
5vcan0  7E0   [8]  30 00 00 00 00 00 00 00

我发送流控帧后没有结果，那么上一条不是我发送的7DF，就是ECU重启时的对外广播

去掉07长度，67 30 47 72 65 33 6E转ascii是g0Gre3n

Engine Trouble?

Hint说查询DTC，去备忘录找了一下，

0x19 读取故障码信息 ReadDTCInformation

那就用0x19服务，但是读取DTC也有很多方式，查询子服务就能看到。题目说了车灯亮了，这是一个状态，我们要通过状态读取DTC，就是0x02子服务

查询这个需要掩码来查询，掩码对应内容是

BitMeaning
0testFailed
1testFailedThisMonitoringCycle
2pendingDTC
3confirmedDTC
4testNotCompletedSinceLastClear
5testFailedSinceLastClear
6testNotCompletedThisMonitoringCycle
7warningIndicatorRequested

我们要读取confirmedDTC，bit 3就是1，其余不需要就是0，所以就是00001000，转十进制就是8

所以我们广播这个命令：cansend vcan0 7DF#03190208

收到vcan0 7E8 [8] 07 59 02 08 3E 9F 01 AB

所以数据是3E 9F 01 AB，DTC固定返回三个字节，AB是状态，舍去

参考https://blog.csdn.net/qq_40309666/article/details/133955750

00P 动力总成
01C 底盘
10B 车身
11U 网络

3E 9F 01转二进制得到00111110 10011111 00000001

前两个数字就是上面表中的对应关系。其余转回去

P3E9F01，根据提示的格式，答案是P3E9F-01

Secrets in Memory?

让从内存读数据，内存地址从0xC3F80000开始

从地址读内存是23号服务

我们需要构建的can帧是7DF#072314C3F80000FF

07是长度，23是SID ，14代表地址用4个字节表示，读取的块大小用一个字节表示

C3F80000就是地址，FF就是一个字节能读的最大长度。

发送后补一个cansend vcan0 7E0#3000000000000000 流控帧

又遇到收不到连续帧的问题

cansend vcan0 7DF#072314C3F80000FF && sleep 0.01 && cansend vcan0 7e0#3000000000000000

这样可以

可以看到输出了很多行数据，后面大片是0，仅有的几行数据转码是

Block Harbor 2022 Mach-E Simulator Version 1.0.

写脚本吧，不知道距离给的地址有多远呢

脚本循环读取内存，每次读取0xFF的大小，然后加上0xFF的地址，一直读取到我们预设的endAddr

python
 1import can
 2import time
 3import binascii
 4
 5bus = can.Bus(interface="socketcan",channel="vcan0")
 6recv = "[DATA]:"
 7# 开始地址已有，结束地址选大点
 8startAddr=0xC3F80000
 9endAddr=0xC3F88000
10
11#循环读取内存数据
12for readAddr in range(startAddr,endAddr,0xFF):
13    #分割地址
14    byte1=(readAddr >>24)& 0xFF
15    byte2=(readAddr >>16)& 0xFF
16    byte3=(readAddr >>8)& 0xFF
17    byte4=readAddr& 0xFF
18    # 构造数据
19    candata = [0x07, 0x23, 0x14, byte1, byte2, byte3, byte4, 0xFF]
20    #构造读取内存can帧
21    readMem = can.Message(arbitration_id=0x7DF, is_extended_id=False, dlc=8, data=candata)
22    bus.send(readMem,timeout=0.2)
23    frameCount=0
24    # 一帧7字节数据，36帧252，基本能覆盖完了
25    while frameCount<36:
26        msg=bus.recv(timeout=0.1)
27        if msg is not None:
28            # 判断是否是首帧
29            if frameCount==0:
30                # 首帧要去掉前3个字节，也就是前6个字母
31                recv+=binascii.hexlify(msg.data).decode('utf-8')[6:]
32                # 收到首帧立马发流控帧
33                FC=can.Message(arbitration_id=0x7E0,is_extended_id=False,dlc=8,data=[0x30, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00])
34                bus.send(FC,timeout=0.2)
35            else:
36                recv+=binascii.hexlify(msg.data).decode('utf-8')[2:]
37            frameCount+=1
38        else:
39            break
40bus.shutdown()
41print(recv)

输出很长的十六进制字符串，不知道为什么，无论我用fromhex，还是unhexlify都报错，可能是这俩函数太严格，毕竟我们截取的字符串长度不够标准

所以执行脚本是用xxd转码

bash
1python readmem.py |xxd -r -p

xxd比较宽松，可以得到flag{mem+r34d}

注：以前模拟器内置python-can库，现在没有了，需要pip安装，但提示会破坏系统环境，venv没权限，pipx也没有。所以强制安装python-can：pip install python-can --break-system-packages

Security Access Level 3

这题靠猜算法，在CTF中4个字节的种子最基本的算法就是取反、移位、异或0x12345678

取反其实就是和0xFFFFFFFF异或，取反另一种写法是~seed

这题就是取反，种子是0x1337

python异或比较方便

python
1>>> hex(0x1337 ^ 0xFFFF)
2'0xecc8'

用Cyberchef也可以，不过要先把input作为Hex处理，再异或，然后以Hex输出：

https://cyberchef.io/#recipe=From_Hex(‘Auto’)XOR(%7B’option’:‘Hex’,‘string’:‘FFFF’%7D,‘Standard’,false)To_Hex(‘None’,0)&input=MTMzNw

Web

Sorry, But Your Princess is in Another Castle

jwt暴破

我本以为是解开后，伪造一下admin，但是解开后发现有password字段。不过这个题是用hashcat暴破 JWT HS256算法的密钥。

可以使用常见的密码注册，比如admin123，然后暴破 jwt token

这里使用例子里的json登录：

json
1{
2  "username": "example",
3  "email": "example@example.com",
4  "password": "example123"
5}

可以使用密钥解开password，不过这题admin的密码就是密钥

hashcat命令：

bash
1hashcat -m 16500 -a 0 "C:\Users\Tajang\Desktop\1.txt" "D:\Tools\字典\密码\rockyou.txt"

16500代表HS256算法，-a 0代表字典攻击

得到密钥为princess

账号为admin，登录即可拿到 token，然后get 访问/protected，header写：authorization: Bearer JWT_TOKEN值

bash
1curl -X GET http://celsius.blockharbor.io:5011/protected -H "Authorization: Bearer eyJhbGciOiJIUzI1NiIsInR5cCI6IkpXVCJ9.eyJ1c2VybmFtZSI6ImFkbWluIiwiZW1haWwiOiJhZG1pbkBiaC5pbyIsInBhc3N3b3JkIjoiJDJiJDEwJFNiNXZ0WU44c3dYR1dtbTNrdmYvbE8uNDdoV3BBQnBQQ2xYNjN2VDZrYWxRTVpYeWVyTy9XIiwiaWF0IjoxNzU3MzQ5MDM1LCJleHAiOjE3NTc3ODEwMzV9.0HdP-jCxBA7DQ1225uzJqsNSklRngOzB9h471UpUD7g"
2{"message":"Welcome admin! Here's the flag: bh{cr4ck_d3m_jwts}"}

拿到flag：bh{cr4ck_d3m_jwts}

ICSim

Unlock my door

关于安装 ICSim 我写了一篇文章：Ubuntu与ICSim安装二三事

在几年前想转车联网安全的时候也出过一期 ICSim 视频：车联网安全-把玩汽车安全模拟器ICSim

指定了种子是10000

启动仪表盘：./icsim -s 10000 vcan0

启动控制器：./controls -s 10000 vcan0

我的方法是对比法：

candump vcan0 > 1.log，什么都不做等待10秒钟。

candump vcan0 > 2.log，启动后只执行一次开门指令，其他转向加速都不要做

提取出两个日志的CAN ID，然后对比，发现 2.log 多出了 5C6，所以答案就是0x5C6

如何对比？

笨方法是提取出CAN ID，去重排序，用肉眼看，或者使用BCompare工具对比

快速方法是：

bash
1comm -13 <(awk '{print $2}' 1.log | sort | uniq) <(awk '{print $2}' 2.log | sort | uniq)

这个命令会提取CAN ID ，输出 2.log 独有，而 1.log 没有的内容

comm命令会一列列地比较两个已排序文件的差异，并将其结果显示出来，如果没有指定任何参数，则会把结果分成3行显示：第1行仅是在第1个文件中出现过的列，第2行是仅在第2个文件中出现过的列，第3行则是在第1与第2个文件里都出现过的列。若给予的文件名称为”-“，则comm指令会从标准输入设备读取数据。 -1 不显示只在第1个文件里出现过的列 -2 不显示只在第2个文件里出现过的列 -3 不显示只在第1和第2个文件里出现过的列

Speedometer ArbId

速度是一直有指令发送的，所以上面的方法不再奏效

我们需要一直加速，观察哪个CAN ID 的数据帧也在不断增大，使用sniffer观察变动的数据

cansniffer -c vcan0

可以看到779数值在增加，达到最大速度后不再变化

0x779

Steganography

Alpha Beta Gamma Delta

课程自己给了隐写术代码，杂项不太会，通过脚本反推一下如何隐藏的吧

python
 1#读取整个日志文件内容，并去除每行末尾的换行符，保存到 data 列表中
 2with open('./chall-log.txt','r') as fd:
 3
 4        data = [x.strip() for x in fd.readlines()]
 5
 6#从一行日志中提取出时间戳的小数部分（毫秒/微秒级），并转换为整数返回
 7def convert_line_to_ts(line):
 8
 9        ts = line.split(' ')[0][1:-1].split('.')[1]
10
11        return int(ts)
12#获取第一行的时间戳小数部分作为初始值
13last = convert_line_to_ts(data[0])
14#遍历其余每一行，计算当前行和上一行时间戳差值，并将其视为 ASCII 码输出对应的字符。
15for line in data[1:]:
16
17        ts = convert_line_to_ts(line)
18
19        print(chr(ts - last),end='' )
20
21        last = ts
22
23print()

bh{delta_force_five!}

Reversing

Reversing #1

逆向咯

We managed to get the source code to a program running on an ESP32, can you reverse it and find an input that unlocks it? 我们成功获取了运行在 ESP32 上的程序源代码，你能对其进行逆向分析，并找出一个能解锁它的输入吗？

就是典型的CTF题，看逻辑写脚本破解密码

给的代码是：

c
 1#define MAX_SIZE 32
 2
 3const uint32_t a = 1103515245;
 4const uint32_t c = 12345;
 5const uint32_t m = 2147483647;
 6uint32_t seed = 1337;
 7
 8unsigned char user_input[MAX_SIZE];
 9const uint32_t STATE[4] = {0x1e48add6, 0xaaa7550c, 0x18df53bf, 0xe6af1116};
10
11uint32_t start[] = {0x0, 0x0, 0x0, 0x0};
12
13uint32_t gen_random(void) {
14  seed = (uint32_t)(((uint32_t)a * (uint32_t)seed + (uint32_t)c) % m);
15  return (uint32_t)seed;
16}
17
18void setup() {
19  Serial.begin(115200);
20  Serial.println("==================================================");
21  Serial.println("=               SECURE LOCK - v0.5               =");
22  Serial.println("==================================================");
23}
24
25int check_pass(uint32_t start[]) {
26    Serial.println("checking\n");
27    uint32_t temp = 0;
28    for (int i = 0; i < 4; ++i) {
29      temp = start[i];
30      temp *= (uint32_t)0xcafebeef;
31      temp += (uint32_t)gen_random();
32      temp *= (uint32_t)0xfacefeed;
33      temp ^= (uint32_t)gen_random();
34
35      if ((uint32_t)temp != (uint32_t)STATE[i]) {
36        return 0;
37      }
38    }
39    return 1;
40}
41
42void loop() {
43  
44  memset(user_input,0,MAX_SIZE);
45  memset(start, 0, 16);
46
47  Serial.println("Enter your password: ");
48
49  while (Serial.available() == 0) {
50    delay(100);
51  }
52
53  Serial.readBytes(user_input, MAX_SIZE);
54  
55  Serial.println();
56  for (int i = 0; i < 4; i++) {
57    
58    start[i] |= ((uint32_t)user_input[(i * 4)]   << 24);
59    start[i] |= ((uint32_t)user_input[(i * 4)+1] << 16);
60    start[i] |= ((uint32_t)user_input[(i * 4)+2] << 8);
61    start[i] |= ((uint32_t)user_input[(i * 4)+3] << 0);
62
63    Serial.println(start[i],HEX);
64  }
65
66  if (check_pass(start) == 1) {
67    Serial.print("Thats it!\r\nSubmit in the format FLAG{");
68    for (int i = 0; i < 4; i++) {
69          Serial.print(start[i],HEX);
70    }
71    Serial.println("}");
72    while (true) { delay(1000); }
73  }
74
75  // Failed, just spin
76  Serial.println("Incorrect password!");
77  while (true) {delay(1000); }
78}

首先是输入最大16字节，每四个一组，大端序存到start数组中

然后每组放到check_pass中做计算，分别判断是否等于四个预设值

这里check_pass虽然有随机数，但是伪随机，所有初始值都给了，每次返回的seed我们也就知道了

脚本：

python
 1#define MAX_SIZE 32
 2
 3a = 1103515245;
 4c = 12345;
 5m = 2147483647;
 6seed = 1337;
 7
 8STATE = [0x1e48add6, 0xaaa7550c, 0x18df53bf, 0xe6af1116]
 9
10MOD = 2**32
11
12def inv(x):
13    # 计算模 2^32 下的乘法逆元
14    return pow(x, -1, MOD)
15
16inv_CAFE = inv(0xcafebeef)
17inv_FACE = inv(0xfacefeed)
18
19
20def gen_random():
21    global seed
22    seed = ((a * seed + c)% MOD) % m
23    print(hex(seed))
24    return seed
25
26# 每组两次随机，总共8组，所以循环八次
27rands = []
28for _ in range(8):
29    rands.append(gen_random())
30
31# 然后每段特征码和密钥，随机数反解密码
32start=[]
33for i in range(4):
34    r1 = rands[i * 2]
35    r2 = rands[i * 2 + 1]
36    temp = STATE[i] ^ r2
37    temp = (temp * inv_FACE) % MOD
38    temp = (temp-r1) % MOD
39    start_i=(temp * inv_CAFE) % MOD
40    start.append(start_i)
41
42# 转换成字节
43flag_bytes = b""
44for val in start:
45    flag_bytes += val.to_bytes(4, byteorder='big')
46
47
48print("Recovered input:", flag_bytes.hex())
49print("flag{", end="")
50for val in start:
51    print(f"{val:08x}", end="")
52print("}")

这个脚本很丑陋，非常手工，有一点怎么问AI也无法解决，就是生成随机数那个函数，youtube的官方视频，随机数数组和我的不一样，我逻辑并没问题，后来看了chamd5的wp，才知道要手动取低32位。因为源码是C语言，无符号变量进行的运算，溢出了会自动取32位，也就是模 2^32。包括后面的加减乘除都是在mod 2^32的情况下进行的。python的运算是无限精度的，所以它不会自动溢出取模，要手动。

ChaMD5的脚本也有一个不优雅的地方，他的随机数函数是：

python
1def gen_random():
2    return ((((((a&0xffffffff) * (seed&0xffffffff))&0xffffffff) + (c&0xffffffff))&0xffffffff) % m)&0xffffffff

使用 0xffffffff 每个变量都取低32位，但实际上，只需要整体模2^32就可以：

python
1((a * seed + c)% MOD) % m

这里的hint是z3，ChaMD5也是用的z3，学了下z3，牛逼，这个引擎好像是通过剪枝缩小解的范围，然后暴破

不过也挺快的

这里用z3写一个脚本：

python
 1from z3 import *
 2a = 1103515245
 3c = 12345
 4m = 2147483647
 5seed = 1337
 6MOD=1 << 32
 7STATE = [0x1e48add6, 0xaaa7550c, 0x18df53bf, 0xe6af1116]
 8flag = [BitVec(f'start_{i}', 32) for i in range(4)]
 9CAFE = 0xcafebeef
10FACE = 0xfacefeed
11
12s = Solver()
13def gen_random():
14    global seed
15    seed = ((a * seed + c)% MOD) % m
16    return seed
17
18seeds=[]
19for _ in range(8):
20    seeds.append(gen_random())
21
22for i in range(4):
23    temp=flag[i]
24    temp = (temp * CAFE)% MOD
25    temp = (temp + seeds[i * 2]) % MOD
26    temp = (temp * FACE) % MOD
27    temp = (temp ^ seeds[i * 2 + 1]) % MOD
28    s.add(temp==STATE[i])
29
30# Check for solution
31if s.check() == sat:
32    model = s.model()
33    result_start = [model.eval(flag[i]).as_long() for i in range(4)]
34    user_input = bytearray()
35    for value in result_start:
36        user_input.extend(value.to_bytes(4, 'big'))
37    print("Correct input (in hex):", user_input.hex().upper())
38else:
39    print("No solution found")