MIT 6.858 — Computer Systems Security (labs)

Working solutions to the five 6.858 labs on the zoobar web application — buffer-overflow exploitation, privilege separation, a symbolic-execution bug-finder, browser-security attacks, and the SecFS secure file system — an independent, from-skeleton implementation of 6.858 — Computer Systems Security (MIT, 2022), part of a csdiy.wiki full-catalog build.

Educational scope (please read)

This repository is educational security coursework: authorized self-study of a public university course. Every exploit and attack here runs only against the course's own intentionally-vulnerable targets — the provided zookd web server, the local zoobar app, and a local SecFS server — inside a private WSL2 sandbox. There is nothing here that targets real third-party systems, and nothing about malware, C2/botnets, DoS, or detection evasion. The point is to learn how these classes of bug work and how to defend against them.

Overview

6.858 teaches systems security by having you play both attacker and defender on a small but realistic web app. This repo implements each lab from the official skeleton and verifies it by actually running it: real exploits hijack the real vulnerable binary, the concolic engine finds the real planted bugs, the SecFS integrity checks reject a real forged server state, and so on. Memory-safety work is done in an x86-64 WSL2 sandbox with ASLR disabled per-run exactly as the course specifies.

Results (measured on WSL2 Ubuntu 24.04, x86-64, CPU-only)

Lab	What it does	Result (measured)
1 · Buffer overflows	3 exploits + a fix on the vulnerable zookd	exploit-2 crash → SIGSEGV; exploit-4 exec-stack shellcode → grades.txt unlinked; exploit-5 ret2libc system("rm …") → grades.txt unlinked — all PASS via the course's check-crash/check-attack; bounds-checked url_decode defeats all three while normal requests still 200
3 · Symbolic execution	Concolic executor + Z3 bug-finder	8/10 exercises PASS: int-avg (both unsat), concolic ×/÷, concolic_find_input/force_branch/execs, string len/in, SQLAlchemy .get() — all "Found all cases". Ex9-10 (zoobar-under-concolic) = documented partial
5 · SecFS	SUNDR-style secure FS over an untrusted server	Real FUSE mount: create files/dirs, read back; a fresh client rebuilds the FS from the server's RSA-signed VSL; a forged signature in the VSL is detected and the mount is refused. Ex2/Ex3 (groups, encryption) = documented partial
2 · Privilege separation	auth + bank RPC services	PASS (core): PBKDF2 + per-user salt credential storage (no plaintext in DB), random tokens, bank authenticates every transfer via the auth service and refuses a forged token. Container/firewall isolation = documented partial
4 · Browser security	XSS / phishing / worm on zoobar	Reflected XSS confirmed to render unescaped against the real users.html (because users.py uses Markup()); payloads written for cookie theft, exfiltration, phishing, and a self-propagating profile worm. PhantomJS browser-grading = documented partial

Full captured output is under results/ (lab1-results.txt … lab5-results.txt).

Implemented labs

• Lab 1 — Buffer overflows — exploit-2/4/5.py (crash, exec-stack shellcode, return-to-libc) against zookd, plus a bounds-checked url_decode fix; all verified with the course's own check scripts.
• Lab 3 — Symbolic execution — full concolic engine in symex/fuzzy.py (AST nodes, concolic int/str/bytes, find_input, force_branch, execs), symsql.py, and the int-avg bit-trick; 8/10 exercises green.
• Lab 5 — SecFS — fs._create, the SUNDR VSL (tables.py, RSA-signed version structures, fork/rollback detection) and crypto.sign/ verify; verified end-to-end on a real FUSE mount incl. tamper detection.
• Lab 2 — Privilege separation (core) — PBKDF2 auth.py, the auth and bank RPC services, and cross-service token authentication.
• Lab 4 — Browser security — answer-1/2/3.js/txt (XSS), answer-9.html (phishing), answer-14.txt (worm); vulnerability confirmed by rendering.

Deviations are called out honestly in each lab's results/*.txt and in Verification below.

Project structure

mit-6858/
├── lab1-buffer-overflow/      # zookd.c, http.c, exploit-2/4/5.py, fix/, answers.txt
├── lab2-privilege-separation/ # zoobar/{auth,auth-server,auth_client,bank-server}.py …
├── lab3-symbolic-execution/   # symex/{fuzzy,symsql,symeval}.py, int-avg.py, check-*.py
├── lab4-browser-security/     # answer-1.js, answer-2.js, answer-3.txt, answer-9.html, answer-14.txt
├── lab5-secfs/                # secfs/{fs,tables,crypto}.py, bin/secfs-{server,fuse}
├── results/                   # measured output for every lab
├── LICENSE                    # MIT (our own code only)
└── README.md

How to run

Everything runs in WSL2 Ubuntu (Linux-only labs). A Python venv provides Z3, Flask, SQLAlchemy 1.4, cryptography, Pyro4 and llfuse.

