Skip to content

chore(TestVectors): Test Smithy-generated ItemEncryptor #1814

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

Draft
wants to merge 34 commits into
base: main
Choose a base branch
from
Draft
41 changes: 40 additions & 1 deletion TestVectors/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -7,14 +7,17 @@ TRANSPILE_TESTS_IN_RUST=1
include ../SharedMakefile.mk

PROJECT_SERVICES := \
DDBEncryption
DDBEncryption \
WrappedDynamoDbItemEncryptor

MAIN_SERVICE_FOR_RUST := DDBEncryption

SMITHY_MODEL_ROOT := $(PROJECT_ROOT)/DynamoDbEncryption/dafny/DynamoDbEncryption/Model
OUTPUT_LOCAL_SERVICE_DDBEncryption := --local-service-test
OUTPUT_LOCAL_SERVICE_WrappedDynamoDbItemEncryptor := --local-service-test

SERVICE_NAMESPACE_DDBEncryption=aws.cryptography.dbEncryptionSdk.dynamoDb
SERVICE_NAMESPACE_WrappedDynamoDbItemEncryptor=aws.cryptography.dbEncryptionSdk.dynamoDb.itemEncryptor

MAX_RESOURCE_COUNT=10000000
# Order is important
Expand All @@ -35,6 +38,7 @@ RUST_OTHER_FILES := \
runtimes/rust/src/ddb.rs \
runtimes/rust/src/concurrent_call.rs \
runtimes/rust/src/create_client.rs \
runtimes/rust/src/create_wrapped_item_encryptor.rs \
runtimes/rust/src/dafny_libraries.rs \
runtimes/rust/src/digest.rs \
runtimes/rust/src/ecdh.rs \
Expand Down Expand Up @@ -66,6 +70,8 @@ PROJECT_INDEX := \
DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy \
DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy \
DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy \
DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy \
DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy \

STD_LIBRARY=submodules/MaterialProviders/StandardLibrary
SMITHY_DEPS=submodules/MaterialProviders/model
Expand All @@ -85,8 +91,41 @@ SERVICE_DEPS_DDBEncryption := \
DynamoDbEncryption/dafny/StructuredEncryption \
submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders \

SERVICE_DEPS_WrappedDynamoDbItemEncryptor := \
submodules/MaterialProviders/AwsCryptographyPrimitives \
submodules/MaterialProviders/ComAmazonawsKms \
submodules/MaterialProviders/ComAmazonawsDynamodb \
submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders \
submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore \
DynamoDbEncryption/dafny/StructuredEncryption \
DynamoDbEncryption/dafny/DynamoDbEncryption \
DynamoDbEncryption/dafny/DynamoDbItemEncryptor \
submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders \

transpile_implementation_rust: _remove_wrapped_client_rust

_remove_wrapped_client_rust:
$(MAKE) _sed_file SED_FILE_PATH="runtimes/rust/src/deps/aws_cryptography_materialProviders.rs" \
SED_BEFORE_STRING=' \#\[cfg(feature = "wrapped-client")\]' SED_AFTER_STRING='\/\/ Removed cfg(feature = "wrapped-client")'

REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_PRIMITIVES=runtimes/rust/src/deps/aws_cryptography_primitives.rs
REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_KEYSTORE=runtimes/rust/src/deps/aws_cryptography_keyStore.rs
REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_DYNAMODB=runtimes/rust/src/deps/aws_cryptography_dbEncryptionSdk_dynamoDb_transforms.rs
REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_DYNAMODB_ITEM_ENCRYPTOR=runtimes/rust/src/deps/aws_cryptography_dbEncryptionSdk_dynamoDb_itemEncryptor.rs
REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_DYNAMODB_STRUCTURED_ENCRYPTION=runtimes/rust/src/deps/aws_cryptography_dbEncryptionSdk_structuredEncryption.rs
REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_1 = "\#\[cfg(feature = \"wrapped-client\")\]"
REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_2 := 'pub mod wrapped;'
REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1 := '\/\/ removed wrapped-client feature using sed;'
REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_2 := '\/\/ removed wrapped module using sed;'

_polymorph_rust: _remove_wrapped_client_rust

_remove_wrapped_client_rust:
$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_PRIMITIVES) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_1) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1)
$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_PRIMITIVES) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_2) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_2)
$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_KEYSTORE) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_1) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1)
$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_KEYSTORE) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_2) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_2)
$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_DYNAMODB) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_1) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1)
$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_DYNAMODB) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_2) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_2)
$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_DYNAMODB_STRUCTURED_ENCRYPTION) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_1) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1)
$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_DYNAMODB_STRUCTURED_ENCRYPTION) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_2) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_2)
Original file line number Diff line number Diff line change
@@ -0,0 +1,50 @@
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0

include "../Model/AwsCryptographyDynamoDbEncryptionTypesWrapped.dfy"
include "../../../../DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy"

