HTB CTF 2026 Writeups

Phuc000 included in category reverse

2026-07-30 2026-07-30 673 words 4 minutes

Contents

Writeup for some rev challenges in the event.

Overview

Better not get myself rusty so I participated in this year HTB together with my company team. Too bad work was so stressful I had to settle with 2 challenges.

Cinderbound

Challenge Information

Given file: cinderbound.mpy

Warm up. Dump into bytecode with Micropython

1

python3 mpy-tool.py -d cinderbound.mpy

We obtain the easily encrypted code and we can obtain the flag by doing the reverse rotation.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16


TARGET = [
    57,129,154,31,
    199,192,73,243,
    43,176,255,173,
    54,203,67,15,
]

state = 90
flag = []

for i, enc in enumerate(TARGET):
    ch = enc ^ state ^ ((13 * i) & 0xff)
    flag.append(chr(ch))
    state = (state + ch) & 0xff

print("".join(flag))

HTB{c1nd3rbound_v0w5}

Ringtrue

Challenge Information

Given file: ringtrue

okay I really had fun with this one. It makes me remember my Introduction to AI class. The program required us to input 8 numbers. The code do something akin to a vector transformation and compare to static data ECHO_S, welp time for z3 to shine upon us once more. We just need to mimic the logic of what is done.

One of the issue I saw was how to dump the data from IDA with correct format. And this script might be useful for future dumping.

 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


import struct
import json

def read_i8(addr, n):
    return list(struct.unpack(
        f"<{n}b",
        get_bytes(addr, n)
    ))

def read_i32(addr, n):
    return list(struct.unpack(
        f"<{n}i",
        get_bytes(addr, n * 4)
    ))

def read_i64(addr, n):
    return list(struct.unpack(
        f"<{n}q",
        get_bytes(addr, n * 8)
    ))

def matrix8(x):
    return [
        x[i:i + 8]
        for i in range(0, len(x), 8)
    ]

layers = {}

# 8x8 signed int8 weights
for name in [
    "L0_W",
    "L1_W",
    "L2_W"
]:
    addr = get_name_ea_simple(name)

    print(name, hex(addr))

    layers[name] = matrix8(
        read_i8(addr, 64)
    )

# 8 signed int32 biases
for name in [
    "L0_B",
    "L1_B",
    "L2_B"
]:
    addr = get_name_ea_simple(name)

    print(name, hex(addr))

    layers[name] = read_i32(addr, 8)

# 8 signed int64 values
addr = get_name_ea_simple("ECHO_S")

print("ECHO_S", hex(addr))

layers["ECHO_S"] = read_i64(addr, 8)

print(json.dumps(
    layers,
    indent=4
))

Now onto the solver using value obtained from the dumper.

  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


from z3 import *

L0_W = [
    [5,13,10,14,1,0,-15,12],
    [4,4,3,1,11,-3,-10,-1],
    [10,3,1,-11,-12,5,12,14],
    [10,2,3,7,7,-6,-1,-4],
    [16,10,-10,12,5,6,2,-5],
    [15,-1,-7,-3,9,7,1,-5],
    [6,-12,-8,-10,0,7,-15,15],
    [4,-9,-4,12,-4,16,15,5]
]

L1_W = [
    [14,-1,13,-3,-15,10,1,-14],
    [16,16,12,-7,14,5,-8,-7],
    [-2,3,7,15,-12,11,1,12],
    [-9,-8,-14,-2,-3,3,-1,0],
    [-11,-13,6,7,-3,-4,0,16],
    [-4,2,-4,11,16,-10,5,-5],
    [-8,-4,1,8,3,-14,-12,6],
    [-13,-12,5,13,14,-15,15,5]
]

L2_W = [
    [9,-15,0,-16,2,-15,6,-6],
    [8,0,-5,-4,-1,10,-7,3],
    [-9,-15,-14,-7,-5,-4,-11,9],
    [9,-9,15,13,1,-8,1,-3],
    [-13,9,-8,4,-16,11,11,12],
    [-10,-12,-1,-10,-1,11,6,-4],
    [6,-4,-5,-13,-3,8,6,-4],
    [-2,-12,-15,4,16,-9,13,-13]
]

L0_B = [
    541,-548,1968,1610,68,-1078,-42,-2020
]

L1_B = [
    -1709,704,1565,304,-209,1690,-1151,245
]

L2_B = [
    506,-234,1551,1479,1058,1130,1320,330
]

ECHO_S = [1542223, 574187, -2694563, -3518303, 383776, 576877, 2637871, -2518822]

def dense_z3(W,B,x):

    result=[]

    for i in range(8):

        value=B[i]

        for j in range(8):
            value += W[i][j]*x[j]

        result.append(value)

    return result

def activate_z3(values):

    return [
        If(v < 0, v*2, v)
        for v in values
    ]

x=[
    Int(f"x{i}")
    for i in range(8)
]

solver=Solver()

for v in x:
    solver.add(v >= -2147483648)
    solver.add(v <= 2147483647)

y1=dense_z3(L0_W,L0_B,x)
y1=activate_z3(y1)

y2=dense_z3(L1_W,L1_B,y1)
y2=activate_z3(y2)

y3=dense_z3(L2_W,L2_B,y2)

for i in range(8):
    solver.add(
        y3[i]==ECHO_S[i]
    )

print(solver.check())


if solver.check()==sat:

    model=solver.model()

    solution=[
        model[x[i]]
        for i in range(8)
    ]

    print(solution)

    # 83 97 108 116 67 114 119 110

HTB{h3y_s1gn3t_1_4m_y0ur_k1ng}