Proofs of correctness of the TLS Handshake and corking state machine

.travis.yml

@@ -32,44 +32,47 @@ env:
   - S2N_LIBCRYPTO=openssl-1.1.0 OPENSSL_ia32cap="~0x200000200000000" BUILD_S2N=true TESTS=integration GCC6_REQUIRED=true
   - S2N_LIBCRYPTO=openssl-1.1.x-master BUILD_S2N=true TESTS=integration GCC6_REQUIRED=true
   - S2N_LIBCRYPTO=openssl-1.1.0 LATEST_CLANG=true TESTS=fuzz
-  - TESTS=sawHMAC SAW_HMAC_TEST=md5    SAW=true GCC6_REQUIRED=false
-  - TESTS=sawHMAC SAW_HMAC_TEST=sha1   SAW=true GCC6_REQUIRED=false
-  - TESTS=sawHMAC SAW_HMAC_TEST=sha224 SAW=true GCC6_REQUIRED=false
-  - TESTS=sawHMAC SAW_HMAC_TEST=sha256 SAW=true GCC6_REQUIRED=false
-  - TESTS=sawHMAC SAW_HMAC_TEST=sha384 SAW=true GCC6_REQUIRED=false
-  - TESTS=sawHMAC SAW_HMAC_TEST=sha512 SAW=true GCC6_REQUIRED=false
-  - TESTS=sawDRBG                      SAW=true
-  - TESTS=sawHMACFailure               SAW=true
+
 
 matrix:
   exclude:
   - os: osx
     env: TESTS=ctverif
-  - os: osx
-    env: TESTS=sawHMAC SAW_HMAC_TEST=md5    SAW=true GCC6_REQUIRED=false
-  - os: osx
-    env: TESTS=sawHMAC SAW_HMAC_TEST=sha1   SAW=true GCC6_REQUIRED=false
-  - os: osx
-    env: TESTS=sawHMAC SAW_HMAC_TEST=sha224 SAW=true GCC6_REQUIRED=false
-  - os: osx
-    env: TESTS=sawHMAC SAW_HMAC_TEST=sha256 SAW=true GCC6_REQUIRED=false
-  - os: osx
-    env: TESTS=sawHMAC SAW_HMAC_TEST=sha384 SAW=true GCC6_REQUIRED=false
-  - os: osx
-    env: TESTS=sawHMAC SAW_HMAC_TEST=sha512 SAW=true GCC6_REQUIRED=false
-  - os: osx
-    env: S2N_LIBCRYPTO=openssl-1.1.0 LATEST_CLANG=true TESTS=fuzz
-  - os: osx
-    env: TESTS=sawDRBG                      SAW=true  GCC6_REQUIRED=false
-  - os: osx
-    env: TESTS=sawHMACFailure               SAW=true
   - os: osx
     env: S2N_LIBCRYPTO=openssl-1.1.x-master BUILD_S2N=true TESTS=integration GCC6_REQUIRED=true
   #This exception is because the test isn't finished yet, remove to turn on DRBG Saw tests
   - env: TESTS=sawDRBG                      SAW=true
+  include:
+  - os : linux
+    env : TESTS=sawHMAC SAW_HMAC_TEST=md5    SAW=true GCC6_REQUIRED=false
+    addons: &sawaddons
+      apt:
+        packages:
+          - clang-3.8
+          - llvm-3.8
+  - os : linux
+    env : TESTS=sawHMAC SAW_HMAC_TEST=sha1   SAW=true GCC6_REQUIRED=false
+    addons : *sawaddons
+  - os : linux
+    env : TESTS=sawHMAC SAW_HMAC_TEST=sha224 SAW=true GCC6_REQUIRED=false
+    addons : *sawaddons
+  - os : linux
+    env : TESTS=sawHMAC SAW_HMAC_TEST=sha256 SAW=true GCC6_REQUIRED=false
+    addons : *sawaddons
+  - os : linux
+    env : TESTS=sawHMAC SAW_HMAC_TEST=sha384 SAW=true GCC6_REQUIRED=false
+    addons : *sawaddons
+  - os : linux
+    env : TESTS=sawHMAC SAW_HMAC_TEST=sha512 SAW=true GCC6_REQUIRED=false
+    addons : *sawaddons
+  - os : linux
+    env : TESTS=tls SAW=true GCC6_REQUIRED=false
+    addons : *sawaddons    
+  - os : linux
+    env : TESTS=sawHMACFailure SAW=true
+    addons : *sawaddons    
   allow_failures:
     - os: osx
