Refactor CMM/Keyring traits to use immutable datatypes, fix MultiKeyring #73
Conversation
Commented out algorithmSuiteID postcondition since the trait doesn't ensure that (yet) Valid() and unchanged(...) postconditions not yet validating
Mostly verifies now, just have to deal with Valid() on the key itself and the OnDecrypt path
…ws-encryption-sdk-dafny into robin-aws/multikeyring
Everything verifies now, but need to deal with "compilation of seq<TRAIT> is not supported" now
src/SDK/Keyring/Defs.dfy
Outdated
|
|
||
| module KeyringDefs { | ||
| module KeyringDefs { |
| method OnEncrypt(encMat: Materials.EncryptionMaterials) returns (res: Result<Materials.EncryptionMaterials>) | ||
| method OnEncrypt(algorithmSuiteID: Materials.AlgorithmSuite.ID, | ||
| encryptionContext: Materials.EncryptionContext, | ||
| plaintextDataKey: Option<seq<uint8>>) returns (res: Result<Option<Materials.ValidDataKeyMaterials>>) |
There was a problem hiding this comment.
I find the nested Result<Option<Y>> pattern to be somewhat verbose. But it seems like a symptom of something else. I think we should take a step back and think about what these values represent, and what we want these methods to return.
There was a problem hiding this comment.
I know what you mean, but I propose it only feels verbose because we have to have explicit syntax for error handling, which isn't the case in many other languages. It's the equivalent of a method that returns an Option<T>, where failures are handled as exceptions and therefore implicit.
I feel strongly that returning an Option in this case is the right way to model things, since the keyring is allowed to opt out of the operation. It's the equivalent of allowing the keyring to not modify the materials in the stateful version.
There was a problem hiding this comment.
Actually, it's also an option to return a ValidDataKeyMaterials with no encrypted data keys, since the non-emptiness of the list is only asserted at the CMM level. Is that more appealing?
There was a problem hiding this comment.
An empty list sounds better to me, but I'd like to hear @lavaleri and @RustanLeino's opinions too.
There was a problem hiding this comment.
I think Result<Option<>>, while a mouthful, contains exactly what we are trying to express here. We could take advantage of the fact that creating empty ValidDataKeyMaterials is easy, and argue that it would be sane to expect a no-op keyring to implement just that. However, I'm not sure it's worth doing that just to save a couple characters.
|
Heads up, I still have an outstanding refactoring of MultiKeyring that simplifies the code a lot, so don't spend time on that yet. |
- No need for proving the child Repr sets are disjoint apparently - Use simpler while loops instead of recursion
| encryptedDataKeys: seq<EncryptedDataKey>) | ||
| { | ||
| predicate method Valid() { | ||
| algorithmSuiteID.ValidPlaintextDataKey(plaintextDataKey) |
There was a problem hiding this comment.
We should also ensure each edk in encryptedDataKeys is valid.
There was a problem hiding this comment.
Great catch, turns out that was exactly what was needed to fix the Client.dfy verification hang.
* feat(Crypto-Java): AES GCM Extern Passes Dafny Tests. * enable tests Co-authored-by: texastony <[email protected]>
* feat(Crypto-Java): AES GCM Extern Passes Dafny Tests. * enable tests Co-authored-by: texastony <[email protected]>
* feat(Crypto-Java): AES GCM Extern Passes Dafny Tests. * enable tests Co-authored-by: texastony <[email protected]>
* feat(Crypto-Java): AES GCM Extern Passes Dafny Tests. * enable tests Co-authored-by: texastony <[email protected]>
Mostly addresses #65. Will address spacing on MultiKeyring.dfy separately to avoid hiding interesting changes in the noise.
Verifies but doesn't compile yet due to dafny-lang/dafny#406, will refactor to fix that if the overall approach looks good.
I'm very happy with using immutable values instead of side-effects everywhere, but it's interesting that wrapping up repeated predicate expressions so they can be shared (especially between trait and implementor definitions) has the side effect of hiding their definitions and requiring silly lemmas to verify things. Interested in Dafny best practices here.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.