module {:extern} CreateWrappedItemEncryptor {
import opened Wrappers
import AwsCryptographyDbEncryptionSdkDynamoDbTypes
import ENC = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
import DynamoDbItemEncryptor
import Operations = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations

method {:extern} CreateWrappedItemEncryptor(config: ENC.DynamoDbItemEncryptorConfig)
returns (output: Result<ENC.IDynamoDbItemEncryptorClient, ENC.Error>)
ensures output.Success? ==>
&& output.value is DynamoDbItemEncryptor.DynamoDbItemEncryptorClient
&& fresh(output.value)
&& fresh(output.value.History)
&& output.value.ValidState()
&& var rconfig := (output.value as DynamoDbItemEncryptor.DynamoDbItemEncryptorClient).config;
&& fresh(output.value.Modifies)
&& rconfig.logicalTableName == config.logicalTableName
&& rconfig.partitionKeyName == config.partitionKeyName
&& rconfig.sortKeyName == config.sortKeyName
&& rconfig.attributeActionsOnEncrypt == config.attributeActionsOnEncrypt
&& rconfig.allowedUnsignedAttributes == config.allowedUnsignedAttributes
&& rconfig.allowedUnsignedAttributePrefix == config.allowedUnsignedAttributePrefix
&& rconfig.algorithmSuiteId == config.algorithmSuiteId

//= specification/dynamodb-encryption-client/ddb-table-encryption-config.md#attribute-actions
//= type=implication
//# The [Key Action](#key-action)
//# MUST be configured to the partition attribute and, if present, sort attribute.
&& rconfig.version == Operations.VersionFromActions(config.attributeActionsOnEncrypt)
&& config.partitionKeyName in config.attributeActionsOnEncrypt
&& config.attributeActionsOnEncrypt[config.partitionKeyName] == Operations.KeyActionFromVersion(rconfig.version)
&& (config.sortKeyName.Some? ==>
&& config.sortKeyName.value in config.attributeActionsOnEncrypt
&& config.attributeActionsOnEncrypt[config.sortKeyName.value] == Operations.KeyActionFromVersion(rconfig.version))

//= specification/dynamodb-encryption-client/ddb-table-encryption-config.md#plaintext-policy
//# If not specified, encryption and decryption MUST behave according to `FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ`.
ensures
&& output.Success?
&& config.plaintextOverride.None?
==>
&& var config := (output.value as DynamoDbItemEncryptor.DynamoDbItemEncryptorClient).config;
&& config.plaintextOverride.FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ?
}
2 changes: 2 additions & 0 deletions TestVectors/dafny/DDBEncryption/src/Index.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
include "LibraryIndex.dfy"
include "TestVectors.dfy"
include "WriteSetPermutations.dfy"
include "../../WrappedDynamoDbItemEncryptor/src/Index.dfy"

