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

Remove Assume in DefaultCMM #79

Closed
RustanLeino opened this issue Nov 11, 2019 · 0 comments · Fixed by #203
Closed

Remove Assume in DefaultCMM #79

RustanLeino opened this issue Nov 11, 2019 · 0 comments · Fixed by #203

Comments

@RustanLeino
Copy link
Contributor

DefaultCMM.GetEncryptionMaterials contains:

MessageHeader.AssumeValidAAD(enc_ec);

This unchecked assumption should be removed. Replacing it with a run-time check seems appropriate, probably here but possibly later (during serialization).
@RustanLeino RustanLeino mentioned this issue Nov 11, 2019
Merged
@lavaleri lavaleri self-assigned this Jan 9, 2020
@MatthewBennington MatthewBennington added this to the Public Beta milestone Jan 24, 2020
@RustanLeino RustanLeino mentioned this issue Feb 21, 2020
Merged
@lavaleri lavaleri removed their assignment Feb 21, 2020
@lavaleri lavaleri assigned lavaleri and RustanLeino and unassigned lavaleri Feb 27, 2020
RustanLeino added a commit that referenced this issue Feb 29, 2020
@RustanLeino
fix: Trade AssumeValidAAD for run-time checks and proofs (#203)
c3cfb9a 
* fix: Trade AssumeValidAAD for run-time checks and proofs

DefaultCMM.GetEncryptionMaterials is given a valid encryption context, to which it may
append the mapping `[reservedField := enc_vk]`. This would invalidate the encryption
context if the new entry causes problems with the size limits.

* `reservedField` is not UTF8 or is too long (but we know it's fine, because it's a constant)

* `enc_vk` is not UTF8 or is too long after it has been Base64 encoded (but we know it's fine, because of the new and
  tested postcondition of `Signature.KeyGen`, and because of some new specifications and lemmas regarding `Base64.Encode`)

* the updated encryption context exceeds the maximum number of allowed mappings (this is now run-time checked)

* the updated encryption context contains too many bytes altogether (this is now run-time checked, which involves
   walking over all the entries in the encryption context--possibly expensive)

Fixes #79

* Remove AssumeValidAAD altogether

The previous uses of AssumeValidAAD in test/SDK/Serialize.dfy have now been replaced
by proofs, found in test/Util/TestUtils.dfy.

* Respond to PR comment

* Replace extern postcondition with runtime check
@lavaleri lavaleri mentioned this issue Mar 3, 2020
Merged
josecorella pushed a commit to josecorella/aws-encryption-sdk-dafny that referenced this issue Oct 11, 2023
@texastony
feat(DDB-Java): convert DDB client To(Native/Dafny) (aws#79)
6441e55
josecorella pushed a commit that referenced this issue Oct 11, 2023
@texastony @josecorella
feat(DDB-Java): convert DDB client To(Native/Dafny) (#79)
53eca6d
josecorella pushed a commit that referenced this issue Oct 11, 2023
@texastony @josecorella
feat(DDB-Java): convert DDB client To(Native/Dafny) (#79)
84b7948
josecorella pushed a commit that referenced this issue Oct 11, 2023
@texastony @josecorella
feat(DDB-Java): convert DDB client To(Native/Dafny) (#79)
8514997
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: Trade AssumeValidAAD for run-time checks and proofs
3 participants
@RustanLeino @MatthewBennington @lavaleri