Add unbounded AES-GCM verification, isolate newer SAW from other proofs

[RyanGlScott]

This proves unbounded AES-GCM functions, building on top of the cryptol-specs work in GaloisInc/cryptol-specs#72 and the saw-script work in GaloisInc/saw-script#2037. This supersedes previous efforts in #80, #139, and #143.

This requires a newer version of SAW to work than what aws-lc-verification's CI currently uses, so I isolated these proofs into their own SAW scripts, Cryptol specs, shell scripts, Docker image, and CI action. Moreover, some of the AES-GCM proofs use Z3's Constrained Horn Clause (CHC) feature, which is buggy on Z3-4.8.8. aws-lc-verification's other CI jobs are currently using Z3-4.8.8, so I specifically chose a newer version (Z3-4.8.14) for the new, AES-GCM–specific CI job.

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

[RyanGlScott]

Ah, I mistakenly introduced some changes to SAW/proof/common/helpers.saw which require a newer version of SAW, but weren't properly isolated to only affect AES-GCM. I'll push a fix momentarily.

[RyanGlScott]

At long last, the CI finally passes! Ready for review, @apetcher-amazon and @pennyannn.

[apetcher-amazon]

I have a few high-level comments before I examine the details.

1. A big thing that is missing is an indication of how well the proof can be parallelized. Unless I'm missing something, the current scripts appear to only check a single pair of mres and res_mres values because AES-GCM-check-entrypoint.go just falls through to AES_GCM.saw. You should be able to modify the Go scripts to execute AES_GCM.saw in parallel with multiple parameter values. Can you try this so we can get some indication of how much RAM is needed and how well we can parallelize the proof? You don't need to run the SAW script on all parameter values---just show how many parameter values we can check in parallel. The runner that we are using for the CI has 64 GB of RAM.
2. In SPEC.md, you should describe the spec of the top-level functions like EVP_EncryptUpdate and EVP_EncryptFinal. There is no need to include specs for internal functions.
3. The Cryptol spec for AES-GCM is very hard to follow. Can you organize/simplify it a bit and/or add some comments. It needs to be easy for someone to examine it and agree that it describes (some implementation-specific variant of) AES-GCM.
4. In general, the code could be improved with more comments and some slight tweaks to organization. Please look over the code and make sure that magic numbers are explained and defined using constants(e.g. why length is a 28-bit integer), variable names are clear or described using documentation (e.g. meaning of mres and res_mres are not clear from the name), etc. Also, move large proof scripts that do not need to be inspected out of top-level files like AES-GCM.saw so it is easier to see what is proved.

[RyanGlScott]

1. A big thing that is missing is an indication of how well the proof can be parallelized.

Yes, a fair point. I can experiment locally to see how well we can parallelize it, although my local machine only has 32 GB of RAM.

2. In SPEC.md, you should describe the spec of the top-level functions like EVP_EncryptUpdate and EVP_EncryptFinal. There is no need to include specs for internal functions.

Ah, good to know. I'll do that.

3. The Cryptol spec for AES-GCM is very hard to follow. Can you organize/simplify it a bit and/or add some comments. It needs to be easy for someone to examine it and agree that it describes (some implementation-specific variant of) AES-GCM.

Yes, quite so. One of the challenges here is that much of the Cryptol code checked in here is not meant to reflect the official NIST AES-GCM specification so much as it is an aid for SAW to help identify the loop structure of the C code itself, so it is written in a much more "low-level" style than what you'd find in the NIST spec. The Cryptol code that is closer to the NIST spec is found in GaloisInc/cryptol-specs#72 (in AES_256_GCM.cry).

That being said, the comments could definitely explain all this better. I'll do that and add some more commentary where I can.

4. In general, the code could be improved with more comments and some slight tweaks to organization. Please look over the code and make sure that magic numbers are explained and defined using constants(e.g. why length is a 28-bit integer), variable names are clear or described using documentation (e.g. meaning of mres and res_mres are not clear from the name), etc. Also, move large proof scripts that do not need to be inspected out of top-level files like AES-GCM.saw so it is easier to see what is proved.

Sure, will do.

[pennyannn]

I want to confirm if my understanding is correct. In this proof, the bulk processing functions aesni_gcm_encrypt and aesni_gcm_decrypt are verified with arbitrary input length, therefore they are unbounded proofs.

For all other functions, they are all bounded proofs serving some purpose, and this includes proofs for the top-level EVP functions as well. For example, aes_hw_ctr32_encrypt_blocks is only verified with number of blocks smaller than MIN_BULK_BLOCKS = 18. This is because this function is only used when there aren't enough message blocks to do one loop iteration of bulk processing. Likewise for GHASH functions like gcm_ghash_avx.

For top-level EVP function, I believe only one set of verification parameter is chosen for the proof, so it is also a bounded proof. The override matching to bulk functions aesni_gcm_encrypt and aesni_gcm_decrypt will automatically figure out what the message block length is.

Is my understanding correct?

If so, could you add some comments to the proof command for the top-level EVP functions (the various llvm_verify for EVP_EncryptUpdate and EVP_DecryptUpdate) explaining the meaning of the input numbers. What do they refer to and why we are choosing this set of parameter?

[pennyannn]

Wow, this is so cool! All workflow pass and apparently the proofs now run faster even though we are checking more combinations of parameters! I wonder if it is because you removed the bounded proofs. I will start reviewing. Thank you so much for the help, @RyanGlScott !

[pennyannn]

I have reviewed the workflow, shell scripts and most of the SAW files (excluding goal-rewrites files). I will send another review for the Cryptol files and the goal-rewrites.

[pennyannn]

I finished reviewing goal-rewrites and the Cryptol files.

[pennyannn]

LGTM. I just had one minor comment.