Yan Peng
Yan Peng
AWS-LC [PR1324](https://github.com/aws/aws-lc/pull/1324) adds support for EVP_PKEY_HMAC. Currently proofs for HMAC only covers up to functions `HMAC_Init_ex`, `HMAC_Update`, `HMAC_Final` and etc. We need to extend the proofs to cover the top-level...
When the CI produces this error message "Docker Action run completed with exit code 137", it means the Github runner is running out of memory. There are many possibilities for...
As pointed out in #68 , it should be possible to refactor the code in ECDH, ECDSA and RSA proofs to allow code reuse.
### Description: A detailed description of your contribution. Why is this change necessary? ### Testing: What tests have been run? Did `make all` succeed for your changes? Was conformance testing...
### Description: This PR contains: 1. Adding instruction class -- Move wide (immediate) 2. Adding instruction class -- Hints (for NOP) 3. Fixing a bug in conditional branch instructions 4....
### Description: This PR adds ELFLoader tests for AES-GCM assembly routines. When updating the binary file crypto_test, the file exceeds the maximum file size on Github. In this PR, crypto_test...
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license. C11 upgrade in AWS-LC revealed a bug in older version...
### Description: A detailed description of your contribution. Why is this change necessary? ### Testing: What tests have been run? Did `make all` succeed for your changes? Was conformance testing...
Currently, `List` type is used when we refer to a list of `BitVec` in functional specification of AES-GCM. This means information on the length of the list of `BitVec`s are...
### Description: Currently, LNSym could not handle `gcm_init_v8` fully expanded out and solved by `bv_decide`. Simply expand out the definitions (even with pmult uninterpreted) will result in stack overflow from...