PlaidCTF 2025
May 1st, 2025
So I played plaidctf some time ago. It was pretty fun, but sadly I only played for like 5 hours since I had to do other work.
WHAT? Other work?
I know, doing work instead of playing ctf...Completely unacceptable >:(
Anyways here's writeups for a couple challenges I solved
Innov8: Excav8
This was a pretty neat crypto? challenge.
import subprocess
secret = open('secret.txt').read().strip()
secretbits = ''.join(f'{ord(i):08b}' for i in secret)
output = []
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 gen.js', shell=True).decode().split()]
for i in output:
print(i)
we are also given a output.txt file
0.7337623820947822
0.7422123750824269
0.8899813769451984
0.4179450530394614
0.3580459144486847
0.34814267246372055
0.5568139014001128
0.06917593168568936
0.5207352761362871
0.13636263742870747
...
14976 total lines
So, this python script reads a secret message (presumably the flag) and then for each bit, it calls a js script with either d8 or node (both are js engines)
Let's take a look at this script.
for (let i = 0; i < 24; i++) {
console.log(Math.random());
}
Huh, we just call Math.random()?
Ok so the internal implementation of Math.random() must somehow differ between node and d8 in such a way that we can tell the difference and then infer whether a bit was a one or a zero.
Helpfully, I remembered watching a video on using Z3 to predict random numbers generated with Math.random()
Maybe we can use this?
I started playing a bit using Node and d8 and I realized that when I tried using my Z3 script it would return sat for numbers generated with Node and unsat for numbers generated with d8! It kinda makes sense, since my solver script was written based on the implementation of Node, if the d8 implementation is different, of course my solvescript is not going to be able to predict the next number!
Now that we have a way to tell the difference, we can guess all the bits!
Here is the solvescript I wrote:
from z3 import *
import struct
import copy
secrets = ""
def get_next(sequence_in):
global secrets
sequence = copy.deepcopy(sequence_in)
sequence = sequence[::-1]
solver = Solver()
state0, state1 = BitVecs("state0 state1", 64)
# do the xorshifting
for i in range(len(sequence)):
s1 = state0
s0 = state1
state0 = s0
s1 ^= s1 << 23
s1 ^= LShR(s1,17)
s1 ^= s0
s1 ^= LShR(s0,26)
state1 = s1
# pack as double and re interpret as unsigned long long
float_64 = struct.pack('d', sequence[i]+1)
u_long_long_64 = struct.unpack("<Q", float_64)[0]
# get mantissa
mantissa = u_long_long_64 & ((1 << 52) - 1)
solver.add(int(mantissa) == z3.LShR(state0,12))
print(solver.check())
if solver.check() == z3.sat:
model = solver.model()
states = {}
for state in model.decls():
states[state.__str__()] = model[state]
#print(states)
state0 = states["state0"].as_long()
u_long_long_64 = (state0 >> 12) | 0x3FF0000000000000
float_64 = struct.pack("<Q", u_long_long_64)
next_sequence = struct.unpack("d", float_64)[0]
next_sequence -= 1
secrets += '1'
return next_sequence
else:
secrets += '0'
return "unsat"
sequence = open("./output.txt").readlines()
sequence = [float(i.strip()) for i in sequence]
subsequences = [sequence[i:i+24] for i in range(0,len(sequence),24)]
for subseq in subsequences:
get_next(subseq)
def bits_to_string(bits):
"""Converts a string of bits to a string of characters."""
return ''.join(chr(int(bits[i:i+8], 2)) for i in range(0, len(bits), 8))
print(bits_to_string(secrets))
Pretty cool huh? It's actually pretty slow, it took like 11 minutes to run in my computer. Which is actually interesting since the fastest solve was faster than that, which means theres a different and faster way to solve this challenge! I guess I could have run every bit in parallel which would have sped things up.
flag: PCTF{BuilD1nG_v8_i5_SuCh_4_pa1N...}
Prospector's Claim
This one was an RE challenge, which I also solved using Z3... I guess I really like SAT solvers :)
We are given a binary, which I promptly threw into Ghidra to see what was going on.
void bump(int* param_1){
*param_1 = *param_1 + 1;
return;
}
undefined8 main(void)
{
char local_55 [65];
setvbuf(_stdout,(char *)0x0,2,0);
printf("=== The Prospector\'s Claim ===\n");
printf("Old Man Jenkins\' map to his modest gold claim has been floating around\n");
printf("Fool\'s Gulch for years. Most folks think it\'s worthless, but you\'ve\n");
printf("noticed something peculiar in the worn-out corners...\n\n");
printf("Enter the claim sequence: ");
fgets(local_55,0x41,_stdin);
if (local_55[27] == '2') {
bump(0,&score);
}
if ((byte)(local_55[31] ^ local_55[24]) == 0xaa) {
bump(0,&score);
}
if ((char)(local_55[31] + local_55[46]) == -0x70) {
bump(0,&score);
}
if ((char)(local_55[59] + local_55[36]) == -0x7f) {
bump(0,&score);
}
if (local_55[13] == -0x42) {
bump(0,&score);
}
if (local_55[32] == 'd') {
bump(0,&score);
}
if (local_55[26] == '1') {
bump(0,&score);
}
if (local_55[42] == '9') {
bump(0,&score);
}
if ((char)(local_55[45] + local_55[63]) == -0x6d) {
bump(0,&score);
}
if (local_55[50] == '1') {
bump(0,&score);
}
if ((char)(local_55[1] + local_55[15]) == '8') {
bump(0,&score);
}
if ((byte)(local_55[13] ^ local_55[35]) == 0x8e) {
bump(0,&score);
}
if ((byte)(local_55[1] ^ local_55[46]) == 0x71) {
bump(0,&score);
}
if (local_55[42] == -0x4c) {
bump(0,&score);
}
// ...
// many many more constraints
// ...
if ((byte)(local_55[45] ^ local_55[18]) == 0x91) {
bump(0,&score);
}
if (local_55[18] == 'd') {
bump(0,&score);
}
if (score < DAT_00115054) {
if (score < DAT_00115050) {
if (score < DAT_0011504c) {
printf("\nThat claim\'s as empty as a desert well in August.\n",
(ulong)(uint)(score - DAT_0011504c));
printf("Not a speck of gold to be found. Try another spot, prospector!\n");
}
else {
printf("\nYou\'ve been swindled, partner! All you\'ve dug up is worthless rock.\n",
(ulong)(uint)(score - DAT_0011504c));
printf("The saloon erupts in laughter as you show off your \'treasure\'.\n");
printf("Keep prospecting - or take up farming instead!\n");
}
}
else {
printf("\nA few gold flakes glimmer in your pan, but it ain\'t enough to stake a claim.\n",
(ulong)(uint)(score - DAT_00115050));
printf("The assayer laughs you out of his office. \"Come back when you\'ve got\n");
printf("something worth my time, greenhorn!\"\n");
}
}
else {
printf(&DAT_00104850,(ulong)(uint)(score - DAT_00115054));
printf("You\'ve struck a rich vein of gold! Your claim is officially recorded\n");
printf("at the assayer\'s office, and the flag is yours: %s\n",local_55);
}
return 0;
}
Ok there's a lot to take in here. First, this is a classic flag checker. You give it some input and then if it satisfies some conditions, you get the flag!
Ok, I see something like this and I immediately think of just throwing angr at it.
I tried normal angr... OOMKILLED
I tried lazy solves..... OOMKILLED
I tried veritesting........ OOMKILLED
...
Ok maybe not an angr challenge
I copy pasted just the constraints into a file I could parse with python and then asked Z3 to give me an input that would satisfy all the constraints.
unsat
Huh!? Did I mess something up?
I started looking at the constraints I generated and I saw some of them had been simplified to false...
I counted the total number of constraints and it happened that there was more constraints than the number of points you needed to get the highest score!
So you don't need to satisfy all constraints, just enough to get the score you need.
The problem is to figure out which ones to solve.
But why do hard work if you can just let Z3 figure it out for you! :)
The idea is to have a symbolic variable that keeps track of your score. Then add a logic If statement that adds 1 to it if your constraint is true or 0 if it is false. Then solve for score to be the value you want!
Here's the solver:
import re
from z3 import *
import sys
def parse_constraints_file(filename):
# Initialize Z3 solver
solver = Solver()
# Create a symbolic array for local_55
# Using 8-bit BitVecs to represent bytes/chars
local_55 = [BitVec(f'local_55_{i}', 8) for i in range(64)] # Assuming size 64
bitone = BitVecVal(1,32)
bitzero = BitVecVal(0,32)
bit_total = BitVecVal(0,32)
# Add constraints for printable ASCII characters
for i in range(64):
solver.add(local_55[i] >= 32)
solver.add(local_55[i] <= 126)
# Read the constraints file
with open(filename, 'r') as f:
content = f.read()
# Extract and process each constraint
constraints = []
for line in content.splitlines():
line = line.strip()
# Skip empty lines, lines with bump function call, or closing braces
if not line or "bump" in line or line == '}':
continue
# Extract the condition part between 'if' and the opening brace
match = re.search(r'if\s*\((.*?)\)\s*{', line)
if match:
constraint = match.group(1).strip()
constraints.append(constraint)
# Process different types of constraints
if "==" in constraint:
left_side, right_side = [s.strip() for s in constraint.split("==")]
# Parse each side of the equation independently
left_expr = parse_expression(left_side, local_55)
right_expr = parse_expression(right_side, local_55)
# Add the constraint to the solver
if not isinstance((left_expr == right_expr), bool):
bit_total += If(left_expr == right_expr,bitone,bitzero)
else:
print("FALSE EXPRESSION ",left_expr, right_expr)
solver.add(bit_total >= 281)
return solver, local_55, constraints
def parse_expression(expr, local_55):
expr = expr.strip()
# Direct character literal
if expr.startswith("'") and expr.endswith("'") and len(expr) == 3:
return ord(expr[1])
# Direct numeric value
if expr.startswith("0x"):
return int(expr, 16)
elif expr.startswith("-0x"):
return (256 - int(expr[1:], 16)) & 0xff
elif expr.startswith("-") and expr[1:].isdigit():
return (256 - int(expr[1:])) & 0xff
elif expr.isdigit():
return int(expr)
# Direct local_55 array access
local_55_match = re.match(r'^local_55\[(\d+)\]$', expr)
if local_55_match:
idx = int(local_55_match.group(1))
return local_55[idx]
# Handle type casts
cast_match = re.match(r'\((byte|char)\)\((.*)\)', expr)
if cast_match:
cast_type, inner_expr = cast_match.groups()
inner_result = parse_expression(inner_expr, local_55)
return inner_result & 0xff
# XOR operation
xor_match = re.search(r'local_55\[(\d+)\]\s*\^\s*local_55\[(\d+)\]', expr)
if xor_match:
idx1, idx2 = int(xor_match.group(1)), int(xor_match.group(2))
return local_55[idx1] ^ local_55[idx2]
# Addition operation
add_match = re.search(r'local_55\[(\d+)\]\s*\+\s*local_55\[(\d+)\]', expr)
if add_match:
idx1, idx2 = int(add_match.group(1)), int(add_match.group(2))
return local_55[idx1] + local_55[idx2]
print(f"Warning: Could not parse expression: {expr}")
return None
def solve_and_print(solver, local_55, constraints):
print("Z3 Constraints:")
for i, constraint in enumerate(constraints):
print(f"{i+1}. {constraint}")
print("\nSolver assertions:")
for assertion in solver.assertions():
print(assertion)
print("\nChecking satisfiability...")
if solver.check() == sat:
print("Constraints are satisfiable!")
model = solver.model()
# Create a solution array
solution = {}
for i in range(64):
if model.get_interp(local_55[i]) is not None:
val = model.eval(local_55[i]).as_long()
solution[i] = (val, chr(val) if 32 <= val <= 126 else '.')
# Print the solution in order of indices
print("\nSolution:")
for i in sorted(solution.keys()):
print(f"local_55[{i}] = {solution[i][0]} ('{solution[i][1]}')")
# Print the solution as a string if it seems to be a flag/message
if solution:
max_idx = max(solution.keys())
result = ""
for i in range(max_idx + 1):
if i in solution:
result += solution[i][1]
else:
result += "?"
print(f"\nResult string: {result}")
else:
print("Constraints are not satisfiable.")
def main():
if len(sys.argv) != 2:
print(f"Usage: {sys.argv[0]} <constraints_file>")
sys.exit(1)
filename = sys.argv[1]
solver, local_55, constraints = parse_constraints_file(filename)
solve_and_print(solver, local_55, constraints)
if __name__ == "__main__":
main()
flag:
PCTF{24d16126d6739d6ada82b125534d2ae2324b39ed72e5a1200c5ac96200}