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

feat: AwsKmsMrkAwareSymmetricKeyring #383

Merged
merged 26 commits into from
Oct 29, 2021
Merged

feat: AwsKmsMrkAwareSymmetricKeyring #383

Show file tree
Hide file tree
Changes from 14 commits
Commits
Show all changes
26 commits
Select commit Hold shift + click to select a range
0bb1514
feat: AwsKmsMrkAwareSymmetricKeyring
seebees Oct 20, 2021
5478563
Moving Closures into our code for review
seebees Oct 21, 2021
5d61a2d
Actions are a better name
seebees Oct 22, 2021
a28ebba
Remove unused imports
seebees Oct 22, 2021
302a7d2
Needs to be valid to use
seebees Oct 22, 2021
78fd161
Better subset type
seebees Oct 22, 2021
099e393
Argument order
seebees Oct 22, 2021
0720f59
Start to remove the old KMS keyring
seebees Oct 22, 2021
a8d75ff
No using
seebees Oct 22, 2021
31a0a87
Useable is a better name
seebees Oct 22, 2021
77f9c02
Remove comment
seebees Oct 22, 2021
e6a43e7
Unused import
seebees Oct 22, 2021
22c2d0d
Remove this.
seebees Oct 22, 2021
f82550b
Better filter name
seebees Oct 22, 2021
0692958
Update comment
seebees Oct 27, 2021
7e49afb
Spelling
seebees Oct 27, 2021
2d518c5
Simplify the import/name
seebees Oct 27, 2021
2b6fb33
Ensure constructor…
seebees Oct 27, 2021
117708e
Parsed to handle the `.value` confusion
seebees Oct 27, 2021
12966e8
Better error message
seebees Oct 27, 2021
e6c7778
DecryptCalledWith
seebees Oct 27, 2021
abf6900
Merge branch 'develop' into aws-kms-mrk-aware-symmetric-keyring
seebees Oct 27, 2021
1bc350f
More names
seebees Oct 27, 2021
4e1e3b6
Update the other keyring
seebees Oct 28, 2021
cdf3d22
Wow license, good job CI
seebees Oct 28, 2021
7089a3d
Update library
seebees Oct 29, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,3 +8,6 @@ test/**/Output/*

# Duvet output
specification_compliance_report.html

# VS Code local history
/.history
2 changes: 1 addition & 1 deletion aws-encryption-sdk-specification
Open in desktop
Submodule aws-encryption-sdk-specification updated from 3c7c72 to c35fbd
2 changes: 1 addition & 1 deletion libraries
Open in desktop
Submodule libraries updated from 162c2a to 2e56b6
1 change: 1 addition & 0 deletions src/KMS/AmazonKeyManagementService.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,3 +10,4 @@ module {:extern "Amazon.KeyManagementService"} AmazonKeyManagementService {
// TODO: https://github.com/awslabs/aws-encryption-sdk-dafny/issues/284
class {:extern "IAmazonKeyManagementService"} IAmazonKeyManagementService {}
}

11 changes: 11 additions & 0 deletions src/KMS/AwsKmsArnParsing.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,15 @@

include "../StandardLibrary/StandardLibrary.dfy"
include "../../libraries/src/Collections/Sequences/Seq.dfy"
include "../Util/UTF8.dfy"

module AwsKmsArnParsing {
import opened StandardLibrary
import opened Wrappers
import opened Seq
import UTF8

const MAX_AWS_KMS_IDENTIFIER_LENGTH := 2048

datatype AwsResource = AwsResource(
resourceType: string,
Expand Down Expand Up @@ -325,4 +329,11 @@ module AwsKmsArnParsing {
case AwsKmsRawResourceIdentifier(_) => None()
}
}

type AwsKmsIdentifierString = s: string |
&& ParseAwsKmsIdentifier(s).Success?
&& UTF8.IsASCIIString(s)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I didn't actually realize this, is it explicitly documented in the ARN and/or KMS documentation?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, but it is required for how we did Dafny. Because UTF8 is not "built in" :(

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That is why it is here, and NOT in ParseAwsKmsIdentifier

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What part of the Dafny requires ASCII (I'm assuming it's probably UTF8Valid requires later on)? And what is the consequence if there is some ID out there that uses some non-ASCII UTF8 character?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@lavaleri your intuition is correct

&& 0 < |s| <= MAX_AWS_KMS_IDENTIFIER_LENGTH
witness *

}
Loading