refactor: Review of src/SDK/DefaultCMM.dfy #218
Conversation
AWS CodeBuild CI Report
Powered by github-codebuild-logs, available on the AWS Serverless Application Repository |
src/SDK/CMM/DefaultCMM.dfy
Outdated
| kr := k; | ||
| Repr := {this, kr} + k.Repr; | ||
| keyring := k; | ||
| Repr := {this, keyring} + k.Repr; | ||
| } | ||
|
|
||
| method GetEncryptionMaterials(materialsRequest: Materials.EncryptionMaterialsRequest) | ||
| returns (res: Result<Materials.ValidEncryptionMaterials>) | ||
| requires Valid() | ||
| requires ValidAAD(materialsRequest.encryptionContext) |
There was a problem hiding this comment.
I think with #79 in, we should also be able to just remove this line.
Just to be clear: we still need to be sure we pass our keyring a valid encryption context here, so you suggest a runtime check?
There was a problem hiding this comment.
The spec doesn't actually specify that the EC passed in MUST be serializable, which is why #210 suggests removing that condition from the CMM interface (which would require removing it here too). After the work done in #203, we should already be doing the runtime checks in deafult CMM needed to ensure that the output EC is serializable. As such, this line currently isn't doing anythign useful in DefaultCMM, and should be removed either in this PR or in a different PR which removes these conditions from the CMM interface.
test/SDK/DefaultCMM.dfy
Outdated
| expect shouldBeFail.Failure?, "GetEncryptionMaterials returned Success with bad input"; | ||
| } | ||
|
|
||
| method MakeKeyring() returns (res: Result<RawRSAKeyringDef.RawRSAKeyring>) |
There was a problem hiding this comment.
Because none of the above tests depend on the particular confiuration of the keyring, let's move this into TestUtils, where it can be possibly reused by other tests which similarly needs keyrings, but don't actually care about the keyring configuration.
- Remove ValidAAD precondition on DefaultCMM.GetEncryptionMaterials - Add runtime check of encryptionContext validity to DefaultCMM.GetEncryptionMaterials - Move MakeKeyring from DefaultCMMTests to TestUtils
AWS CodeBuild CI Report
Powered by github-codebuild-logs, available on the AWS Serverless Application Repository |
src/SDK/CMM/DefaultCMM.dfy
Outdated
| if UINT16_LIMIT <= |enc_ctx| { | ||
| return Failure("encryption context has too many entries"); | ||
| } else if UINT16_LIMIT <= len { |
There was a problem hiding this comment.
These two cases should already be covered by ComputeValidAAD. We should remove ComputeKVPairsLength in order to avoid two computations on the EC, and just check ComputeValidAAD instead.
There was a problem hiding this comment.
In this case, relying only on ComputeValidAAD() would mean we give less helpful error messages to the customer. I think Ideally we could break out ComputeValidAAD is a what in which we can identify how an encryption context violated it's bounds. Until then, I think the performance tradeoff is worth having better error messages.
If that sounds okay to you, I'll cut an issue and reference it in the code.
There was a problem hiding this comment.
The Default CMM shouldn't be aware of the different ways that the EC may be un-serializable, it just needs to concern itself with whether the EC it produces is serializable or not. But you are correct that this means less helpful messages to the user unless the thing computing the "AAD Validity" is able to surface the different failure cases, which we don't do here because ComputeValidAAD just returns a bool. Perhaps what we want here is a "ValidateECSerializability" method which errors if the EC can't be serialized into AAD. This might make sense because currently everywhere we use "ComputeValidAAD" we just return an error if it's false, and I can't think of a case where we would want to do anything other than error if we're working with a bad EC.
My preference would be to keep DefaultCMM as simple as possible, as least aware of the serializing logic as possible, and cut an issue to address surfacing better error messaging in this case. Regardless, I won't block on this.
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 |
Issue #, if available: resolves #41
Description of changes: Changes mostly to specification of the DefaultCMM. Added tests.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.