Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Repair TLS 1.3 proofs after c096a55 #3079

Merged
merged 5 commits into from
Oct 8, 2021
Merged

Repair TLS 1.3 proofs after c096a55 #3079

merged 5 commits into from
Oct 8, 2021

Conversation

RyanGlScott
Copy link
Contributor

@RyanGlScott RyanGlScott commented Oct 1, 2021 •
edited
Loading

Resolved issues:

This fixes an issue that was discovered in #3074/#3077 involving the TLS 1.3 proofs, which were re-enabled in #3031.

Description of changes:

Unfortunately, #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.

Call-outs:

The first commit in this PR simply reverts #3077 so that the TLS 1.3 proofs are re-enabled. That code is exactly as it was in #3031. The last two commits are the interesting part, so reviewers should look at those commits as a starting point.

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 PR only changes SAW code, so the behavior of s2n-tls itself is not affected. I made one change to the C code in tls/s2n_connection.h to move all of the bitfields upfront so that the SAW proofs can more maintainbly index into them with crucible_elem (see the comments in tests/saw/spec/handshake/handshake_io_lowlevel.saw). However, reordering bitfields should not have any user-observable effect on the C code itself.

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

@RyanGlScott RyanGlScott mentioned this pull request Oct 1, 2021
Merged
@RyanGlScott
Copy link
Contributor Author

I don't have the ability to view why the CI is failing, so I'll need to ask someone with the necessary permissions to do so. My hope is that the CI failure is simply due to the other issues discovered in #3074.

@RyanGlScott RyanGlScott mentioned this pull request Oct 4, 2021
Open
feliperodri
feliperodri suggested changes Oct 5, 2021
View reviewed changes
tls/s2n_config.h Outdated Show resolved Hide resolved
tls/s2n_connection.h Outdated Show resolved Hide resolved
@feliperodri feliperodri added the SAW Anything related to SAW proofs. label Oct 5, 2021
@feliperodri
Copy link
Contributor

@RyanGlScott could you also rebase your branch?

@RyanGlScott
Copy link
Contributor Author

I've rebased on top of 270bfbb.

@RyanGlScott
Copy link
Contributor Author

Is there anything else I should do before this can be merged?

@feliperodri
Copy link
Contributor

Is there anything else I should do before this can be merged?

I don't think so, just update your branch and merge once CI is happy with it. @lrstewart ?

