Initial commit

Makefile

@@ -0,0 +1,35 @@
+.PHONY: build clean runner runner-safari trace-matching push pull deploy
+SHELL=/usr/bin/env bash
+
+REGISTRY=ghcr.io/secpriv
+
+all: build
+
+runner: instrumentation/extension instrumentation/proxy runner/
+	docker-compose -f runner/docker-compose.yaml build
+	docker tag wpt-runner:latest $(REGISTRY)/wpt-runner:latest
+
+runner-safari: runner/safari
+	cd runner/safari; docker build -t $(REGISTRY)/wpt-safari-runner:latest .
+
+trace-matching: trace_matching/
+	docker run --rm -i -v `pwd`/trace_matching:/mnt:ro --workdir /tmp nixos/nix sh -c "nix-build /mnt/default.nix -A docker 1>&2 && cat result" | docker load
+	docker tag wpt-trace-matching:latest $(REGISTRY)/wpt-trace-matching:latest
+
+build: runner runner-safari trace-matching
+push:
+	docker push $(REGISTRY)/wpt-runner:latest
+	docker push $(REGISTRY)/wpt-safari-runner:latest
+	docker push $(REGISTRY)/wpt-trace-matching:latest
+pull:
+	docker pull $(REGISTRY)/wpt-runner:latest
+	docker pull $(REGISTRY)/wpt-safari-runner:latest
+	docker pull $(REGISTRY)/wpt-trace-matching:latest
+
+deploy: kubernetes/pipeline.yaml kubernetes/safari_runner.yaml
+	kubectl apply -f kubernetes/pipeline.yaml kubernetes/safari_runner.yaml
+
+
+clean:
+	docker rmi wpt-runner:latest wpt-trace-matching:latest
+	docker rmi $(REGISTRY)/wpt-runner:latest $(REGISTRY)/wpt-safari-runner:latest $(REGISTRY)/wpt-trace-matching:latest

README.md

@@ -0,0 +1,76 @@
+# WPT Security
+
+Web Platform Threats: Automated Detection of Web Security Issues With WPT.
+
+## Repo Structure
+
+```
+├── docs
+│   └── report.pdf          Extended version of the USENIX'24 paper
+├── instrumentation/        Browser Instrumentation used by the runner
+│   ├── extension/          Extension for tracing browser actions
+│   │   ├── chromium/       Chromium extension
+│   │   ├── firefox/        Firefox extension
+│   │   └── safari/         Safari extension
+│   └── proxy/              Proxy for logging requests/responses
+├── kubernetes/             Kubernetes definitions to deploy the pipeline in a cluster
+├── results/                Results of running the pipeline (USENIX'24 Paper)
+│   ├── wpt/                Verification results of the WPT suite (Sec. 5.1)
+│   └── beyond_wpt/         Verification results of the separate test suite of Sec. 5.3
+├── runner/                 Docker container for running a browser and producing a trace
+│   └── safari/             Safari-specific Docker container
+├── trace_matching/         Trace parser and SMT-LIB generator
+│   ├── trace_matching.smt  Definition of datatypes and invariants in SMT-LIB format
+│   ...
+├── Makefile                Makefile for automating common tasks
+├── README.md               This file
+└── wpt-check               Local pipeline executable
+```
+
+## Usage
+
+WPT Security requires a working [docker](https://docker.io) installation, the bash shell and GNU make.
+
+### Download or build the pipeline docker images
+
+```sh
+./wpt-check pull    # or make pull
+```
+
+The command downloads three images from the github docker registry
+- `wpt-runner` Browser runner for Chromium and Firefox
+- `wpt-safari-runner` Browser runner for Safari (Note: this image does not include MacOS, which needs to be run separately)
+- `wpt-trace-matching` Trace verifier, including trace parsing and Z3
+
+Alternatively, the images can be built locally with the following command.
+
+```sh
+./wpt-check build   # or make
+```
+
+Note that the build **may take up to 30 minutes**, as a specific version of z3 is compiled from source.
+
+### Verify all Web Invariants on the execution of WPT tests
+
+```sh
+./wpt-check run firefox '/cookies/secure/set-from-dom.https.sub.html'
+```
+
+The script runs the instrumented `firefox` browser, converts the execution trace to SMT-LIB, and verifies it with the Z3 theorem prover.
+The verification results are printed on standard output for every subtest and invariant:
+- `unsat`: the invariant is valid;
+- `sat`: the invariant does not hold, i.e., Z3 could find a counterexample.
+
+
+The `wpt-check` script supports running Firefox and Chromium. 
+For Safari, refer to the [runner/safari/README.md](runner/safari/README.md) file for a guide on (i) how to install the Safari instrumentation on a MacOS system, and (ii) generate an execution trace in JSON format.
+The JSON trace can be verified using the `wpt-check verify` command, as described in the following.
+
+### Verify all Web Invariants on an execution trace in JSON format
+
+```sh
+./wpt-check verify safari_1710427255.json
+```
+
+The sript converts the trace to SMT-LIB and verifies it using Z3.
+The output is printed in the same format as the `wpt-check run` command.

instrumentation/README.md

@@ -0,0 +1,13 @@
+# Browser Instrumentation
+
+Our browser instrumentation combines a browser extension with a network proxy in order to sidstep the limitations of the extension API with respect to their ability to inspect network traffic.
+
+## Extension
+
+The `extension` folder includes the source code of the browser extension for each of the three major browsers: Chromium, Firefox and Safari.
+As the three browsers implement the Web extension API with some minor differences, the code requires minor browser-specific modifications.
+
+## Proxy
+
+The network proxy is implemented as a plugin for the [mitmproxy](https://mitmproxy.org) Python proxy.
+It logs the requests and responses it intercepts in a JSON file that can be downloaded by sending a GET request to the `http://b1v253vpqwutupjwntfmpc9a4m94s5zm.mitm.it/download-trace` non-existent URL, so that the extension can fetch it and merge it with the logged execution trace.

instrumentation/extension/.gitignore

@@ -0,0 +1,2 @@
+webextensions-examples
+webextensions-examples/*