Re-enable TLS 1.3 SAW tests #3031

RyanGlScott · 2021-09-02T19:26:55Z

Resolved issues:

Resolves #1826.

Description of changes:

This PR re-enables the SAW tests that exercise TLS 1.3–specific code paths. In particular, we now:

Check TLS 1.3–specific code in the specificatins for s2n_conn_set_handshake_type and s2n_advance_message. The key change is in setup_connection, which now checks all possible actual_protocol_version values instead of just S2N_TLS12. I also modernized the implementations of the Cryptol TLS 1.3 code, especially tls13_state_machine_fnandtls13_handshakes`.
Check for all possible handshake_types in initial_connection, not just INITIAL.
Update the cork-uncork proofs to only check handshakes up until the first APPLICATION_DATA message, since going past that leads to strange results, especially for non-INITIAL handshake_types. The trace_advance_message function also now uses s2nTrans instead of simply advance_message, which is a more accurate portrayal of what actually goes on in S2N.
Update the TLS 1.3 RFC state machine to be aware of EARLY_CLIENT_CCS, WITH_EARLY_DATA, and MIDDLEBOX_COMPAT.
Consolidate the TLS_HELLO_RETRY_REQUEST handshake_action (which no longer exists in S2N) with TLS_SERVER_HELLO.

Call-outs:

I primarily tested against LLVM 3.9.1 and a nightly version of SAW (0.6.0.99), as this is what the CI currently uses. I have also verified that these changes work with a newer version of LLVM (10) and SAW (0.8), but I did not change the versions of these tools as part of this PR. If there is interest in updating the versions of these tools, I would be happy to do so.

Testing:

To check the proofs, run make -C tests/saw tmp/verify_handshake.log. This should be covered by CI, which runs this command as one of its steps.

For the most part, this only changes SAW code. The one exception is a change that I made to tls/Makefile, which was only required to make sure that s2n_tls13.bc is linked against in the bitcode file that SAW verifies against. None of the C code was changed.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

tests/saw/spec/handshake/s2n_handshake_io.cry

tests/saw/spec/handshake/handshake_io_lowlevel.saw

tests/saw/spec/handshake/s2n_handshake_io.cry

lrstewart · 2021-09-13T22:52:10Z

You'll need to rebase to pick up 01b3c46 and get the integration tests to pass.

Fortunately, these changes are backwards compatible with older versions of SAW as well.

…e_type()

z3 appears to bestow some performance gains over abc in these proofs.

This is needed to make the SAW proofs work after commit 9a4233e, which moves the logic for detecting QUIC support to `s2n_connection_is_quic_enabled` in `s2n_quic_support.c`.

feliperodri

Only minor comments.

tests/saw/spec/handshake/handshake.saw

tests/saw/spec/handshake/handshake_io_lowlevel.saw

tests/saw/spec/handshake/s2n_handshake_io.cry

This reverts commit 04e494e.

This reverts commit d5a044b.

Unfortunately, aws#3031 landed before it had a chance to be tested against c096a55, which alters the logic used to check whether QUIC is enabled `s2n_connection_is_quic_enabled`. This updates the corresponding SAW specification to take the new definition of `s2n_connection_is_quic_enabled` into account. This requires inspecting one more bitfield in `s2n_connection` to accomplish. While I was in town, I updated the relevant comments in the SAW specification that describe `quic_enabled` and friends.

This reverts commit d5a044b. CI won't pass because the Let's Encrypt trust fix is not included.

This reverts commit c74ada5.

Unfortunately, aws#3031 landed before it had a chance to be tested against c096a55, which alters the logic used to check whether QUIC is enabled `s2n_connection_is_quic_enabled`. This updates the corresponding SAW specification to take the new definition of `s2n_connection_is_quic_enabled` into account. This requires inspecting one more bitfield in `s2n_connection` to accomplish. While I was in town, I took the time to tidy up the various pieces of the SAW specification that involve bitfields. It's still not as pretty as it could be, but it's a sit better than it was before.

This reverts commit c74ada5.

Unfortunately, aws#3031 landed before it had a chance to be tested against c096a55, which alters the logic used to check whether QUIC is enabled `s2n_connection_is_quic_enabled`. This updates the corresponding SAW specification to take the new definition of `s2n_connection_is_quic_enabled` into account. This requires inspecting one more bitfield in `s2n_connection` to accomplish. While I was in town, I took the time to tidy up the various pieces of the SAW specification that involve bitfields. It's still not as pretty as it could be, but it's a sit better than it was before.

This reverts commit c74ada5.

Unfortunately, aws#3031 landed before it had a chance to be tested against c096a55, which alters the logic used to check whether QUIC is enabled `s2n_connection_is_quic_enabled`. This updates the corresponding SAW specification to take the new definition of `s2n_connection_is_quic_enabled` into account. This requires inspecting one more bitfield in `s2n_connection` to accomplish. While I was in town, I took the time to tidy up the various pieces of the SAW specification that involve bitfields. It's still not as pretty as it could be, but it's a sit better than it was before.

lrstewart self-requested a review September 3, 2021 17:34

lrstewart reviewed Sep 9, 2021

View reviewed changes

lrstewart mentioned this pull request Sep 13, 2021

Validate early TLS1.3 handshake types in s2n_conn_set_tls13_handshake_type #3047

Open

lrstewart reviewed Sep 13, 2021

View reviewed changes

tests/saw/spec/handshake/s2n_handshake_io.cry Outdated Show resolved Hide resolved

RyanGlScott added 25 commits September 14, 2021 09:11

Allow building with saw-0.8

9d10c82

Fortunately, these changes are backwards compatible with older versions of SAW as well.

Update TLS 1.3 handshakes, state machine in Cryptol

4aeb1fe

Verify TLS 1.3 code paths for advance_message() and conn_set_handshak…

c613f67

…e_type()

Make handshake_io_lowlevel.saw work with LLVM 7+

fe6e926

Consolidate conn_set_handshake_type

a974a9c

rfc_handshake_tls13: Fill in missing fields

f98c648

Restore tls13rfcSimulatesS2N proof

3201e2f

Remove unused Cryptol early data states

eecaf85

Generalize initial_connection to test more handshake_types

3b63d7d

Replace TLS_HELLO_RETRY_REQUEST with TLS_SERVER_HELLO

c5a97a8

Hackily exclude illegal WITH_EARLY_DATA handshakes

978b86d

Refine RFC state machine

7022c18

A slightly more reasonable attempt at excluding illegal handshakes

4a4ad1f

Delete unnecessary precondition in initial_connection

ec8160b

Refine predicate in connectionParameters

7fc0b3b

Move precondition to initial_connection

56c1011

Consider quic_enabled in TLS 1.3 proofs

09b3574

Adjust compat_mode based on middlebox compat

4e318a5

Add a middlebox-specific precondition to initial_connection

a139e88

Repair the cork-uncork properties by constraining them slightly

ee34344

trace_advance_message: Use s2nTrans instead of advance_message

91a3c7e

Use z3 instead of abc for cork-uncork proofs

28f78c1

z3 appears to bestow some performance gains over abc in these proofs.

Replace llvm_equal with llvm_points_to

8fc45d9

Remove unneeded reference to quic_enabled

fb90443

Rename setup_connection functions, correct comments

b28047c

RyanGlScott added 3 commits September 14, 2021 09:11

Mention #3047 in the comments

66096cb

Rephrase comments in initial_connection slightly

7396326

tls/Makefile: add s2n_quic_support.bc

de3387a

This is needed to make the SAW proofs work after commit 9a4233e, which moves the logic for detecting QUIC support to `s2n_connection_is_quic_enabled` in `s2n_quic_support.c`.

RyanGlScott mentioned this pull request Sep 15, 2021

handshake_io_lowlevel.saw: Avoid the use of an explicit chosen_psk_null boolean argument #3052

Open

lrstewart approved these changes Sep 15, 2021

View reviewed changes

zaherd requested a review from feliperodri September 27, 2021 16:42

feliperodri approved these changes Sep 27, 2021

View reviewed changes

feliperodri assigned RyanGlScott Sep 27, 2021

feliperodri added type/test type/tls_1.3 labels Sep 27, 2021

RyanGlScott added 5 commits September 27, 2021 19:00

Factor out S2N_MAX_HANDSHAKE_LENGTH in s2n_handshake_io.cry

ba445a5

Abbreviate issue URL in s2n_handshake_io.cry comments

04e494e

Comment why s2n_conn_set_handshake_type_spec is invoked twice

b1a8c6f

Reference GaloisInc/saw-script#1461 in bitfield-adjacent code

50e0db8

Revert "Abbreviate issue URL in s2n_handshake_io.cry comments"

895ec15

This reverts commit 04e494e.

lrstewart merged commit d5a044b into aws:main Sep 29, 2021

dougch added a commit that referenced this pull request Sep 30, 2021

Revert "Re-enable TLS 1.3 SAW tests (#3031)"

623be58

This reverts commit d5a044b.

dougch mentioned this pull request Sep 30, 2021

Revert "Re-enable TLS 1.3 SAW tests" #3077

Merged

RyanGlScott mentioned this pull request Oct 1, 2021

Repair TLS 1.3 proofs after c096a55 #3079

Merged

dougch added a commit that referenced this pull request Oct 1, 2021

Revert "Re-enable TLS 1.3 SAW tests (#3031)" (#3077)

c74ada5

This reverts commit d5a044b. CI won't pass because the Let's Encrypt trust fix is not included.

dougch added a commit to dougch/s2n-tls that referenced this pull request Oct 1, 2021

Revert "Re-enable TLS 1.3 SAW tests (aws#3031)" (aws#3077)

282db13

This reverts commit d5a044b. CI won't pass because the Let's Encrypt trust fix is not included.

dougch added a commit to dougch/s2n-tls that referenced this pull request Oct 1, 2021

Revert "Re-enable TLS 1.3 SAW tests (aws#3031)" (aws#3077)

c933cf8

This reverts commit d5a044b. CI won't pass because the Let's Encrypt trust fix is not included.

dougch added a commit to dougch/s2n-tls that referenced this pull request Oct 1, 2021

Revert "Re-enable TLS 1.3 SAW tests (aws#3031)" (aws#3077)

fc9ad4f

This reverts commit d5a044b. CI won't pass because the Let's Encrypt trust fix is not included.

RyanGlScott added a commit to RyanGlScott/s2n-tls that referenced this pull request Oct 2, 2021

Revert "Revert "Re-enable TLS 1.3 SAW tests (aws#3031)" (aws#3077)"

b83e187

This reverts commit c74ada5.

RyanGlScott added a commit to RyanGlScott/s2n-tls that referenced this pull request Oct 5, 2021

Revert "Revert "Re-enable TLS 1.3 SAW tests (aws#3031)" (aws#3077)"

bb240be

This reverts commit c74ada5.

RyanGlScott added a commit to RyanGlScott/s2n-tls that referenced this pull request Oct 7, 2021

Revert "Revert "Re-enable TLS 1.3 SAW tests (aws#3031)" (aws#3077)"

92594c7

This reverts commit c74ada5.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Re-enable TLS 1.3 SAW tests #3031

Re-enable TLS 1.3 SAW tests #3031

RyanGlScott commented Sep 2, 2021 •

edited

Loading

lrstewart commented Sep 13, 2021

feliperodri left a comment

Re-enable TLS 1.3 SAW tests #3031

Re-enable TLS 1.3 SAW tests #3031

Conversation

RyanGlScott commented Sep 2, 2021 • edited Loading

Resolved issues:

Description of changes:

Call-outs:

Testing:

lrstewart commented Sep 13, 2021

feliperodri left a comment

Choose a reason for hiding this comment

RyanGlScott commented Sep 2, 2021 •

edited

Loading