-
Notifications
You must be signed in to change notification settings - Fork 22
KMS Keyring #86
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.
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
KMS Keyring #86
Conversation
A build command isn't the right place to attempt to run integration tests. Ideally we will run something similar in the future, but not until #54 is figured out.
After some investigation, I don't think there is a way to run such integration tests intelligently without creating a new testing approach. I've removed the line from |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice work in getting all this to verify, and even better to have the end-to-end encrypt/decrypt test work!
@@ -46,7 +48,10 @@ DEPS_CS = $(wildcard src/extern/dotnet/*.cs) | |||
|
|||
BCDLL = lib/BouncyCastle.1.8.5/lib/BouncyCastle.Crypto.dll | |||
|
|||
DEPS = $(DEPS_CS) $(BCDLL) | |||
AWSDLLS = lib/AWSSDK.KeyManagementService.3.3.101.83/lib/net45/AWSSDK.KeyManagementService.dll \ | |||
lib/AWSSDK.Core.3.3.103.62/lib/net45/AWSSDK.Core.dll |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Side-note I don't expect you to address in this PR, but I don't want to leave much longer: I'm starting to really hate all the hard-coded, manually-managed dependency references. We need to leverage nuget here somehow.
@@ -115,7 +115,7 @@ module DefaultCMMDef { | |||
|
|||
var dm :- kr.OnDecrypt(alg_id, enc_ctx, edks); | |||
if dm.None? { | |||
return Failure("Could not get materials required for decryption."); | |||
return Failure("Keyring.OnDecrypt did not return a value."); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Interesting, why do you prefer this version?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
When debugging, I found it helpful to not have duplicate error messages (there's an identical one on line 109), so I made this one more specific.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I smell a missing error enum. ;)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can of worms territory here :) See #32
src/SDK/Keyring/KMSKeyring.dfy
Outdated
|keyIDs| == 0 && generator.None? ==> isDiscovery | ||
} | ||
|
||
constructor(clientSupplier: string -> KMSUtils.KMSClient, keyIDs: seq<string>, generator: Option<string>, grantTokens: seq<string>) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We definitely need to document the strings the supplier will be passed - It should be public region names, right? It might even be worth defining a type alias for string
or string -> KMSUtils.KMSClient
Also, perhaps generatorKeyID
instead of generator
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Good point, could we get away with `region in ["us-east-1", "us-west-2"...]?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I wouldn't try to enumerate the regions anywhere in Dafny code. We definitely want to leave that up to the AWS libraries to manage.
|
||
datatype GenerateDataKeyResponse = GenerateDataKeyResponse(ciphertextBlob: seq<uint8>, contentLength: int, httpStatusCode: HttpStatusCode, keyID: string, plaintext: seq<uint8>, responseMetadata: ResponseMetadata) | ||
{ | ||
predicate method IsWellFormed() { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Any reason not to call this Valid()
instead?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
IsWellFormed
makes more sense to me since it's not checking if these datatypes are in a valid state. Rather we are checking if they are in the shape we want them to be in. That's just a feeling for me though, Valid()
may make more sense.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If we expect every GenerateDataKeyResponse
value that we ever produce to satisfy these conditions, then I think Valid()
is an appropriate name. If we expect to be passing around some GenerateDataKeyResponse
values that don't satisfy these conditions, then a different name, like IsWellFormed()
, seems good.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
f we expect every
GenerateDataKeyResponse
value that we ever produce to satisfy these conditions, then I think Valid() is an appropriate name.
This structure is the result of a network call, so I am not inclined to believe anything about it for sure.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Agreed with that, and I fully expect you to explicitly test Valid()
. I don't think there's a huge distinction between other code that can't statically guarantee the value is valid (especially since we're going to have external code in the shim like that) and code that happens to be deserializing a web service response.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There are two different things that we might be concerned about regarding what the KMS reponse contains:
- Things the API promises (according to aws documentation: https://docs.aws.amazon.com/kms/latest/APIReference/API_GenerateDataKey.html):
- 1 <= |ciphertextBlob| <= 6144
- 1 <= |keyID| <= 2048
- 1 <= |plaintext| <= 4096
- Things that we require of the response otherwise we can't continue:
- keyID is ASCII characters
- |keyID| < UINT16_LIMIT
- |ciphertextBlob| < UINT16_LIMIT
I'm currently having a hard time deciding whether either set of restrictions should be called "valid" or "wellformed" or something else. However, I do think that the former is something we should be able to assume about the response, and the latter is something that we need to check at runtime and fail if the conditions are not met.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
1 <= |ciphertextBlob| <= 6144
NP: That's the length of the base64 encoded ciphertext. We're dealing with bytes.
I think a base64 string of length 6144 translates to 4608 bytes, but I'd really like someone to confirm my math, because that seems odd.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think a base64 string of length 6144 translates to 4608 bytes, but I'd really like someone to confirm my math, because that seems odd.
I'd strongly suggest you actually define a function for that math if it shows up in the requirements, so that you can state something like 1 <= |ciphertextBlob| <= Base64Length(4608)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
How should the ESDK respond is the case where a response is within the bounds of the ESDK specification, but violates the restrictions in the KMS API reference?
i.e. KMS.Encrypt returns a ciphertext of length greater than Base64Length(6144)?
Note: The latest build failure is expected, and due to lack of IAM policy allowing KMS calls. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Removing the assume
and considering an alternate version of StringFind
are my main comments.
|
||
datatype GenerateDataKeyResponse = GenerateDataKeyResponse(ciphertextBlob: seq<uint8>, contentLength: int, httpStatusCode: HttpStatusCode, keyID: string, plaintext: seq<uint8>, responseMetadata: ResponseMetadata) | ||
{ | ||
predicate method IsWellFormed() { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If we expect every GenerateDataKeyResponse
value that we ever produce to satisfy these conditions, then I think Valid()
is an appropriate name. If we expect to be passing around some GenerateDataKeyResponse
values that don't satisfy these conditions, then a different name, like IsWellFormed()
, seems good.
new ArrayDString(response.KeyId.ToCharArray()), | ||
new Arraybyteseq(response.Plaintext.ToArray()), | ||
__default.ConvertMetaData(response.ResponseMetadata) | ||
)); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I've done both, so I'm afraid I'm no help to this discussion.
public STL.Result<GenerateDataKeyResponse> GenerateDataKey(GenerateDataKeyRequest request) { | ||
try { | ||
KMS.Model.GenerateDataKeyRequest kmsRequest = new KMS.Model.GenerateDataKeyRequest() | ||
{ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
My preference would be to put this {
at the end of the previous line, since it goes with the new
that's on that line.
AWS CodeBuild CI Report
Powered by github-codebuild-logs, available on the AWS Serverless Application Repository |
new ArrayDString(response.KeyId.ToCharArray()), | ||
new Arraybyteseq(response.Plaintext.ToArray()), | ||
__default.ConvertMetaData(response.ResponseMetadata) | ||
)); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't see a practicle value for one over the over, but aesthetically I prefer the close parens on the previous line. Is there a widely used linter for C# we could use?
src/extern/dotnet/KMS.cs
Outdated
} else { | ||
return new STL.Result_Failure<KMSClient>(new ArrayDString("Client Supplier does not have default region.".ToCharArray())); | ||
} | ||
} catch (System.Exception exception) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe I'm unfamiliar with C# idioms, but we should probably be more specific than System.Exception
. What exceptions are we looking to catch here?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is the pattern we're following in most of the extern files. Yes, I would be surprised if it were inline with c# idioms. I think this connects to #32, and how we plan on handling exceptions.
In this specific case, none of the methods called are documented to throw exceptions. But other methods seems to throw undocumented exceptions, so I aired on the side of caution.
Depending on what direction we want to go until #32 is resolved, it may make the most sense to remove this try block.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, at a bare minimum we should be catching all "non-fatal" exceptions so they don't short-circuit the entire Dafny runtime, as part of the "FFI". As long as System.Exception
is correct and doesn't include out-of-memory exceptions, this is fine for now. Agreed that once we have a way to distinguish different types of exceptions we'll want to handle them more specifically.
src/extern/dotnet/KMS.cs
Outdated
try { | ||
if (region.is_Some) { | ||
DString neverUsed = new ArrayDString("".ToCharArray()); | ||
return new STL.Result_Success<KMSClient>(new KMSClient(new KMS.AmazonKeyManagementServiceClient(RegionEndpoint.GetBySystemName(region.GetOrElse(neverUsed).ToString())))); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why are we doing a GetOrElse here if we know region is populated by this point?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
As far as I can tell, there is no other way to get the value from an option in c#.
test/KMS/KMSKeyring.dfy
Outdated
@@ -0,0 +1,85 @@ | |||
// RUN: %dafny /out:Output/KMSKeyring.exe "./KMSKeyring.dfy" ../../src/extern/dotnet/KMS.cs ../../src/extern/dotnet/UTF8.cs "%kmslib" "%awslib" /compile:2 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Because this file is testing logic in KMSKeyring it should be named test/Keyring/KMSKeyring.dfy.
We should also include tests that exercise the extern code.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We should also include tests that exercise the extern code.
I agree (I think there are a couple of comments saying this). Before we do that though, I think we need to think about what testing looks like.
This comes back to our ongoing discussions about what the test suite for this project looks like. I think we need to reach a decision on that before starting to write C# tests.
This is problematic, since I'm worried that the C# utility methods included in this C# are a potential weak link, as they are doing fairly complex things, and not exposed to and form of verification.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You should be able to use NUnit for the C# code AFAICT, once I get my .csproj/.sln files committed so that NUnit can resolve all the dependencies. If that doesn't happen in time I think it would be reasonable to cut a follow-up issue to backfill the unit tests.
In the extern C# files, don't call the constructor |
AWS CodeBuild CI Report
Powered by github-codebuild-logs, available on the AWS Serverless Application Repository |
Note: Right now the build checks are failing due to a timeout in If the |
AWS CodeBuild CI Report
Powered by github-codebuild-logs, available on the AWS Serverless Application Repository |
AWS CodeBuild CI Report
Powered by github-codebuild-logs, available on the AWS Serverless Application Repository |
AWS CodeBuild CI Report
Powered by github-codebuild-logs, available on the AWS Serverless Application Repository |
AWS CodeBuild CI Report
Powered by github-codebuild-logs, available on the AWS Serverless Application Repository |
AWS CodeBuild CI Report
Powered by github-codebuild-logs, available on the AWS Serverless Application Repository |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
One last nitpick, otherwise LGTM.
AWS CodeBuild CI Report
Powered by github-codebuild-logs, available on the AWS Serverless Application Repository |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks great! Just some minor quibbles to address first.
lit test -q -v | ||
|
||
clean-test: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
YAY, thank you. :)
I need to add somewhere that we need to call this after #101 is merged to clean up the random .cs files.
src/Main.dfy
Outdated
@@ -65,8 +65,14 @@ module Main { | |||
return; | |||
} | |||
|
|||
var ek, dk := RSAEncryption.RSA.RSAKeygen(2048, RSAEncryption.PKCS1); | |||
var keyring := new RawRSAKeyringDef.RawRSAKeyring(namespace.value, name.value, RSAEncryption.RSAPaddingMode.PKCS1, 2048, Some(ek), Some(dk)); | |||
var generatorStr := "arn:aws:kms:us-west-2:658956600833:key/b3537ef1-d8dc-4780-9f5a-55776cbb2f7f"; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can we not do this since you've got a separate integration test now? I've already relocated the current version of this as test/Client.dfy
in #101 :)
|
||
datatype GenerateDataKeyResponse = GenerateDataKeyResponse(ciphertextBlob: seq<uint8>, contentLength: int, httpStatusCode: HttpStatusCode, keyID: string, plaintext: seq<uint8>, responseMetadata: ResponseMetadata) | ||
{ | ||
predicate method IsWellFormed() { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think a base64 string of length 6144 translates to 4608 bytes, but I'd really like someone to confirm my math, because that seems odd.
I'd strongly suggest you actually define a function for that math if it shows up in the requirements, so that you can state something like 1 <= |ciphertextBlob| <= Base64Length(4608)
if !generatorResponse.IsWellFormed() { | ||
return Failure("Invalid response from KMS GenerateDataKey"); | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Idle thought: I'm thinking once #101 is in we can go with this idiom for all these dynamic checks:
var _ :- Require(generatorResponse.IsWellFormed(), "Invalid response from KMS GenerateDataKey");
Besides tightening up the code, I'm hoping it will push us towards better error handling in general, possibly being able to chain failures better - it might make sense to make Require
a built-in mechanism closer to requires
at some point.
src/extern/dotnet/KMS.cs
Outdated
} else { | ||
return new STL.Result_Failure<KMSClient>(new ArrayDString("Client Supplier does not have default region.".ToCharArray())); | ||
} | ||
} catch (System.Exception exception) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, at a bare minimum we should be catching all "non-fatal" exceptions so they don't short-circuit the entire Dafny runtime, as part of the "FFI". As long as System.Exception
is correct and doesn't include out-of-memory exceptions, this is fine for now. Agreed that once we have a way to distinguish different types of exceptions we'll want to handle them more specifically.
AWS CodeBuild CI Report
Powered by github-codebuild-logs, available on the AWS Serverless Application Repository |
AWS CodeBuild CI Report
Powered by github-codebuild-logs, available on the AWS Serverless Application Repository |
AWS CodeBuild CI Report
Powered by github-codebuild-logs, available on the AWS Serverless Application Repository |
@@ -48,6 +48,11 @@ module {:extern "STL"} StandardLibrary { | |||
} | |||
} | |||
|
|||
function method Base64LengthToByteLength(len: nat): nat { | |||
// This function does NOT account for padding characters. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Doesn't it need to for correctness though?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This method purely converts a nat
representing a base64 length, to a nat
representing byte length. There's no way for it to account for padding. That comment is meant to indicate that it shouldn't be called as Base64LengthToByteLength(|base64str|)
, as in that case there may be padding characters.
You're right.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
As discussed offline, we can cut an issue for this after merging
Issue #, if available: #66
Description of changes: Implemented KMS Keyring. In addation to the Keyring file, the files
KMSUtils.dfy
andKMS.cs
were added. Thebuildspec.yml
was edited to executemono build/Main.exe
, this should give us some semblance of a integration test.Note: To run
Main.exe
after these changes, you must have AWS credentials configured in your environment with sufficient permissions to to call:KMS:GenerateDataKey
,KMS:Encrypt
, andKMS:Decrypt
.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.