-    - env: S2N_LIBCRYPTO=openssl-1.1.x-master BUILD_S2N=true TESTS=integration GCC6_REQUIRED=true
   fast_finish: true
 
 before_install:
@@ -131,5 +134,6 @@ script:
   - if [[ "$TESTS" == "fuzz" ]]; then export PATH=$LATEST_CLANG_INSTALL_DIR/bin:$PATH && make clean && make fuzz ; fi
   - if [[ "$TRAVIS_OS_NAME" == "linux" && "$TESTS" == "sawHMAC" ]]; then make -C tests/saw/ tmp/verify_s2n_hmac_$SAW_HMAC_TEST.log ; fi
   - if [[ "$TESTS" == "sawDRBG" ]]; then make -C tests/saw tmp/spec/DRBG/DRBG.log ; fi
+  - if [[ "$TESTS" == "tls" ]]; then make -C tests/saw tmp/handshake.log && make -C tests/saw tmp/cork-uncork.log ; fi
   - if [[ "$TESTS" == "sawHMACFailure" ]]; then make -C tests/saw failure-tests ; fi
   - if [[ "$TESTS" == "ctverif" ]]; then .travis/run_ctverif.sh $CTVERIF_INSTALL_DIR ; fi

Makefile

@@ -33,7 +33,10 @@ bitcode :
 
 .PHONY : bc
 bc: 
-	${MAKE} -C crypto bc 
+	${MAKE} -C crypto bc
+#	${MAKE} -C stuffer bc
+	${MAKE} -C tls bc
+#	${MAKE} -C utils bc
 
 .PHONY : saw
 saw : bc 

crypto/Makefile

@@ -18,16 +18,13 @@ OBJS=$(SRCS:.c=.o)
 
 BITCODE_DIR?=../tests/saw/bitcode/
 
-BCS_1=s2n_hmac.bc s2n_drbg.bc
+BCS_1=s2n_hash.bc s2n_hmac.bc s2n_drbg.bc
 BCS=$(addprefix $(BITCODE_DIR), $(BCS_1))
 
 .PHONY : all
 all: $(OBJS)
 
 .PHONY : bc
-bc: $(BITCODE_DIR)all_llvm.bc
-
-$(BITCODE_DIR)all_llvm.bc : $(BCS)
-	llvm-link -o $@ $+
+bc: $(BCS)
 
 include ../s2n.mk

s2n.mk

@@ -28,6 +28,8 @@ CRYPTO_LIBS = -lcrypto
 CC	:= $(CROSS_COMPILE)$(CC)
 AR	= $(CROSS_COMPILE)ar
 RANLIB	= $(CROSS_COMPILE)ranlib
+CLANG    ?= clang-3.8
+LLVMLINK ?= llvm-link-3.8
 
 SOURCES = $(wildcard *.c *.h)
 CRUFT   = $(wildcard *.c~ *.h~ *.c.BAK *.h.BAK *.o *.a *.so *.dylib *.bc)
@@ -66,10 +68,10 @@ ifeq ($(S2N_UNSAFE_FUZZING_MODE),1)
 endif
 
 
-CFLAGS_LLVM = ${DEFAULT_CFLAGS} -emit-llvm -c -O1
+CFLAGS_LLVM = ${DEFAULT_CFLAGS} -emit-llvm -c -g -O1
 
 $(BITCODE_DIR)%.bc: %.c
-	clang $(CFLAGS_LLVM) -o $@ $< 
+	$(CLANG) $(CFLAGS_LLVM) -o $@ $< 
 
 
 INDENTOPTS = -npro -kr -i4 -ts4 -nut -sob -l180 -ss -ncs -cp1

