diff options
| author |   Jason A. Donenfeld <Jason@zx2c4.com> | 2017-03-28 18:09:09 +0200 |
|---|---|---|
| committer | Jason A. Donenfeld <Jason@zx2c4.com> | 2017-03-28 18:10:18 +0200 |
| commit | 754c4f1a15f821c9c11ae6ad71f6eecfad8b5d28 (patch) | |
| tree | f29011c7d5cf0925498618aa808099f0b8bd0422 | |
| parent | PSK Mode added, and efficiency improved by splitting out state invariants (diff) | |
| download | wireguard-tamarin-754c4f1a15f821c9c11ae6ad71f6eecfad8b5d28.tar.xz wireguard-tamarin-754c4f1a15f821c9c11ae6ad71f6eecfad8b5d28.zip | |
Makefile: be less insane
This is still insane, but now slightly less so.
| -rw-r--r-- | Makefile | 38 |
1 files changed, 20 insertions, 18 deletions
@@ -8,6 +8,8 @@ TAMARIN_BIN ?= tamarin-prover TAMARIN_ARGS ?= "--heuristic=i" # The remote path to tamarin and directory that the .spthy gets copied to TAMARIN_REMOTEBIN ?= tamarin-prover +# The target protocol to be proved +TAMARIN_PROTO ?= wireguard logfile = log @@ -15,32 +17,32 @@ default: local .PHONY: check-ports check-file remote local -proto-file: - m4 wireguard.m4 > proto.spthy +%.spthy: %.m4 + m4 $< > $@ -# Find the smallest unused port > 3000 on ${host}; thanks http://unix.stackexchange.com/a/55940 +# Find the smallest unused port > 3000 on $(host); thanks http://unix.stackexchange.com/a/55940 # There's a race condition (if someone binds that port in the middle of the make) but it's hardly important # Choose a local port for Tamarin (FYI you need -n in lsof or it takes 20s for DNS resolution... yuck) check-ports: ifndef TAMARIN_HOST $(error Running remotely requires a TAMARIN_HOST to be defined in your environment) endif - $(eval remoteport := $(shell ssh -t ${TAMARIN_HOST} \ - "ss -tln | awk 'NR > 1{gsub(/.*:/,"\"\"",\$$4); print \$$4}' | sort -un |\ - awk -v n=3001 '\$$0 < n {next}; \$$0 == n {n++; next}; {exit}; END {print n}'")) + $(eval remoteport := $(shell ssh -t $(TAMARIN_HOST) \ + "ss -tln | awk 'NR > 1(gsub(/.*:/,"\"\"",\$$4); print \$$4)' | sort -un |\ + awk -v n=3001 '\$$0 < n (next); \$$0 == n (n++; next); (exit); END (print n)'")) $(eval localport := $(shell lsof -n -i -P | grep -i "listen" |\ grep -o "[0-9]* (LISTEN)" | cut -d' ' -f1 | sort -un | awk -v n=3001\ - '$$0 < n {next}; $$0 == n {n++; next}; {exit}; END {print n}')) + '$$0 < n (next); $$0 == n (n++; next); (exit); END (print n)')) remote: check-ports proto-file - $(eval remotedir := $(shell ssh ${TAMARIN_HOST} "mktemp -d")) - scp proto.spthy ${TAMARIN_HOST}:${remotedir} > /dev/null - @echo ========= local port ${localport}, remote port ${remoteport} ========= - (tail -f ${logfile} | grep -m1 "Application launched" | xargs echo "" >> ${logfile};\ - ${TAMARIN_BROWSER} http://localhost:${localport}/thy/trace/1/overview/help) & - ssh -L ${localport}:localhost:${remoteport} -S'none' -t ${TAMARIN_HOST} \ - "${TAMARIN_REMOTEBIN} interactive ${remotedir}/ --interface='*4' --port=${remoteport} ${TAMARIN_ARGS}" 2>&1 | tee ${logfile} - -local: proto-file - (sleep 1 && ${TAMARIN_BROWSER} http://localhost:3001/thy/trace/1/overview/help) & - ${TAMARIN_BIN} interactive . --interface='*4' --port=3001 ${TAMARIN_ARGS} + $(eval remotedir := $(shell ssh $(TAMARIN_HOST) "mktemp -d")) + scp proto.spthy $(TAMARIN_HOST):$(remotedir) > /dev/null + @echo ========= local port $(localport), remote port $(remoteport) ========= + (tail -f $(logfile) | grep -m1 "Application launched" | xargs echo "" >> $(logfile);\ + $(TAMARIN_BROWSER) http://localhost:$(localport)/thy/trace/1/overview/help) & + ssh -L $(localport):localhost:$(remoteport) -S'none' -t $(TAMARIN_HOST) \ + "$(TAMARIN_REMOTEBIN) interactive $(remotedir)/ --interface='*4' --port=$(remoteport) $(TAMARIN_ARGS)" 2>&1 | tee $(logfile) + +local: $(TAMARIN_PROTO).spthy + (sleep 1 && $(TAMARIN_BROWSER) http://localhost:3001/thy/trace/1/overview/help) & + $(TAMARIN_BIN) interactive . --interface='*4' --port=3001 $(TAMARIN_ARGS) |