Skip to content

Commit

Permalink
fix(sidetrail): Invalid stream cipher struct in proof wrapper
Browse files Browse the repository at this point in the history
  • Loading branch information
goatgoose committed Apr 1, 2024
1 parent 0381567 commit be7870f
Show file tree
Hide file tree
Showing 3 changed files with 17 additions and 4 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -40,10 +40,9 @@ cp $S2N_BASE/stuffer/s2n_stuffer.c stuffer/
cp $S2N_BASE/stuffer/s2n_stuffer_network_order.c stuffer/

mkdir -p tls
#add invariants etc needed for the proof to the s2n_cbc code
cp $S2N_BASE/tls/s2n_cbc.c tls/
#add invariants etc needed for the proof
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/
Expand Down
Original file line number Diff line number Diff line change
@@ -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.
*/
Original file line number Diff line number Diff line change
Expand Up @@ -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 = {
Expand Down

0 comments on commit be7870f

Please sign in to comment.