stuffer/Makefile

@@ -16,7 +16,14 @@
 SRCS=$(wildcard *.c)
 OBJS=$(SRCS:.c=.o)
 
+BITCODE_DIR?=../tests/saw/bitcode/
+BCS_1=$(SRCS:.c=.bc)
+BCS=$(addprefix $(BITCODE_DIR), $(BCS_1))
+
 .PHONY : all
 all: $(OBJS)
 
+.PHONY : bc
+bc: $(BCS)
+
 include ../s2n.mk

tests/saw/Makefile

@@ -18,6 +18,7 @@
 # permissions and limitations under the License.
 ########################
 
+#The scripts are all of the saw files in this directory
 SCRIPTS = $(wildcard *.saw)
 #A log file will be created for each test in the temp dir
 LOGS=$(patsubst %.saw,tmp/%.log,$(SCRIPTS))
@@ -32,6 +33,10 @@ all:
 	@${MAKE} $(LOGS)
 	@${MAKE} failure-tests
 
+
+############################################
+## Clean targets
+############################################
 .PHONY : clean-logs
 clean-logs : 
 	$(RM) -- $(wildcard tmp/*.log)
@@ -44,13 +49,6 @@ clean-bitcode :
 clean-failure-logs :
 	$(RM) -- $(wildcard failure_tests/*.log)
 
-
-tmp/%.log : %.saw bitcode/all_llvm.bc tmp
-	@echo "Running formal verification with ${Z3_VERSION}"
-	@echo saw $<
-	@set -o pipefail; \
-	saw $< | tee $@
-
 .PHONY: clean
 clean: decruft
 
@@ -60,29 +58,73 @@ decruft : clean-logs
 	${RM} -r s2n
 	${RM} -r tmp
 
+clean_the_dir :
+	${RM} -r s2n
+	${RM} -r tmp
+	${RM} -r failure_tests/*.log
+	${RM} -r bitcode/*.bc
 
-FAILURE_PATCHES = $(wildcard failure_tests/*.patch)
-FAILURE_LOGS = $(FAILURE_PATCHES:.patch=.log)
+###########################################
+## Script Tests
+###########################################
 
+# To make a log we need the corresponding saw file, the all_llvm file, and a temp directory
+# The pipefail command causes the entire command to fail if saw fails, even though we pipe it to tee
+# without it we would see only the tee return code
+tmp/%.log : %.saw bitcode/all_llvm.bc tmp
+	@echo "Running formal verification with ${Z3_VERSION}"
+	@echo saw $<
+	@set -o pipefail; \
+	saw $< | tee $@
+
+
+###########################################
+## Failure Tests
+##
+## where we patch the code and make sure
+## that our proofs fail when it is patched
+## with errors
+###########################################
+
+#These won't work in parallel, so we just hard code them,
+#Otherwise we'd have to make a separate patched folder for each one
 .PHONY : failure-tests
 failure-tests : bitcode
 	@${MAKE} clean-failure-logs
-	@${MAKE} failure_tests/bad_magic_mod.log
-	@${MAKE} failure_tests/msgchange.log
+	@${MAKE} failure_tests/tls_early_ccs.log
+	@${MAKE} failure_tests/tls_missing_full_handshake.log
+	@${MAKE} failure_tests/sha_bad_magic_mod.log
+	@${MAKE} failure_tests/cork_one.log
+	@${MAKE} failure_tests/cork_two.log
 
-#@${MAKE} $(FAILURE_LOGS) commented for now because these can't happen in parallel
 
 #The bitcode files don't get deleted, in case we want to do tests on them
-.SECONDARY : $(wildcard btcode/*.bc)
+.SECONDARY : $(wildcard bitcode/*.bc)
 
-failure_tests/%.log : bitcode/%.bc
-	cp $< bitcode/all_llvm.bc
+# We're just making separate prefix targets for each saw script we want to do
+# negative tests on
+failure_tests/sha_%.log : bitcode/sha_%.bc
+        #this might not be necessary
+	cp $< bitcode/all_llvm.bc 
 	! saw verify_s2n_hmac_sha256.saw &> $@
 
-#keeping track of the status to make sure that even if the make fails the patch still gets undone
+failure_tests/tls_%.log : bitcode/tls_%.bc
+        #this might not be necessary
+	cp $< bitcode/all_llvm.bc 
+	! saw handshake.saw &> $@
+
+failure_tests/cork_%.log : bitcode/cork_%.bc
+        #this might not be necessary
+	cp $< bitcode/all_llvm.bc 
+	! saw cork-uncork.saw &> $@
+
+
+# we patch the s2n dir, build it with the top level s2n makefile, and
+# move the resulting, patched and linked llvm bitcode into our bitcode directory
 bitcode/%.bc : failure_tests/%.patch
 	patch -p1 -d s2n -i ../$<
 	${MAKE} -C s2n bc; \
+	${MAKE} bitcode/all_llvm.bc; \
         status=$$?; \
 	cp bitcode/all_llvm.bc $@
 	patch -R -p1 -d s2n -i  ../$<; \
@@ -94,18 +136,24 @@ bitcode :
 	${MAKE} clean_the_dir
 	${MAKE} bitcode/all_llvm.bc
 
-clean_the_dir :
-	${RM} -r s2n
-	${RM} -r tmp
-	${RM} -r failure_tests/*.log
-	${RM} -r bitcode/*.bc
+
+
+########################################################
+## Rules to copy the s2n directory for patching and bulding
+########################################################
 
 CRYPTO_C = $(wildcard ../../crypto/*.c) $(wildcard ../../crypto/*.h) ../../crypto/Makefile
 CRYPTO_COPY = $(addprefix s2n/crypto/, $(notdir $(CRYPTO_C)))
 
-UTILS_COPY =$(addprefix s2n/utils/, $(notdir $(wildcard ../../utils/*.h)))
-TLS_COPY =$(addprefix s2n/tls/, $(notdir $(wildcard ../../tls/*.h)))
-STUFFER_COPY =$(addprefix s2n/stuffer/, $(notdir $(wildcard ../../stuffer/*.h)))
+UTILS_C = $(wildcard ../../utils/*.c) $(wildcard ../../utils/*.h) ../../utils/Makefile
+UTILS_COPY =$(addprefix s2n/utils/, $(notdir $(UTILS_C)))
+
+TLS_C = $(wildcard ../../tls/*.c) $(wildcard ../../tls/*.h) ../../tls/Makefile
+TLS_COPY =$(addprefix s2n/tls/, $(notdir $(TLS_C)))
+
+STUFFER_C = $(wildcard ../../stuffer/*.c) $(wildcard ../../stuffer/*.h) ../../stuffer/Makefile
+STUFFER_COPY =$(addprefix s2n/stuffer/, $(notdir $(STUFFER_C)))
+
 API_COPY =$(addprefix s2n/api/, $(notdir $(wildcard ../../api/*.h)))
 ERROR_COPY =$(addprefix s2n/error/, $(notdir $(wildcard ../../error/*.h)))
 
@@ -132,12 +180,9 @@ export BITCODE_DIR := $(CURDIR)/bitcode/
 tmp:
 	mkdir -p tmp
 
-tmp/IS_PATCHED : | tmp
-	if [ -f ../patch.patch ]; then patch -p1 -d s2n -i ../patch.patch; fi
-	touch $@
-
-bitcode/all_llvm.bc : s2n/crypto s2n/utils s2n/stuffer s2n/tls s2n/api s2n/error s2n/Makefile s2n/s2n.mk $(CRYPTO_COPY) $(UTILS_COPY) $(TLS_COPY) $(STUFFER_COPY) $(API_COPY) $(ERROR_COPY)
+bitcode/all_llvm.bc : s2n/crypto s2n/utils s2n/tls s2n/api s2n/error s2n/stuffer s2n/Makefile s2n/s2n.mk $(CRYPTO_COPY) $(UTILS_COPY) $(TLS_COPY) $(API_COPY) $(ERROR_COPY) $(STUFFER_COPY)
 	${MAKE} -C s2n bc
+	${MAKE} -C bitcode all_llvm.bc
 
 s2n/%.h : ../../%.h
 	cp $< $@

tests/saw/bitcode/.gitignore

@@ -1 +1,2 @@
-*.bc
+*.bc
+*.ll

tests/saw/bitcode/Makefile

@@ -1 +1,6 @@
 include ../../../s2n.mk
+
+BCS=$(wildcard *.bc)
+
+all_llvm.bc : $(BCS)
+	$(LLVMLINK) -o $@ $+

tests/saw/cork-uncork.saw

@@ -0,0 +1,16 @@
+// Entry point for the corking correctness proof.
+import "spec/cork-uncork.cry";
+include "s2n_handshake_io.saw";
+
+//prove correspondence of the C code and the low-level model
+s2n_handshake_io_lowlevel;
+print "Verified that the low-level specification corresponds to the C code";
+//prove correspondence of the high-level and low-level models
+prove_print abc {{ highLevelSimulatesLowLevel `{16} }}; 
+print "Verified the low-level->high-level cork-uncork simulation";
+//prove no-double-uncork property for server mode
+prove_print abc {{ noDoubleCorkUncork }};
+print "Verified that double uncorking or corking cannot occur in server mode";
+//(for the record) evidence that a double uncork can occur in client mode
+print "Expecting failure when proving low-high simulation without the server mode assumption";
+sat abc {{ ~highLevelDoesNotSimulateLowLevel `{16} }};

tests/saw/failure_tests/cork_one.patch

@@ -0,0 +1,12 @@
+diff --git a/tls/s2n_handshake_io.c b/tls/s2n_handshake_io.c
+index fd9eb0d..51f4c53 100644
+--- a/tls/s2n_handshake_io.c
++++ b/tls/s2n_handshake_io.c
+@@ -242,6 +242,7 @@ static int s2n_advance_message(struct s2n_connection *conn)
+         if (s2n_connection_is_managed_corked(conn)) {
+             /* Set TCP_CORK/NOPUSH */
+             GUARD(s2n_socket_write_cork(conn));
++            GUARD(s2n_socket_write_cork(conn));
+         }
+
+         return 0;

