Add unbounded AES-GCM proof #80
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
It can instead be computed from the GCM context instead.
variable, similar to the already-existing verification commands.
encrypt update function with sybmolic message lengths using partial specifications for the constituent functions. Currently, we're having to play some tricks and make a few minor changes to the source to get this to work.
the "unbounded" operations.
except for decrypt update (probably not very hard). At this point, we are assuming block alignment (16-bytes), but I hope this will be not too hard to lift this restriction later.
We need a new specifciation refinement feature to really tie everything together, but the GHASH procedure is proved correct for block sizes from 1 to 18, which is the maximum number that can be processed following the bulk encrypt/decrypt phase.
Currently, this uses too much memory to actualy run all the proofs.
This currently captures the loop indexing variable, the pointer offsets into the various buffers involved, the IV+counter increments, and the status of a few of the other auxiliary registers. The major remaining pieces needed to capure in the invariant are 1) the status of the prefetched and byte-swapped input blocks on the stack 2) the state of the Xi register 3) the state of the output buffer.
The current state captures most of the "bookeeping" aspects of the loops, and are sufficent to prove memory-safety.
All obligations now go through, execpt the final Xi postcondition.
implementation-level specification functions.
the bulk encryption phase Xi postcondition.
There are a whole bunch of gross hacks in here; it would be nice to see if we can clean some of them up.
the gcm procedures that should eventually be handled in the same way as the other verification patches in `SAW/patch`.
Tweak the AES-HW-CTR proofs. This seems like it makes them a bit faster, but does not seem to affect the memory usage much.
encrypt Xi lemmas file to make them somewhat less mysterious.
and gcm_ghash_array_internal.
with arrayCopy. Not entirely sure if the statement or proof sketch is correct. Add comments to other lemmas with a brief description of what they prove.
and simplify the definition of `aesni_gcm_cipher_block6`.
This was referenced Apr 23, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.