# --- Lab 1: buffer overflows (x86-64, ASLR off per-run via clean-env.sh) ---
cd lab1-buffer-overflow && make
./check-crash.sh  zookd-exstack ./exploit-2.py     # -> PASS (SIGSEGV)
./check-attack.sh zookd-exstack ./exploit-4.py     # -> PASS (grades.txt gone)
./check-attack.sh zookd-nxstack ./exploit-5.py     # -> PASS (ret2libc)

# --- Lab 3: symbolic execution (Z3) ---
cd lab3-symbolic-execution
python3 int-avg.py                                 # both averages -> unsat
python3 check-symex-int.py ; python3 check-symex-str.py ; python3 check-symex-sql.py

# --- Lab 5: SecFS (real FUSE mount) ---
cd lab5-secfs && pip install -e .
secfs-server server.sock &                          # Pyro server
sudo secfs-fuse PYRO:secfs@./u:server.sock mnt/ root.pub user-0-key.pem

# --- Lab 2: privilege separation (auth + bank RPC services) ---
cd lab2-privilege-separation/zoobar
ZOOBAR_AUTH_SVC=127.0.0.1:8027 python3 auth-server.py 8027 &
ZOOBAR_AUTH_SVC=127.0.0.1:8027 python3 bank-server.py 8028 &

Verification

• Lab 1 — the course's own check-crash.sh / check-attack.sh report PASS for all three exploits against the vulnerable build, and report the attacks defeated against the patched build (fix/), with a normal request still returning HTTP 200. Addresses were taken with gdb from a server started under the real clean-env.sh (ASLR off, ulimit -s unlimited) so they match grading exactly. Toolchain note: Ubuntu 24.04 gcc defaults to PIE, so the Makefile adds -no-pie to reproduce the 2022 fixed-address, non-PIE layout.
• Lab 3 — Exercises 1–8 all print their success markers (see results/lab3-results.txt). Z3 4.16's string solver needed a longer timeout than the 2022 default to synthesize len(s) > 30, so fuzzy.z3_timeout was raised. Documented partial: Ex 9–10 drive the whole zoobar app through the concolic engine, whose bytecode rewriter (symex/rewriter.py, importwrapper.py) targets pre-3.9 CPython opcodes; it cannot run on the only interpreter available here (3.12), and Python 3.8 was unobtainable in this sandbox. The detection code and the fixed zoobar-fixed/ are implemented.
• Lab 5 — verified on a real FUSE mount + Pyro server: creation, multi-client reconstruction from the signed VSL, and rejection of a byte-flipped signature (results/lab5-results.txt). Documented partial: Ex 2 (group multi-user) and Ex 3 (read-permission encryption) extend the verified integrity core.
• Lab 2 — a headless harness starts the auth + bank services and shows PBKDF2 storage, token issuance, and a forged token being refused (results/lab2-results.txt). Documented partial: the lxc container / iptables firewall isolation needs the course VM's root networking.
• Lab 4 — the reflected XSS is shown rendering unescaped against the real users.html (and escaped when Markup() is removed), confirming the payloads fire (results/lab4-results.txt). Documented partial: the PhantomJS autograder relies on a now-abandoned browser binary.

Tech stack

C (x86-64, gcc), Python 3.12; Z3 4.16 (SMT), Flask + Jinja2/MarkupSafe, SQLAlchemy 1.4, cryptography (RSA-2048, PBKDF2, Fernet), Pyro4, llfuse/FUSE; gdb, objdump, strace; WSL2 Ubuntu 24.04.

Key ideas / what I learned

• Stack smashing end-to-end: from an unbounded url_decode copy to overwriting a saved return address, NOP-sled shellcode on an executable stack, and a ROP pop rdi; ret → system chain (with a ret for movaps alignment) on a non-executable stack — and the one-line bounds check that stops all of them.
• Concolic execution: mirroring every concrete operation with a symbolic Z3 expression, flipping path conditions, and asking the solver for the next input — enough to enumerate every branch of a function automatically.
• SUNDR / fork consistency: how signed version structures + version vectors let mutually-distrusting clients share an untrusted server and detect a server that forks, rolls back, or forges history.
• Least privilege: splitting a monolith so a front-end compromise can't read passwords or mint tokens; salting + PBKDF2 so a stolen DB is near-useless.
• The web trust model: how one Markup() (disabled escaping) turns a text field into cross-site scripting, phishing, and a self-replicating worm.

Credits & license

Based on the labs of 6.858 Computer Systems Security by MIT PDOS / CSAIL (2022, http://css.csail.mit.edu/6.858/2022/). SecFS is based on the SUNDR paper and the mit-pdos/secfs-skeleton. This repository is an independent educational reimplementation; all course materials, starter code, and specifications belong to their original authors. Original code in this repo is released under the MIT License.