tests/saw/failure_tests/cork_two.patch

@@ -0,0 +1,12 @@
+diff --git a/tls/s2n_handshake_io.c b/tls/s2n_handshake_io.c
+index fd9eb0d..11734ac 100644
+--- a/tls/s2n_handshake_io.c
++++ b/tls/s2n_handshake_io.c
+@@ -242,6 +242,7 @@ static int s2n_advance_message(struct s2n_connection *conn)
+         if (s2n_connection_is_managed_corked(conn)) {
+             /* Set TCP_CORK/NOPUSH */
+             GUARD(s2n_socket_write_cork(conn));
++            GUARD(s2n_socket_write_uncork(conn));
+         }
+
+         return 0;

tests/saw/failure_tests/tls_early_ccs.patch

@@ -0,0 +1,9 @@
+Binary files s2n/.git/index and s2n2/.git/index differ
+diff -p1 -Nur s2n/tls/s2n_handshake_io.c s2n2/tls/s2n_handshake_io.c
+--- s2n/tls/s2n_handshake_io.c	2017-07-14 15:29:09.806626239 -0700
++++ s2n2/tls/s2n_handshake_io.c	2017-07-19 11:17:13.347220835 -0700
+@@ -106,3 +106,3 @@ static message_type_t handshakes[64][16]
+             CLIENT_HELLO,
+-            SERVER_HELLO, SERVER_CERT, SERVER_HELLO_DONE,
++            SERVER_HELLO, CLIENT_CHANGE_CIPHER_SPEC, SERVER_CERT, SERVER_HELLO_DONE,
+             CLIENT_KEY, CLIENT_CHANGE_CIPHER_SPEC, CLIENT_FINISHED,