Skip to content

Commit

Permalink
feat: add expected context cmm (#146)
Browse files Browse the repository at this point in the history
* feat: add expected context cmm

* another polymorph run for test vectors

---------

Co-authored-by: seebees <[email protected]>
  • Loading branch information
2 people authored and josecorella committed Oct 11, 2023
1 parent 840f3e7 commit 1ddbb7e
Show file tree
Hide file tree
Showing 14 changed files with 562 additions and 124 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,7 @@ include "../../StandardLibrary/src/Index.dfy"
CreateRawRsaKeyring := [];
CreateAwsKmsRsaKeyring := [];
CreateDefaultCryptographicMaterialsManager := [];
CreateExpectedEncryptionContextCMM := [];
CreateCryptographicMaterialsCache := [];
CreateDefaultClientSupplier := [];
InitializeEncryptionMaterials := [];
Expand Down Expand Up @@ -81,6 +82,7 @@ include "../../StandardLibrary/src/Index.dfy"
ghost var CreateRawRsaKeyring: seq<DafnyCallEvent<CreateRawRsaKeyringInput, Result<IKeyring, Error>>>
ghost var CreateAwsKmsRsaKeyring: seq<DafnyCallEvent<CreateAwsKmsRsaKeyringInput, Result<IKeyring, Error>>>
ghost var CreateDefaultCryptographicMaterialsManager: seq<DafnyCallEvent<CreateDefaultCryptographicMaterialsManagerInput, Result<ICryptographicMaterialsManager, Error>>>
ghost var CreateExpectedEncryptionContextCMM: seq<DafnyCallEvent<CreateExpectedEncryptionContextCMMInput, Result<ICryptographicMaterialsManager, Error>>>
ghost var CreateCryptographicMaterialsCache: seq<DafnyCallEvent<CreateCryptographicMaterialsCacheInput, Result<ICryptographicMaterialsCache, Error>>>
ghost var CreateDefaultClientSupplier: seq<DafnyCallEvent<CreateDefaultClientSupplierInput, Result<IClientSupplier, Error>>>
ghost var InitializeEncryptionMaterials: seq<DafnyCallEvent<InitializeEncryptionMaterialsInput, Result<EncryptionMaterials, Error>>>
Expand Down Expand Up @@ -464,6 +466,36 @@ include "../../StandardLibrary/src/Index.dfy"
ensures CreateDefaultCryptographicMaterialsManagerEnsuresPublicly(input, output)
ensures History.CreateDefaultCryptographicMaterialsManager == old(History.CreateDefaultCryptographicMaterialsManager) + [DafnyCallEvent(input, output)]

predicate CreateExpectedEncryptionContextCMMEnsuresPublicly(input: CreateExpectedEncryptionContextCMMInput , output: Result<ICryptographicMaterialsManager, Error>)
// The public method to be called by library consumers
method CreateExpectedEncryptionContextCMM ( input: CreateExpectedEncryptionContextCMMInput )
returns (output: Result<ICryptographicMaterialsManager, Error>)
requires
&& ValidState() && ( input.underlyingCMM.Some? ==>
&& input.underlyingCMM.value.ValidState()
&& input.underlyingCMM.value.Modifies !! {History}
) && ( input.keyring.Some? ==>
&& input.keyring.value.ValidState()
&& input.keyring.value.Modifies !! {History}
)
modifies Modifies - {History} ,
(if input.underlyingCMM.Some? then input.underlyingCMM.value.Modifies else {}) ,
(if input.keyring.Some? then input.keyring.value.Modifies else {}) ,
History`CreateExpectedEncryptionContextCMM
// Dafny will skip type parameters when generating a default decreases clause.
decreases Modifies - {History} ,
(if input.underlyingCMM.Some? then input.underlyingCMM.value.Modifies else {}) ,
(if input.keyring.Some? then input.keyring.value.Modifies else {})
ensures
&& ValidState()
&& ( output.Success? ==>
&& output.value.ValidState()
&& output.value.Modifies !! {History}
&& fresh(output.value)
&& fresh ( output.value.Modifies - Modifies - {History} - (if input.underlyingCMM.Some? then input.underlyingCMM.value.Modifies else {}) - (if input.keyring.Some? then input.keyring.value.Modifies else {}) ) )
ensures CreateExpectedEncryptionContextCMMEnsuresPublicly(input, output)
ensures History.CreateExpectedEncryptionContextCMM == old(History.CreateExpectedEncryptionContextCMM) + [DafnyCallEvent(input, output)]

predicate CreateCryptographicMaterialsCacheEnsuresPublicly(input: CreateCryptographicMaterialsCacheInput , output: Result<ICryptographicMaterialsCache, Error>)
// The public method to be called by library consumers
method CreateCryptographicMaterialsCache ( input: CreateCryptographicMaterialsCacheInput )
Expand Down Expand Up @@ -715,6 +747,11 @@ include "../../StandardLibrary/src/Index.dfy"
datatype CreateDefaultCryptographicMaterialsManagerInput = | CreateDefaultCryptographicMaterialsManagerInput (
nameonly keyring: IKeyring
)
datatype CreateExpectedEncryptionContextCMMInput = | CreateExpectedEncryptionContextCMMInput (
nameonly underlyingCMM: Option<ICryptographicMaterialsManager> ,
nameonly keyring: Option<IKeyring> ,
nameonly requiredEncryptionContextKeys: EncryptionContextKeys
)
datatype CreateMultiKeyringInput = | CreateMultiKeyringInput (
nameonly generator: Option<IKeyring> ,
nameonly childKeyrings: KeyringList
Expand Down Expand Up @@ -1825,6 +1862,41 @@ include "../../StandardLibrary/src/Index.dfy"
History.CreateDefaultCryptographicMaterialsManager := History.CreateDefaultCryptographicMaterialsManager + [DafnyCallEvent(input, output)];
}

predicate CreateExpectedEncryptionContextCMMEnsuresPublicly(input: CreateExpectedEncryptionContextCMMInput , output: Result<ICryptographicMaterialsManager, Error>)
{Operations.CreateExpectedEncryptionContextCMMEnsuresPublicly(input, output)}
// The public method to be called by library consumers
method CreateExpectedEncryptionContextCMM ( input: CreateExpectedEncryptionContextCMMInput )
returns (output: Result<ICryptographicMaterialsManager, Error>)
requires
&& ValidState() && ( input.underlyingCMM.Some? ==>
&& input.underlyingCMM.value.ValidState()
&& input.underlyingCMM.value.Modifies !! {History}
) && ( input.keyring.Some? ==>
&& input.keyring.value.ValidState()
&& input.keyring.value.Modifies !! {History}
)
modifies Modifies - {History} ,
(if input.underlyingCMM.Some? then input.underlyingCMM.value.Modifies else {}) ,
(if input.keyring.Some? then input.keyring.value.Modifies else {}) ,
History`CreateExpectedEncryptionContextCMM
// Dafny will skip type parameters when generating a default decreases clause.
decreases Modifies - {History} ,
(if input.underlyingCMM.Some? then input.underlyingCMM.value.Modifies else {}) ,
(if input.keyring.Some? then input.keyring.value.Modifies else {})
ensures
&& ValidState()
&& ( output.Success? ==>
&& output.value.ValidState()
&& output.value.Modifies !! {History}
&& fresh(output.value)
&& fresh ( output.value.Modifies - Modifies - {History} - (if input.underlyingCMM.Some? then input.underlyingCMM.value.Modifies else {}) - (if input.keyring.Some? then input.keyring.value.Modifies else {}) ) )
ensures CreateExpectedEncryptionContextCMMEnsuresPublicly(input, output)
ensures History.CreateExpectedEncryptionContextCMM == old(History.CreateExpectedEncryptionContextCMM) + [DafnyCallEvent(input, output)]
{
output := Operations.CreateExpectedEncryptionContextCMM(config, input);
History.CreateExpectedEncryptionContextCMM := History.CreateExpectedEncryptionContextCMM + [DafnyCallEvent(input, output)];
}

predicate CreateCryptographicMaterialsCacheEnsuresPublicly(input: CreateCryptographicMaterialsCacheInput , output: Result<ICryptographicMaterialsCache, Error>)
{Operations.CreateCryptographicMaterialsCacheEnsuresPublicly(input, output)}
// The public method to be called by library consumers
Expand Down Expand Up @@ -2304,6 +2376,34 @@ include "../../StandardLibrary/src/Index.dfy"
ensures CreateDefaultCryptographicMaterialsManagerEnsuresPublicly(input, output)


predicate CreateExpectedEncryptionContextCMMEnsuresPublicly(input: CreateExpectedEncryptionContextCMMInput , output: Result<ICryptographicMaterialsManager, Error>)
// The private method to be refined by the library developer


method CreateExpectedEncryptionContextCMM ( config: InternalConfig , input: CreateExpectedEncryptionContextCMMInput )
returns (output: Result<ICryptographicMaterialsManager, Error>)
requires
&& ValidInternalConfig?(config) && ( input.underlyingCMM.Some? ==>
&& input.underlyingCMM.value.ValidState()
) && ( input.keyring.Some? ==>
&& input.keyring.value.ValidState()
)
modifies ModifiesInternalConfig(config) ,
(if input.underlyingCMM.Some? then input.underlyingCMM.value.Modifies else {}) ,
(if input.keyring.Some? then input.keyring.value.Modifies else {})
// Dafny will skip type parameters when generating a default decreases clause.
decreases ModifiesInternalConfig(config) ,
(if input.underlyingCMM.Some? then input.underlyingCMM.value.Modifies else {}) ,
(if input.keyring.Some? then input.keyring.value.Modifies else {})
ensures
&& ValidInternalConfig?(config)
&& ( output.Success? ==>
&& output.value.ValidState()
&& fresh(output.value)
&& fresh ( output.value.Modifies - ModifiesInternalConfig(config) - (if input.underlyingCMM.Some? then input.underlyingCMM.value.Modifies else {}) - (if input.keyring.Some? then input.keyring.value.Modifies else {}) ) )
ensures CreateExpectedEncryptionContextCMMEnsuresPublicly(input, output)


predicate CreateCryptographicMaterialsCacheEnsuresPublicly(input: CreateCryptographicMaterialsCacheInput , output: Result<ICryptographicMaterialsCache, Error>)
// The private method to be refined by the library developer

Expand Down
18 changes: 18 additions & 0 deletions AwsCryptographicMaterialProviders/Model/cmms.smithy
Original file line number Diff line number Diff line change
Expand Up @@ -131,3 +131,21 @@ structure CreateDefaultCryptographicMaterialsManagerInput {
@required
keyring: KeyringReference
}

@positional
structure CreateExpectedEncryptionContextCMMOutput {
@required
materialsManager: CryptographicMaterialsManagerReference
}

operation CreateExpectedEncryptionContextCMM {
input: CreateExpectedEncryptionContextCMMInput,
output: CreateExpectedEncryptionContextCMMOutput,
}

structure CreateExpectedEncryptionContextCMMInput {
underlyingCMM: CryptographicMaterialsManagerReference,
keyring: KeyringReference,
@required
requiredEncryptionContextKeys: EncryptionContextKeys
}
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@ service AwsCryptographicMaterialProviders {

// CMMs
CreateDefaultCryptographicMaterialsManager,
CreateExpectedEncryptionContextCMM,

// CMCs
CreateCryptographicMaterialsCache,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@
import software.amazon.cryptography.materialProviders.model.CreateCryptographicMaterialsCacheInput;
import software.amazon.cryptography.materialProviders.model.CreateDefaultClientSupplierInput;
import software.amazon.cryptography.materialProviders.model.CreateDefaultCryptographicMaterialsManagerInput;
import software.amazon.cryptography.materialProviders.model.CreateExpectedEncryptionContextCMMInput;
import software.amazon.cryptography.materialProviders.model.CreateMultiKeyringInput;
import software.amazon.cryptography.materialProviders.model.CreateRawAesKeyringInput;
import software.amazon.cryptography.materialProviders.model.CreateRawRsaKeyringInput;
Expand Down Expand Up @@ -234,6 +235,16 @@ public ICryptographicMaterialsManager CreateDefaultCryptographicMaterialsManager
return CryptographicMaterialsManager.wrap(result.dtor_value());
}

public ICryptographicMaterialsManager CreateExpectedEncryptionContextCMM(
CreateExpectedEncryptionContextCMMInput nativeValue) {
Dafny.Aws.Cryptography.MaterialProviders.Types.CreateExpectedEncryptionContextCMMInput dafnyValue = ToDafny.CreateExpectedEncryptionContextCMMInput(nativeValue);
Result<Dafny.Aws.Cryptography.MaterialProviders.Types.ICryptographicMaterialsManager, Error> result = this._impl.CreateExpectedEncryptionContextCMM(dafnyValue);
if (result.is_Failure()) {
throw ToNative.Error(result.dtor_error());
}
return CryptographicMaterialsManager.wrap(result.dtor_value());
}

public ICryptographicMaterialsCache CreateCryptographicMaterialsCache(
CreateCryptographicMaterialsCacheInput nativeValue) {
Dafny.Aws.Cryptography.MaterialProviders.Types.CreateCryptographicMaterialsCacheInput dafnyValue = ToDafny.CreateCryptographicMaterialsCacheInput(nativeValue);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@
import Dafny.Aws.Cryptography.MaterialProviders.Types.CreateCryptographicMaterialsCacheInput;
import Dafny.Aws.Cryptography.MaterialProviders.Types.CreateDefaultClientSupplierInput;
import Dafny.Aws.Cryptography.MaterialProviders.Types.CreateDefaultCryptographicMaterialsManagerInput;
import Dafny.Aws.Cryptography.MaterialProviders.Types.CreateExpectedEncryptionContextCMMInput;
import Dafny.Aws.Cryptography.MaterialProviders.Types.CreateMultiKeyringInput;
import Dafny.Aws.Cryptography.MaterialProviders.Types.CreateRawAesKeyringInput;
import Dafny.Aws.Cryptography.MaterialProviders.Types.CreateRawRsaKeyringInput;
Expand Down Expand Up @@ -610,6 +611,21 @@ public static GetEncryptionMaterialsInput GetEncryptionMaterialsInput(
return new GetEncryptionMaterialsInput(encryptionContext, commitmentPolicy, algorithmSuiteId, maxPlaintextLength, requiredEncryptionContextKeys);
}

public static CreateExpectedEncryptionContextCMMInput CreateExpectedEncryptionContextCMMInput(
software.amazon.cryptography.materialProviders.model.CreateExpectedEncryptionContextCMMInput nativeValue) {
Option<Dafny.Aws.Cryptography.MaterialProviders.Types.ICryptographicMaterialsManager> underlyingCMM;
underlyingCMM = Objects.nonNull(nativeValue.underlyingCMM()) ?
Option.create_Some(ToDafny.CryptographicMaterialsManager(nativeValue.underlyingCMM()))
: Option.create_None();
Option<Dafny.Aws.Cryptography.MaterialProviders.Types.IKeyring> keyring;
keyring = Objects.nonNull(nativeValue.keyring()) ?
Option.create_Some(ToDafny.Keyring(nativeValue.keyring()))
: Option.create_None();
DafnySequence<? extends DafnySequence<? extends Byte>> requiredEncryptionContextKeys;
requiredEncryptionContextKeys = ToDafny.EncryptionContextKeys(nativeValue.requiredEncryptionContextKeys());
return new CreateExpectedEncryptionContextCMMInput(underlyingCMM, keyring, requiredEncryptionContextKeys);
}

public static InitializeDecryptionMaterialsInput InitializeDecryptionMaterialsInput(
software.amazon.cryptography.materialProviders.model.InitializeDecryptionMaterialsInput nativeValue) {
AlgorithmSuiteId algorithmSuiteId;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,7 @@
import software.amazon.cryptography.materialProviders.model.CreateCryptographicMaterialsCacheInput;
import software.amazon.cryptography.materialProviders.model.CreateDefaultClientSupplierInput;
import software.amazon.cryptography.materialProviders.model.CreateDefaultCryptographicMaterialsManagerInput;
import software.amazon.cryptography.materialProviders.model.CreateExpectedEncryptionContextCMMInput;
import software.amazon.cryptography.materialProviders.model.CreateMultiKeyringInput;
import software.amazon.cryptography.materialProviders.model.CreateRawAesKeyringInput;
import software.amazon.cryptography.materialProviders.model.CreateRawRsaKeyringInput;
Expand Down Expand Up @@ -606,6 +607,19 @@ public static GetEncryptionMaterialsInput GetEncryptionMaterialsInput(
return nativeBuilder.build();
}

public static CreateExpectedEncryptionContextCMMInput CreateExpectedEncryptionContextCMMInput(
Dafny.Aws.Cryptography.MaterialProviders.Types.CreateExpectedEncryptionContextCMMInput dafnyValue) {
CreateExpectedEncryptionContextCMMInput.Builder nativeBuilder = CreateExpectedEncryptionContextCMMInput.builder();
if (dafnyValue.dtor_underlyingCMM().is_Some()) {
nativeBuilder.underlyingCMM(ToNative.CryptographicMaterialsManager(dafnyValue.dtor_underlyingCMM().dtor_value()));
}
if (dafnyValue.dtor_keyring().is_Some()) {
nativeBuilder.keyring(ToNative.Keyring(dafnyValue.dtor_keyring().dtor_value()));
}
nativeBuilder.requiredEncryptionContextKeys(ToNative.EncryptionContextKeys(dafnyValue.dtor_requiredEncryptionContextKeys()));
return nativeBuilder.build();
}

public static InitializeDecryptionMaterialsInput InitializeDecryptionMaterialsInput(
Dafny.Aws.Cryptography.MaterialProviders.Types.InitializeDecryptionMaterialsInput dafnyValue) {
InitializeDecryptionMaterialsInput.Builder nativeBuilder = InitializeDecryptionMaterialsInput.builder();
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,112 @@
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0
// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
package software.amazon.cryptography.materialProviders.model;

import java.util.List;
import java.util.Objects;
import software.amazon.cryptography.materialProviders.CryptographicMaterialsManager;
import software.amazon.cryptography.materialProviders.ICryptographicMaterialsManager;
import software.amazon.cryptography.materialProviders.IKeyring;
import software.amazon.cryptography.materialProviders.Keyring;

public class CreateExpectedEncryptionContextCMMInput {
private final CryptographicMaterialsManager underlyingCMM;

private final Keyring keyring;

private final List<String> requiredEncryptionContextKeys;

protected CreateExpectedEncryptionContextCMMInput(BuilderImpl builder) {
this.underlyingCMM = builder.underlyingCMM();
this.keyring = builder.keyring();
this.requiredEncryptionContextKeys = builder.requiredEncryptionContextKeys();
}

public CryptographicMaterialsManager underlyingCMM() {
return this.underlyingCMM;
}

public Keyring keyring() {
return this.keyring;
}

public List<String> requiredEncryptionContextKeys() {
return this.requiredEncryptionContextKeys;
}

public Builder toBuilder() {
return new BuilderImpl(this);
}

public static Builder builder() {
return new BuilderImpl();
}

public interface Builder {
Builder underlyingCMM(ICryptographicMaterialsManager underlyingCMM);

CryptographicMaterialsManager underlyingCMM();

Builder keyring(IKeyring keyring);

Keyring keyring();

Builder requiredEncryptionContextKeys(List<String> requiredEncryptionContextKeys);

List<String> requiredEncryptionContextKeys();

CreateExpectedEncryptionContextCMMInput build();
}

static class BuilderImpl implements Builder {
protected CryptographicMaterialsManager underlyingCMM;

protected Keyring keyring;

protected List<String> requiredEncryptionContextKeys;

protected BuilderImpl() {
}

protected BuilderImpl(CreateExpectedEncryptionContextCMMInput model) {
this.underlyingCMM = model.underlyingCMM();
this.keyring = model.keyring();
this.requiredEncryptionContextKeys = model.requiredEncryptionContextKeys();
}

public Builder underlyingCMM(ICryptographicMaterialsManager underlyingCMM) {
this.underlyingCMM = CryptographicMaterialsManager.wrap(underlyingCMM);
return this;
}

public CryptographicMaterialsManager underlyingCMM() {
return this.underlyingCMM;
}

public Builder keyring(IKeyring keyring) {
this.keyring = Keyring.wrap(keyring);
return this;
}

public Keyring keyring() {
return this.keyring;
}

public Builder requiredEncryptionContextKeys(List<String> requiredEncryptionContextKeys) {
this.requiredEncryptionContextKeys = requiredEncryptionContextKeys;
return this;
}

public List<String> requiredEncryptionContextKeys() {
return this.requiredEncryptionContextKeys;
}

public CreateExpectedEncryptionContextCMMInput build() {
if (Objects.isNull(this.requiredEncryptionContextKeys())) {
throw new IllegalArgumentException("Missing value for required field `requiredEncryptionContextKeys`");
}
return new CreateExpectedEncryptionContextCMMInput(this);
}
}
}
Loading

0 comments on commit 1ddbb7e

Please sign in to comment.