module WrappedDDBEncryptionMain {
import opened Wrappers
Expand All @@ -16,6 +17,7 @@ module WrappedDDBEncryptionMain {
import opened JSONHelpers
import KeyVectors
import KeyVectorsTypes = AwsCryptographyMaterialProvidersTestVectorKeysTypes
import WrappedItemEncryptor


const DEFAULT_KEYS : string := "../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json"
Expand Down
11 changes: 6 additions & 5 deletions TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@

include "JsonItem.dfy"
include "CreateInterceptedDDBClient.dfy"
include "CreateWrappedItemEncryptor.dfy"
include "../../../../DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy"

module {:options "-functionSyntax:4"} JsonConfig {
Expand Down Expand Up @@ -31,6 +32,8 @@ module {:options "-functionSyntax:4"} JsonConfig {
import ParseJsonManifests
import CreateInterceptedDDBClient
import DynamoDbItemEncryptor
import CreateWrappedItemEncryptor
import Operations = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations


const abc : UTF8.ValidUTF8Bytes :=
Expand Down Expand Up @@ -259,7 +262,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
}

method GetItemEncryptor(name : string, data : JSON, keys: KeyVectors.KeyVectorsClient)
returns (encryptor : Result<DynamoDbItemEncryptor.DynamoDbItemEncryptorClient, string>)
returns (encryptor : Result<ENC.IDynamoDbItemEncryptorClient, string>)
requires keys.ValidState()
modifies keys.Modifies
ensures keys.ValidState()
Expand Down Expand Up @@ -357,10 +360,8 @@ module {:options "-functionSyntax:4"} JsonConfig {
legacyOverride := legacyOverride,
plaintextOverride := plaintextOverride
);
var enc : ENC.IDynamoDbItemEncryptorClient :- expect DynamoDbItemEncryptor.DynamoDbItemEncryptor(encryptorConfig);
assert enc is DynamoDbItemEncryptor.DynamoDbItemEncryptorClient;
var encr := enc as DynamoDbItemEncryptor.DynamoDbItemEncryptorClient;
return Success(encr);
var enc : ENC.IDynamoDbItemEncryptorClient :- expect CreateWrappedItemEncryptor.CreateWrappedItemEncryptor(encryptorConfig);
return Success(enc);
}

method GetOneTableConfig(name : string, data : JSON, keys: KeyVectors.KeyVectorsClient)
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
// 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.
include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
include "../src/Index.dfy"
abstract module WrappedAbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService {
import opened Wrappers
import opened StandardLibrary.UInt
import opened UTF8
import opened Types = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
import WrappedService : AbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService
function method WrappedDefaultDynamoDbItemEncryptorConfig(): DynamoDbItemEncryptorConfig
method {:extern} WrappedDynamoDbItemEncryptor(config: DynamoDbItemEncryptorConfig := WrappedDefaultDynamoDbItemEncryptorConfig())
returns (res: Result<IDynamoDbItemEncryptorClient, Error>)
ensures res.Success? ==>
&& fresh(res.value)
&& fresh(res.value.Modifies)
&& fresh(res.value.History)
&& res.value.ValidState()
}
17 changes: 17 additions & 0 deletions TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0
// Empty stub expected by Smithy-Dafny

include "../../../../DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy"
include "../Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypesWrapped.dfy"
module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.wrapped" } WrappedItemEncryptor refines WrappedAbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService {

import ComAmazonawsDynamodbTypes

import DynamoDbItemEncryptor

function method WrappedDefaultDynamoDbItemEncryptorConfig(): DynamoDbItemEncryptorConfig
{
DynamoDbItemEncryptor.DefaultDynamoDbItemEncryptorConfig()
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
package CreateWrappedItemEncryptor_Compile;

import Wrappers_Compile.Result;
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.DynamoDbItemEncryptor;
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToDafny;
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToNative;
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error;
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.IDynamoDbItemEncryptorClient;
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.model.DynamoDbItemEncryptorConfig;
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.wrapped.TestDynamoDbItemEncryptor;

public class __default {

public static Result<
IDynamoDbItemEncryptorClient,
Error
> CreateWrappedItemEncryptor(
software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DynamoDbItemEncryptorConfig config
) {
try {
final DynamoDbItemEncryptorConfig nativeConfig =
ToNative.DynamoDbItemEncryptorConfig(config);

final DynamoDbItemEncryptor itemEncryptor = DynamoDbItemEncryptor
.builder()
.DynamoDbItemEncryptorConfig(nativeConfig)
.build();

final TestDynamoDbItemEncryptor wrappedEncryptor =
TestDynamoDbItemEncryptor.builder().impl(itemEncryptor).build();

return Result.create_Success(wrappedEncryptor);
} catch (Exception e) {
return Result.create_Failure(ToDafny.Error((RuntimeException) e));
}
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,110 @@
// 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.dbencryptionsdk.dynamodb.itemencryptor.wrapped;

import Wrappers_Compile.Result;
import java.lang.IllegalArgumentException;
import java.lang.RuntimeException;
import java.util.Objects;
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.DynamoDbItemEncryptor;
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToDafny;
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToNative;
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DecryptItemInput;
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DecryptItemOutput;
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.EncryptItemInput;
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.EncryptItemOutput;
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error;
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.IDynamoDbItemEncryptorClient;

public class TestDynamoDbItemEncryptor implements IDynamoDbItemEncryptorClient {

private final DynamoDbItemEncryptor _impl;

protected TestDynamoDbItemEncryptor(BuilderImpl builder) {
this._impl = builder.impl();
}

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

public Result<DecryptItemOutput, Error> DecryptItem(
DecryptItemInput dafnyInput
) {
try {
software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.model.DecryptItemInput nativeInput =
ToNative.DecryptItemInput(dafnyInput);
software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.model.DecryptItemOutput nativeOutput =
this._impl.DecryptItem(nativeInput);
DecryptItemOutput dafnyOutput = ToDafny.DecryptItemOutput(nativeOutput);
return Result.create_Success(
DecryptItemOutput._typeDescriptor(),
Error._typeDescriptor(),
dafnyOutput
);
} catch (RuntimeException ex) {
return Result.create_Failure(
DecryptItemOutput._typeDescriptor(),
Error._typeDescriptor(),
ToDafny.Error(ex)
);
}
}

public Result<EncryptItemOutput, Error> EncryptItem(
EncryptItemInput dafnyInput
) {
try {
software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.model.EncryptItemInput nativeInput =
ToNative.EncryptItemInput(dafnyInput);
software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.model.EncryptItemOutput nativeOutput =
this._impl.EncryptItem(nativeInput);
EncryptItemOutput dafnyOutput = ToDafny.EncryptItemOutput(nativeOutput);
return Result.create_Success(
EncryptItemOutput._typeDescriptor(),
Error._typeDescriptor(),
dafnyOutput
);
} catch (RuntimeException ex) {
return Result.create_Failure(
EncryptItemOutput._typeDescriptor(),
Error._typeDescriptor(),
ToDafny.Error(ex)
);
}
}

public interface Builder {
Builder impl(DynamoDbItemEncryptor impl);

DynamoDbItemEncryptor impl();

TestDynamoDbItemEncryptor build();
}

static class BuilderImpl implements Builder {

protected DynamoDbItemEncryptor impl;

protected BuilderImpl() {}

public Builder impl(DynamoDbItemEncryptor impl) {
this.impl = impl;
return this;
}

public DynamoDbItemEncryptor impl() {
return this.impl;
}

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