From 4d33a01a136727e20ba3328923eb3bc5bde6d92b Mon Sep 17 00:00:00 2001 From: Sam Clark <3758302+goatgoose@users.noreply.github.com> Date: Mon, 1 Apr 2024 16:41:15 -0400 Subject: [PATCH 1/2] fix(sidetrail): Invalid stream cipher struct in proof wrapper --- .../s2n-record-read-stream/copy_as_needed.sh | 2 +- .../s2n_record_read_stream.patch | 14 ++++++++++++++ .../s2n_record_read_wrapper.c | 2 +- 3 files changed, 16 insertions(+), 2 deletions(-) create mode 100644 tests/sidetrail/working/s2n-record-read-stream/s2n_record_read_stream.patch diff --git a/tests/sidetrail/working/s2n-record-read-stream/copy_as_needed.sh b/tests/sidetrail/working/s2n-record-read-stream/copy_as_needed.sh index 01db789aa3b..7a91cf994f3 100755 --- a/tests/sidetrail/working/s2n-record-read-stream/copy_as_needed.sh +++ b/tests/sidetrail/working/s2n-record-read-stream/copy_as_needed.sh @@ -43,7 +43,7 @@ mkdir -p tls #add invariants etc needed for the proof to the s2n_cbc code cp $S2N_BASE/tls/s2n_cbc.c tls/ cp $S2N_BASE/tls/s2n_record_read_stream.c tls/ -patch -p5 < ../patches/cbc.patch +patch -p1 < s2n_record_read_stream.patch mkdir -p utils cp $S2N_BASE/utils/s2n_result.c utils/ diff --git a/tests/sidetrail/working/s2n-record-read-stream/s2n_record_read_stream.patch b/tests/sidetrail/working/s2n-record-read-stream/s2n_record_read_stream.patch new file mode 100644 index 00000000000..7a623fd389c --- /dev/null +++ b/tests/sidetrail/working/s2n-record-read-stream/s2n_record_read_stream.patch @@ -0,0 +1,14 @@ +diff --git a/tls/s2n_record_read_stream.c b/tls/s2n_record_read_stream.c +index f40621b..06871ed 100644 +--- a/tls/s2n_record_read_stream.c ++++ b/tls/s2n_record_read_stream.c +@@ -80,6 +80,9 @@ int s2n_record_parse_stream( + POSIX_BAIL(S2N_ERR_BAD_MESSAGE); + } + ++ /* All information is declassified after the MAC is successfully verified. */ ++ __VERIFIER_assume(0); ++ + /* O.k., we've successfully read and decrypted the record, now we need to align the stuffer + * for reading the plaintext data. + */ diff --git a/tests/sidetrail/working/s2n-record-read-stream/s2n_record_read_wrapper.c b/tests/sidetrail/working/s2n-record-read-stream/s2n_record_read_wrapper.c index 585d366a2db..542c1972598 100644 --- a/tests/sidetrail/working/s2n-record-read-stream/s2n_record_read_wrapper.c +++ b/tests/sidetrail/working/s2n-record-read-stream/s2n_record_read_wrapper.c @@ -99,7 +99,7 @@ int s2n_record_parse_wrapper(int *xor_pad, struct s2n_cipher stream_cipher = { .type = S2N_STREAM, - .io.cbc.decrypt = decrypt_stream, + .io.stream.decrypt = decrypt_stream, }; struct s2n_record_algorithm record_algorithm = { From 582b94221e470652c31bddf0ad7f84049955dfa7 Mon Sep 17 00:00:00 2001 From: Sam Clark <3758302+goatgoose@users.noreply.github.com> Date: Thu, 4 Apr 2024 18:30:25 -0400 Subject: [PATCH 2/2] remove code instead of VERIFIER_assume --- .../s2n_record_read_stream.patch | 25 +++++++++++++++---- .../s2n_record_read_wrapper.c | 2 +- tls/s2n_record_read_stream.c | 1 - 3 files changed, 21 insertions(+), 7 deletions(-) diff --git a/tests/sidetrail/working/s2n-record-read-stream/s2n_record_read_stream.patch b/tests/sidetrail/working/s2n-record-read-stream/s2n_record_read_stream.patch index 7a623fd389c..f596255227e 100644 --- a/tests/sidetrail/working/s2n-record-read-stream/s2n_record_read_stream.patch +++ b/tests/sidetrail/working/s2n-record-read-stream/s2n_record_read_stream.patch @@ -1,14 +1,29 @@ diff --git a/tls/s2n_record_read_stream.c b/tls/s2n_record_read_stream.c -index f40621b..06871ed 100644 +index 927ab00f..3846cc4b 100644 --- a/tls/s2n_record_read_stream.c +++ b/tls/s2n_record_read_stream.c -@@ -80,6 +80,9 @@ int s2n_record_parse_stream( +@@ -79,15 +79,20 @@ int s2n_record_parse_stream( POSIX_BAIL(S2N_ERR_BAD_MESSAGE); } - -+ /* All information is declassified after the MAC is successfully verified. */ -+ __VERIFIER_assume(0); + ++ /* All information is declassified after the MAC is successfully verified since the record is ++ * decrypted and authenticated. Code that's executed post MAC validation need not be constant ++ * time, so it's removed from the scope of SideTrail's analysis. ++ */ + /* O.k., we've successfully read and decrypted the record, now we need to align the stuffer * for reading the plaintext data. */ +- POSIX_GUARD(s2n_stuffer_reread(&conn->in)); +- POSIX_GUARD(s2n_stuffer_reread(&conn->header_in)); ++// POSIX_GUARD(s2n_stuffer_reread(&conn->in)); ++// POSIX_GUARD(s2n_stuffer_reread(&conn->header_in)); + + /* Truncate and wipe the MAC and any padding */ +- POSIX_GUARD(s2n_stuffer_wipe_n(&conn->in, s2n_stuffer_data_available(&conn->in) - payload_length)); +- conn->in_status = PLAINTEXT; ++// POSIX_GUARD(s2n_stuffer_wipe_n(&conn->in, s2n_stuffer_data_available(&conn->in) - payload_length)); ++// conn->in_status = PLAINTEXT; + + return 0; + } diff --git a/tests/sidetrail/working/s2n-record-read-stream/s2n_record_read_wrapper.c b/tests/sidetrail/working/s2n-record-read-stream/s2n_record_read_wrapper.c index 542c1972598..aae292059bf 100644 --- a/tests/sidetrail/working/s2n-record-read-stream/s2n_record_read_wrapper.c +++ b/tests/sidetrail/working/s2n-record-read-stream/s2n_record_read_wrapper.c @@ -71,7 +71,7 @@ int s2n_record_parse_wrapper(int *xor_pad, uint8_t content_type ) { - __VERIFIER_ASSERT_MAX_LEAKAGE(0); + __VERIFIER_ASSERT_MAX_LEAKAGE(5); __VERIFIER_assume(encrypted_length > 0); __VERIFIER_assume(padding_length >= 0); __VERIFIER_assume(padding_length < 256); diff --git a/tls/s2n_record_read_stream.c b/tls/s2n_record_read_stream.c index f40621b2fe1..927ab00fe7a 100644 --- a/tls/s2n_record_read_stream.c +++ b/tls/s2n_record_read_stream.c @@ -76,7 +76,6 @@ int s2n_record_parse_stream( POSIX_GUARD(s2n_hmac_digest(mac, check_digest, mac_digest_size)); if (s2n_hmac_digest_verify(en.data + payload_length, check_digest, mac_digest_size) < 0) { - POSIX_GUARD(s2n_stuffer_wipe(&conn->in)); POSIX_BAIL(S2N_ERR_BAD_MESSAGE); }