Skip to content

Instantly share code, notes, and snippets.

Last active July 6, 2023 08:27
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save RubenBrocke/248e80151e2ff4d4ea67a5af792ec4d6 to your computer and use it in GitHub Desktop.
Save RubenBrocke/248e80151e2ff4d4ea67a5af792ec4d6 to your computer and use it in GitHub Desktop.
Writeup for the pwnykey challenge of UIUCTF 2023

Pwnykey [rev 400]


Can you obtain a valid pwnyOS activation key?

link files

Looking around

The website

Visiting the link shows the following webpage: website

A quick test using the key 00000-00000-00000-00000-00000 returns the following message:

Incorrect key

The files

The provides files have the following filestructure

├─ .devicescript/
│  ├─ flash/
│  │  ├─ sim.bin
├─ static/
│  ├─ index.html
│  ├─ setup.png
│  ├─ setup-disks-pc.bmp
├─ Dockerfile
├─ flag.txt
├─ keychecker.devs
├─ package.json
├─ package-lock.json

As can be seen it contains a python application, A Dockerfile and a file called keychecker.devs. Another important thing to note is the inclusion of the .devicescript folder. As it turns out the keychecker.devs contains the bytecode for a devicescript program.


Lets first look at the python app to see what kind of functionality it has.

The python app

The first thing to notice about the application is that it's the website hosted on the link provided. Furthermore it uses flask to expose a single endpoint.


This function can be called using both GET and POST requests and does something different depending.


  1. Get the key from the post parameters
  2. Aquire a lock
  3. Set the stored key to the key from the parameters
  4. Run the command ./node_modules/devicescript/cli/devicescript run -t keychecker.devs
  5. For each line in the output of the command
    1. If the line contains success! return the flag


  1. Check of the request came from
  2. Release a lock
  3. Return the stored key

The devicescript pogram

As mentioned the keychecker.devs file called from the website is a devicescript file. Devicescript is a programming language created by microsoft who describes it as TypeScript for Tiny IoT Devices. The repository for it can be found here.

Running the keychecker

The website showed how to run they keychecker file. So after installing devicescript using npm or starting the Dockerfile and executing the python app if needed run the following command:

./node_modules/devicescript/cli/devicescript run -t keychecker.devs

It returns the following output:

