gaslightCTF — rev: Compiled Source Sheets

Challenge: Compiled Source Sheets Category: rev Author: sportshead Flag: gaslightCTF{ch3ck_0ut_lyra-horse!!_2QY90H6F}

Description

My new VM is Spectre-proof! It's also guaranteed race-condition free, and runs on every major OS[1]. Try it out! [1] that supports Chrom(e|ium)

The attachment is a single HTML file, vm.html (~780 KB). The footnote gives it away: this is x86CSS by Lyra Rebane (lyra.horse) — a working x86/8086 CPU implemented entirely in CSS, executing machine code through @property custom properties, container queries and CSS animations. There is no JavaScript at all. Our job is to recover the flag that this CSS "VM" computes.

1. What's in the handout

handout/
├── vm.html
└── static/
    ├── Lekton.woff2
    └── Lekton-bold.woff2

vm.html is the full x86CSS website. The page contains an embedded 8086 program whose machine code has been compiled into CSS declarations. The program runs automatically thanks to the execute @keyframes animation and writes its output to a "screen" element — no user interaction needed.

2. Extracting the program bytes

x86CSS stores one memory byte per CSS custom property. The build_css.py script from the x86CSS repo shows the exact layout:

• memory byte m<i> holds the value of address i,
• the program is loaded at address 0x100 (= 256),
• the initial contents of the program region are baked in as read-only declarations of the form:

--__1m<i>: <byte>;

i.e. memory addresses 0x100..0x100+n are hard-coded. The writable RAM elsewhere falls back to 0x90 (NOP), and the low byte m0 to 0xCC (INT3).

Let's find every read-only program byte in the HTML:

$ grep -oE -- '--__1m([0-9]+): ([0-9]+);' vm.html \
    | sed -E 's/--__1m([0-9]+): ([0-9]+);/\1 \2/' \
    | awk '$1 >= 256' | sort -n
256 86
257 87
258 85
259 137
...

There are 578 such bytes starting at address 0x100. Convert them to a raw binary:

import re
pairs = re.findall(rclass="hljs-string">'--__1m(\d+): (\d+);', open(class="hljs-string">'vm.html').read())
pairs = [(int(a), int(b)) for a, b in pairs if int(a) >= 256]
pairs.sort()
open(class="hljs-string">'prog.bin', class="hljs-string">'wb').write(bytes(v for _, v in pairs))

The starting IP is also embedded: the @property --IP { initial-value: 256 } (line 523) tells us execution begins at 0x100.

3. Disassembly

Use ndisasm to get an 8086 disassembly:

$ ndisasm -b 16 -o 0x100 prog.bin

The program is short. Key excerpts:

00000100  56                push si
00000101  57                push di
00000102  55                push bp
00000103  89E5              mov bp,sp
00000105  83EC0E            sub sp,0xe
00000108  B8EA02            mov ax,0x2ea
0000010B  50                push ax
0000010C  FF163C03          call word near [0x33c]
...
00000123  31FF              xor di,di
00000125  8B1E3803          mov bx,[0x338]
00000129  C7070200          mov word [bx],0x2
0000012D  FF163A03          call word near [0x33a]   ; readInput
00000131  84C0              test al,al
00000133  7424              jz 0x159
...
0000013D  3C0A              cmp al,0xa
0000013F  741D              jz 0x15e                 ; Enter pressed -> stop reading
00000141  89FA              mov dx,di
00000143  42                inc dx
00000144  8956F2            mov [bp-0xe],dx
00000147  89EE              mov si,bp
00000149  89FB              mov bx,di
0000014B  8840F6            mov [bx+si-0xa],al       ; store input char
...
00000168  83FF08            cmp di,0x8
0000016B  8B363C03          mov si,[0x33c]
0000016F  7E03              jle 0x174
00000171  E95D01            jmp 0x2d1                ; too long -> fail

External I/O (the "hardware")

The code calls indirect addresses whose values live in the data table:

0x338: 0x2100  SHOW_KEYBOARD
0x33a: 0x2006  readInput   -> reads one char into AL
0x33c: 0x2004  writeChar8  -> writes 8 chars from a pointer on the stack
0x33e: 0x2002  writeChar4  -> writes 4 chars
0x340: 0x2000  writeChar1  -> writes 1 char

So the program:

1. Prints guess the password: via three string writes,
2. Reads a password (up to ~9 chars; newline terminates),
3. Requires the length to be ≤ 8 (cmp di,0x8 ; jle 0x174),
4. Runs a long chain of bitwise checks over the 8 input bytes,
5. If all checks pass, prints congrats + the flag pieces + the password + }, otherwise prints nope :( and returns.

4. The flag assembly

When the checks pass (at 0x26e), the program prints, in order:

address	I/O call	bytes printed
0x301	writeChar8	congrats
0x2e0	writeChar4	!\n
0x30a	writeChar8	gaslight
0x313	writeChar8	CTF{ch3c
0x31c	writeChar8	k_0ut_ly
0x325	writeChar8	ra-horse
0x2e5	writeChar4	!!_
[bp-0xa]	writeChar8	the 8-char password
0x7d	writeChar1	}

So the flag is:

gaslightCTF{ch3ck_0ut_lyra-horse!!_<password>}

The only unknown is the 8-character password.

5. Reversing the checks

The input characters are stored at [bp-0xa]..[bp-0x3]:

c0 = [bp-0xa]   (in[0])
c1 = [bp-0x9]   (in[1])
c2 = [bp-0x8]   (in[2])
c3 = [bp-0x7]   (in[3])
c4 = [bp-0x6]   (in[4])
c5 = [bp-0x5]   (in[5])
c6 = [bp-0x4]   (in[6])
c7 = [bp-0x3]   (in[7])

The validation routine (0x17d .. 0x26c) is a sequence of mov/xor/and/or/cmp/test pairs. Translating each to a constraint gives 21 boolean equations over the bytes:

1.  c6 ^ c2 = 0x6f
2.  c3 & c7 = 0x00
3.  c3 | c7 = 0x7f
4.  c6 | c3 = 0x3f
5.  c1 & c5 = 0x40
6.  c2 ^ c5 = 0x11
7.  c2 ^ c1 = 0x08
8.  c1 & c4 = 0x10
9.  c2 & c1 = 0x51
10. c6 ^ c0 = 0x04
11. c7 | c4 = 0x76
12. c2 | c7 = 0x5f
13. c3 | c4 = 0x39
14. c5 ^ c3 = 0x71
15. c1 & c6 = 0x10
16. c7 ^ c4 = 0x76
17. c3 & c0 = 0x30
18. c2 ^ c4 = 0x69
19. c2 | c4 = 0x79
20. c4 ^ c0 = 0x02
21. c6 ^ c3 = 0x0f

6. Solving with z3

The constraints are overdetermined (21 equations for 8 unknowns), so a solver is trivial:

from z3 import *
cs = [BitVec(fclass="hljs-string">'c{i}', 8) for i in range(8)]
c0, c1, c2, c3, c4, c5, c6, c7 = cs
s = Solver()
for c in cs:
    s.add(c >= 0x21, c <= 0x7e)          # printable password

s.add(c6 ^ c2 == 0x6f)
s.add(c3 & c7 == 0x00)
s.add(c3 | c7 == 0x7f)
s.add(c6 | c3 == 0x3f)
s.add(c1 & c5 == 0x40)
s.add(c2 ^ c5 == 0x11)
s.add(c2 ^ c1 == 0x08)
s.add(c1 & c4 == 0x10)
s.add(c2 & c1 == 0x51)
s.add(c6 ^ c0 == 0x04)
s.add(c7 | c4 == 0x76)
s.add(c2 | c7 == 0x5f)
s.add(c3 | c4 == 0x39)
s.add(c5 ^ c3 == 0x71)
s.add(c1 & c6 == 0x10)
s.add(c7 ^ c4 == 0x76)
s.add(c3 & c0 == 0x30)
s.add(c2 ^ c4 == 0x69)
s.add(c2 | c4 == 0x79)
s.add(c4 ^ c0 == 0x02)
s.add(c6 ^ c3 == 0x0f)

assert s.check() == sat
while s.check() == sat:
    m = s.model()
    print(bytes(m[c].as_long() for c in cs))
    s.add(Or(c != m[c] for c in cs))     # look for other solutions

Output:

b'2QY90H6F'

and the model is unique (the loop terminates after one iteration).

7. The flag

Plugging the password into the assembled output:

gaslightCTF{ch3ck_0ut_lyra-horse!!_2QY90H6F}

Extra: verifying against the real VM

For completeness, the extracted prog.bin can be run under a real 8086 emulator (with the four memory-mapped I/O "ports" at 0x2000/0x2002/0x2004/0x2006 stubbed as stdout/stdin). Feeding it the password 2QY90H6F produces:

guess the password: 2QY90H6F
congrats!
gaslightCTF{ch3ck_0ut_lyra-horse!!_2QY90H6F}

TL;DR

1. The VM is x86CSS — an 8086 emulator written purely in CSS.
2. The program's machine code is embedded as --__1m<addr>: <byte>; declarations starting at address 0x100.
3. Extract those 578 bytes, disassemble with ndisasm -b16 -o0x100.
4. The code reads an 8-character password and enforces 21 bitwise constraints on the bytes.
5. Feed the constraints to z3 → password 2QY90H6F.
6. The success path concatenates gaslightCTF{ch3ck_0ut_lyra-horse!!_ + password + }.