@RyanGlScott
Revert "Revert "Re-enable TLS 1.3 SAW tests (aws#3031)" (aws#3077)"
92594c7 
This reverts commit c74ada5.
@RyanGlScott
s2n_connection: Move all bitfield fields up front
3b55ffc 
Ultimately, this is for the benefit of the SAW proofs. Due to a limitation
in how SAW currently works, bitfields must be accessed by index rather than
by name, and due to how often new fields are added to `s2n_connection`, the
only way to do this in way that's maintainable is to have all the bitfield
fields be up front. That way, the index to access the bitfield will always be
zero, which significantly decreases the likelihood that the SAW proofs will
need to be updated with each new field added to `s2n_connection`.

This is all rather unfortunate. See
GaloisInc/saw-script#1461 for a plan to
make handling bitfields more maintainable in SAW.
@RyanGlScott
Repair TLS 1.3 proofs after c096a55
8273de5 
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.
@RyanGlScott
Put SAW-tracked bitfield flags up front
0d21de8 
This will reduce the likelihood that their positions will change, which should
make the SAW proofs less susceptible to breakage.
@RyanGlScott
Expand comments in s2n_{config,connection} slightly
e6dde7f
@RyanGlScott
Copy link
Contributor Author

I've rebased on top of b05cc94. I don't have push access to s2n-tls, so I'll need someone else to merge this.

@feliperodri feliperodri merged commit c654369 into aws:main Oct 8, 2021
@RyanGlScott
Copy link
Contributor Author

Thanks!

@RyanGlScott RyanGlScott deleted the rgs/tls-1.3-fix branch October 8, 2021 11:54
RyanGlScott added a commit to RyanGlScott/s2n-tls that referenced this pull request Dec 5, 2021
@RyanGlScott
Restore original positions of bitfields in s2n_{config,connection}.h
a80a987 
Now that the positions of bitfields in structs are no longer important to SAW,
there is no reason to keep the bitfields in `s2n_config` and `s2n_connection`
up front, as was done in aws#3079. As a result, we can move the fields back to
their original positions before that commit.
RyanGlScott added a commit to RyanGlScott/s2n-tls that referenced this pull request Dec 15, 2021
@RyanGlScott
Use llvm_points_to_bitfield in SAW proofs
114ddd8 
This uses SAW's new `llvm_points_to_bitfield` command (introduced in
GaloisInc/saw-script#1539) to simplify specifications that involve the
bitfields in `s2n_config` and `s2n_connection`. In particular, there is no
longer any need to manually compute the size of the bitfields or the indices of
the fields within the bitfields, as these details are handled automatically
by `llvm_points_to_bitfield`. The positions of the fields within bitfields are
also no longer important.

This, along with a subsequent commit that will restore the bitfields' field
order to what they were before aws#3709, will address a review comment in
aws#3079 (comment).
RyanGlScott added a commit to RyanGlScott/s2n-tls that referenced this pull request Dec 15, 2021
@RyanGlScott
Restore original positions of bitfields in s2n_{config,connection}.h
d9623ed 
Now that the positions of bitfields in structs are no longer important to SAW,
there is no reason to keep the bitfields in `s2n_config` and `s2n_connection`
up front, as was done in aws#3079. As a result, we can move the fields back to
their original positions before that commit.
@RyanGlScott RyanGlScott mentioned this pull request Dec 15, 2021
Merged
RyanGlScott added a commit to RyanGlScott/s2n-tls that referenced this pull request Jan 4, 2022
@RyanGlScott
Use llvm_points_to_bitfield in SAW proofs
b55d135 
This uses SAW's new `llvm_points_to_bitfield` command (introduced in
GaloisInc/saw-script#1539) to simplify specifications that involve the
bitfields in `s2n_config` and `s2n_connection`. In particular, there is no
longer any need to manually compute the size of the bitfields or the indices of
the fields within the bitfields, as these details are handled automatically
by `llvm_points_to_bitfield`. The positions of the fields within bitfields are
also no longer important.

This, along with a subsequent commit that will restore the bitfields' field
order to what they were before aws#3709, will address a review comment in
aws#3079 (comment).
RyanGlScott added a commit to RyanGlScott/s2n-tls that referenced this pull request Jan 4, 2022
@RyanGlScott
Restore original positions of bitfields in s2n_{config,connection}.h
0c880a5 
Now that the positions of bitfields in structs are no longer important to SAW,
there is no reason to keep the bitfields in `s2n_config` and `s2n_connection`
up front, as was done in aws#3079. As a result, we can move the fields back to
their original positions before that commit.
RyanGlScott added a commit to RyanGlScott/s2n-tls that referenced this pull request Jan 10, 2022
@RyanGlScott
Use llvm_points_to_bitfield in SAW proofs
a7b0f77 
This uses SAW's new `llvm_points_to_bitfield` command (introduced in
GaloisInc/saw-script#1539) to simplify specifications that involve the
bitfields in `s2n_config` and `s2n_connection`. In particular, there is no
longer any need to manually compute the size of the bitfields or the indices of
the fields within the bitfields, as these details are handled automatically
by `llvm_points_to_bitfield`. The positions of the fields within bitfields are
also no longer important.

This addresses a review comment in
aws#3079 (comment).
RyanGlScott added a commit to RyanGlScott/s2n-tls that referenced this pull request Jan 24, 2022
@RyanGlScott
Use llvm_points_to_bitfield in SAW proofs
5c77b39 
This uses SAW's new `llvm_points_to_bitfield` command (introduced in
GaloisInc/saw-script#1539) to simplify specifications that involve the
bitfields in `s2n_config` and `s2n_connection`. In particular, there is no
longer any need to manually compute the size of the bitfields or the indices of
the fields within the bitfields, as these details are handled automatically
by `llvm_points_to_bitfield`. The positions of the fields within bitfields are
also no longer important.

This addresses a review comment in
aws#3079 (comment).
RyanGlScott added a commit to RyanGlScott/s2n-tls that referenced this pull request Jan 26, 2022
@RyanGlScott
Use llvm_points_to_bitfield in SAW proofs
ed355c6 
This uses SAW's new `llvm_points_to_bitfield` command (introduced in
GaloisInc/saw-script#1539) to simplify specifications that involve the
bitfields in `s2n_config` and `s2n_connection`. In particular, there is no
longer any need to manually compute the size of the bitfields or the indices of
the fields within the bitfields, as these details are handled automatically
by `llvm_points_to_bitfield`. The positions of the fields within bitfields are
also no longer important.

This addresses a review comment in
aws#3079 (comment).
RyanGlScott added a commit to RyanGlScott/s2n-tls that referenced this pull request Jan 26, 2022
@RyanGlScott
Use llvm_points_to_bitfield in SAW proofs
dda0442 
This uses SAW's new `llvm_points_to_bitfield` command (introduced in
GaloisInc/saw-script#1539) to simplify specifications that involve the
bitfields in `s2n_config` and `s2n_connection`. In particular, there is no
longer any need to manually compute the size of the bitfields or the indices of
the fields within the bitfields, as these details are handled automatically
by `llvm_points_to_bitfield`. The positions of the fields within bitfields are
also no longer important.

This addresses a review comment in
aws#3079 (comment).
RyanGlScott added a commit to RyanGlScott/s2n-tls that referenced this pull request Jan 27, 2022
@RyanGlScott
Use llvm_points_to_bitfield in SAW proofs
1270e70 
This uses SAW's new `llvm_points_to_bitfield` command (introduced in
GaloisInc/saw-script#1539) to simplify specifications that involve the
bitfields in `s2n_config` and `s2n_connection`. In particular, there is no
longer any need to manually compute the size of the bitfields or the indices of
the fields within the bitfields, as these details are handled automatically
by `llvm_points_to_bitfield`. The positions of the fields within bitfields are
also no longer important.

This addresses a review comment in
aws#3079 (comment).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@lrstewart lrstewart lrstewart approved these changes

@feliperodri feliperodri feliperodri approved these changes

Assignees

@RyanGlScott RyanGlScott

Labels
SAW Anything related to SAW proofs.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@RyanGlScott @feliperodri @lrstewart