using devs: v2.13.9, runtime: v2.13.9, node: v20.3.0 from /home/panda/CTF/UIUCTF/pwnykey/node_modules/@devicescript/cli/built
WASM> DeviceScript Simulator (WASM) v2.13.9; file v2.11.6
WASM> start: (no name) (null)
WASM> start!
WASM> connecting to tcp://localhost:80
WASM> socket tcp://localhost:80 open undefined
WASM> req: GET /check HTTP/1.1
WASM> user-agent: DeviceScript fetch()
WASM> accept: */*
WASM> host: localhost
WASM> connection: close
WASM> socket tcp://localhost:80 close undefined
WASM> server: Werkzeug/2.3.2 Python/3.11.3
WASM> date: Tue, 04 Jul 2023 18:49:18 GMT
WASM> content-type: text/html; charset=utf-8
WASM> content-length: 29
WASM> connection: close
WASM> fetched key: 00000-00000-00000-00000-00000
WASM> key format ok
WASM> Unhandled exception
WASM> Exception: Error
WASM>  message: Invalid key
WASM>  at main_F0 (pc:562)
WASM> Unhandled exception
PANIC 60005
test failed
Error: test failed

Closely looking at the output it shows the lines: connecting to tcp://localhost:80 and req: GET /check HTTP/1.1. This indicates the program sends a GET request to the /check endpoint on the website. Referencing back the the code of the website shows the program would be originating from and thus would be able to receive the key. However further down the output it shows the line WASM> message: Invalid key. As suspected the keychecker.devs is responsible for checking if a provided key is valid or not. Additionally one can run strings on the file to see the following output (truncated to only include interesting lines):

key format ok
passed check1
passed check2
passed check3

From this it's clear that three checks need to be passed after which it supposedly returns the success! line required to obtain the flag.


To lean more about the keychecker.devs file some reversing is required. After a bit of research on devicescript and more specifically the cli it can be seen that it supports disassembling a file using the disasm argument. Thus running the following command will disassemble the file (you might have to create a devsconfig.json file, this can be empty).

./node_modules/@devicescript/cli/devicescript disasm keychecker.devs --detailed

Running this command shows the following output (truncated for readability)

using devs: v2.13.9, runtime: v2.13.9, node: v20.3.0 from /home/panda/CTF/UIUCTF/pwnykey/node_modules/@devicescript/cli/built
// img size 12416
// 14 globals

proc main_F0(): @1120
  locals: loc0,loc1,loc2
   0:     CALL prototype_F1{F1}() // 270102
???oops: Op-decode: can't find jump target 10; 0c // 0df90007
   7:     RETURN undefined // 2e0c
   9:     JMP 39 // 0d1e
???oops: Op-decode: stack underflow; 4c // 4c
???oops: Op-decode: stack underflow; 250003 // 250003
???oops: Op-decode: can't find jump target 22; 0c // 0df90007
  19:     RETURN undefined // 2e0c
???oops: Op-decode: can't find jump target 51; 0c // 0d1e
  23:     CALL ???oops op126(62, ret_val()) // 7ece2c04
???oops: Op-decode: can't find jump target 34; 0c // 0df90007
  31:     RETURN undefined // 2e0c
???oops: Op-decode: can't find jump target 72; 0c // 0d27
???oops: Op-decode: stack underflow; 02 // 02
???oops: Op-decode: stack underflow; 253303 // 253303
???oops: Op-decode: can't find jump target 46; 0c // 0df90007
  43:     RETURN undefined // 2e0c
  45:     JMP 89 // 0d2c

The disassembly seems to generate a lot of jump and stack errors. Reading one of these errors: ???oops: Op-decode: can't find jump target 10; 0c // 0df90007 seems to also show the bytes of the opcode 0df90007. Presumably this is a jump but to be sure it is important to read through the source to confirm and figure out what parameters are provided. After looking through the disassembly sourcecode in github two important bits of code can be found.

  1. The parseBytecode function
  2. The opcode list

For now the opcode list specifically is very helpful. By using a small assumption that the first byte of the provided opcode bytes is the actual opcode one can try to find which opcode is referenced. The bytes show it's opcode 0x0d or 13. Looking at the source it shows this is the opcode for JMP %j, the jump instruction. Furthermore this shows the other bytes listed must then be the number of bytes to jump (f90007). It however seems unlikely it jumps 16318471 forward. Thus the code has to somehowe convert these bytes to a number. Looking at the parseBytecode function one can spot the line:

const op = decodeOp()

which calls:

function decodeOp() {
    const stack: OpTree[] = []
    for (;;) {
        const op = getbyte()
        if (op == 0 && pc - stmtStart == 1)
            return new OpTree(Op.STMT0_DEBUGGER)
        const e = new OpTree(op)
        if (opTakesNumber(op)) {
            jmpoff = pc - 1
            e.intArg = decodeInt()
        let n = opNumRealArgs(op)
        if (n) {
            if (stack.length < n) error("stack underflow")
            e.args = stack.slice(stack.length - n)
            while (n--) stack.pop()
        if (opIsStmt(op)) break
    if (stack.length != 1) error(`bad stack ${stack.length}`)
    return stack[0]

Reading through the code shows that for an opcode that takes a number argument it will run the function decodeInt():

function decodeInt() {
    const v = getbyte()
    if (v < BinFmt.FIRST_MULTIBYTE_INT) return v

    let r = 0
    const n = !!(v & 4)
    const len = (v & 3) + 1

    for (let i = 0; i < len; ++i) {
        const v = getbyte()
        r = r << 8
        r |= v

    return n ? -r : r

Here it can be seen how the number provided is converted to a number. Firstly it checks if the first byte is larger than BinFmt.FIRST_MULTIBYTE_INT which is equal to 0xf8. Since the first byte is 0xf9 it continues.

  • it calculates n by doing 0xf9 & 4 = 0
  • it calculates len by doing (0xf9 & 3) + 1 = 2

then it will read len bytes and create a number from them. Lastly it negates the value if n is 1. Thus the value of the argument f9007 is 7. It can then be concluded that we jump 7 bytes forward.

Looking back at disassembly after a jump one sees the following:

???oops: Op-decode: can't find jump target 22; 0c // 0df90007
  19:     RETURN undefined // 2e0c
???oops: Op-decode: can't find jump target 51; 0c // 0d1e

This signifies the bytestream 0df900072e0c0d1e Counting 7 bytes from the start shows we end up right in the middle of opcode 0d1e. This is why the disassembler cannot find the jump target as it is in the middle of an opcode instead of at the start. This is a common technique to confuse disassemblers as they greedily take bytes for each opcode even if the code never reaches those opcodes. From this point there are two solutions:

  1. Write a recursive disassembler which takes jumps into account.
  2. Try to patch the binary so the disassembler understands what is happening.

Obviously the second solution would be perefered if possible.

Fixing the disassembler

Very important to notice (this took a bit) is that the jumps are always 7 bytes and it always skips the same bytes. This suggests we can match replace those bytes to a single byte opcode like null bytes (debugger opcode) restoring the program.

A simple program which does this would look like:

program = open("keychecker.devs", "rb").read()
program = program.replace(b"\x0d\xf9\x00\x07\x2e\x0c\x0d", b"\x00"*7)
open("clean.devs", "wb").write(program)

running this code and disassembling clean.devs shows the following (debugger opcodes removed from disassembly):

using devs: v2.13.9, runtime: v2.13.9, node: v20.3.0 from /home/panda/CTF/UIUCTF/pwnykey/node_modules/@devicescript/cli/built�[0m
// img size 12416
// 14 globals

proc main_F0(): @1120
  locals: loc0,loc1,loc2
   0:     CALL prototype_F1{F1}() // 270102
  10:     CALL ds."format"{I76}("start!"{A0}) // 1e4c250003
  22:     CALL ds."print"{I126}(62, ret_val()) // 1e7ece2c04
  34:     CALL fetch_F2{F2}("http://localhost/check"{A51}) // 2702253303
  46:     CALL ret_val()."text"{A52}() // 2c1b3402
  57:     CALL ret_val()."trim"{A48}() // 2c1b3002
  68:     {G4} := ret_val() // 2c1204

This results in very readable disassembly making the challenge significantly easier.

Valid format

Like mentioned before there are three checks the key needs to pass. Looking through the disassembly the following code can be reversed:

G4 = fetch("http://localhost/check").text().trim()
if G4.length() !== 29 {
    new Error("Invalid key")
G5 = G4.split("-")
if G5.length() !== 5 {
    new Error("Invalid key")
if (!G5.some(x => F7(x))) {
    new Error("Invalid key")
if (!G5.some(x => F8(x))) {
    new Error("Invalid key")
print("key format ok")

This code shows the key needs to have a length of 29 and when split by the '-' character have a length of 5. Furthermore two functions F7 and F8 are called. Reversed code of these looks like the following:


function F7(par1) {
    return par1.length() == 5


function F8(par1) {
    return par1.split("").some(x => "0123456789ABCDFGHJKLMNPQRSTUWXYZ".includes(x))

From these function it can be concludes that the key also needs to have 5 groups of characters which can be found in the alphabet 0123456789ABCDFGHJKLMNPQRSTUWXYZ.

Check 1

The reversed code continues as following:

loc0 = => { => {
G6 = loc0[0]
G7 = loc0[1]
G8 = loc0[2]
G9 = loc0[3]
G10 = loc0[4]
loc0 = format("{0}", G6)
loc1 = format("{0}", [30, 10, 21, 29 10])
if loc0 !== loc1 {
    new Error("Invalid key")
print("passed check1")

The code shows it maps the characters to indexes of the alphabet. To pass the first check then, the first group of the key should equal a static array f [30, 10, 21, 29 10]. These numbers correspond to the text YANXA

Check 2

The code continues as follows:

G11 = concat(G7, G8)
loc0 = G11.reduce((x, y) => x + y, 0)
if (loc0 !== 134) {
    new Error("Invalid key")
loc0 = G11.reduct((x, y) => x * y, 1)
if (loc0 !== 12534912000) {
    new Error("Invalid key")
print("passed check2")

From this code it can be deduced that the second and the third block (G7, G8) summed up should equal 134 and the product should equal 12534912000. A simple pythons script can easily find valid characters in less than a minute:

import random

alphabet = "0123456789ABCDFGHJKLMNPQRSTUWXYZ"
def sum(s):
    r = 0
    for c in s:
        r += alphabet.index(c)
    return r

def mul(s):
    r = 1
    for c in s:
        r *= alphabet.index(c)
    return r

while True:
    choice = random.choices(alphabet, k=10)
    if sum(choice) == 134 and mul(choice) == 12534912000:

One valid range of characters is: GM869-1ZHDG

Check 3

The third and final check goes as follows:

G12 = G9
G13 = 1337
loc2 = 0
while (loc2 < 420) {
    loc2 += 1
loc0[0] = nextInt_F13()
loc0[1] = nextInt_F13()
loc0[2] = nextInt_F13()
loc1 = [2897974129, -549922559, -387684011]
if (loc0 !== loc1) {
    new Error("Invalid key")
print("passed check3")
print("success!") // Flag here

Important in this code is the nextInt_F13() function. The disassembly of this function looks as follows:

   0:     CALL {G12}."pop"{I49}() // 160c1a3102
  12:     loc0{L0} := ret_val() // 2c1100
  22:     loc0{L0} := (loc0{L0} ^ ((loc0{L0} >> 2) & 4294967295{D1})) // 15001500924229013e401100
  41:     loc0{L0} := (loc0{L0} ^ ((loc0{L0} << 1) & 4294967295{D1})) // 15001500914129013e401100
  60:     loc0{L0} := (loc0{L0} ^ (({G12}[0] ^ ({G12}[0] << 4)) & 4294967295{D1})) // 1500160c9018160c901894414029013e401100
  86:     {G13} := (({G13} + 13371337) & 4294967295{D1}) // 160028facc07c93a29013e1200
 106:     CALL {G12}."unshift"{I71}(loc0{L0}) // 160c1a47150003
 120:     RETURN (loc0{L0} + {G13}) // 1500160d3a0c

With some experience and a lot of googling (while trying to reverse the routine, in vain) would result in finding that this is an implementation of the xorwow PRNG. This is a PRNG combining LFSR with a running counter. However the disassembled code does show it using 13371337 as increment value for the counter in stead of the standard 362437.

Luckily it is possible to brute force this. While python may be too slow to run the PRNG $30^{5} \times 423$ times, C should be able to. A brute force program would look like this:

#include <stdio.h>
#include <stdint.h>
#include <stdlib.h>
#include <unistd.h>

struct xorwow_state {
    uint32_t x[5];
    uint32_t counter;

/* The state array must be initialized to not be all zero in the first four words */
int32_t xorwow(struct xorwow_state *state)
    /* Algorithm "xorwow" from p. 5 of Marsaglia, "Xorshift RNGs" */
    int32_t t  = state->x[4];
    int32_t s  = state->x[0];  /* Perform a contrived 32-bit shift. */
    state->x[4] = state->x[3];
    state->x[3] = state->x[2];
    state->x[2] = state->x[1];
    state->x[1] = s;
    t = (t ^ (t >> 2)) & 4294967295;
    t = (t ^ (t << 1)) & 4294967295;
    t = (t ^ (s ^ (s << 4))) & 4294967295;
    state->x[0] = t;
    state->counter += (int32_t)13371337 & 4294967295;
    return (t + state->counter) & 4294967295;

int main()
    for (uint x1 = 0; x1 < 32; x1++)
        for (uint x2 = 0; x2 < 32; x2++)
            for (uint x3 = 0; x3 < 32; x3++)
                for (uint x4 = 0; x4 < 32; x4++)
                    for (uint x5 = 0; x5 < 32; x5++)
                        struct xorwow_state* state = malloc(sizeof(struct xorwow_state));
                        state->x[0] = x1;
                        state->x[1] = x2;
                        state->x[2] = x3;
                        state->x[3] = x4;
                        state->x[4] = x5;
                        state->counter = 1337;
                        for (int n = 0; n < 420; n++)
                            int res = xorwow(state);
                        int32_t a = xorwow(state);
                        int32_t b = xorwow(state);
                        int32_t c = xorwow(state);
                        if (a == 2897974129 || a == -1396993167)
                            printf("%d %d %d %d %d ", x1, x2, x3, x4, x5);
                            return 0;
    return 1;

An important addition to the program is the check for both 2897974129 and -1396993167 as C might handle left shifts and signed/unsigned different from devicescript (This took a while to figure out). This program takes about 48 seconds to find the solution 14 11 22 2 27 or FBP2U


In the end the generated valid key is YANXA-GM869-1ZHDG-FBP2U-00000 (note. the last group has no impact). Submitting this to the website will display the flag.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment