Skip to content

Commit 832b391

Browse files
rishav-karanjitrishav-karanjit
committed
Added precontition for the proof and added few comments
1 parent 0f80010 commit 832b391

File tree

146 files changed

+8854
-11238
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

146 files changed

+8854
-11238
lines changed

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy

+26-8
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt
99
import UUID
1010
import AlgorithmSuites
1111
import DynamoToStruct
12+
import opened DynamoDbEncryptionUtil
1213

1314
import Header = StructuredEncryptionHeader
1415

@@ -48,8 +49,12 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt
4849
ensures output.Success? ==> (
4950
match input.input {
5051
case plaintextItem(item) =>
51-
"aws_dbe_head" in DynamoToStruct.ItemToStructured(item).Extract().Keys
52-
&& Header.PartialDeserialize(DynamoToStruct.ItemToStructured(item).Extract()["aws_dbe_head"].content.Terminal.value).Success?
52+
DynamoToStruct.ItemToStructured(item).Success?
53+
&& var extracted := DynamoToStruct.ItemToStructured(item).Extract();
54+
&& var keys := extracted.Keys;
55+
&& "aws_dbe_head" in DynamoToStruct.ItemToStructured(item).Extract()
56+
&& var header := DynamoToStruct.ItemToStructured(item).Extract()["aws_dbe_head"].content.Terminal.value;
57+
&& Header.PartialDeserialize(header).Success?
5358
case header(header) =>
5459
Header.PartialDeserialize(header).Success?
5560
}
@@ -59,16 +64,18 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt
5964
match input.input
6065
{
6166
case plaintextItem(plaintextItem) =>{
67+
:- Need(DynamoToStruct.ItemToStructured(plaintextItem).Success?, E("error"));
68+
:- Need("aws_dbe_head" in DynamoToStruct.ItemToStructured(plaintextItem).Extract(), E("error"));
6269
header := DynamoToStruct.ItemToStructured(plaintextItem).Extract()["aws_dbe_head"].content.Terminal.value;
6370
}
64-
case header(headeritem) => {
71+
case header(headeritem) =>
6572
header := headeritem;
66-
}
6773
}
74+
:- Need(Header.PartialDeserialize(header).Success?, E("error"));
6875
var deserializedHeader := Header.PartialDeserialize(header);
69-
print deserializedHeader;
7076

7177
var algorithmSuite;
78+
7279
if deserializedHeader.Extract().flavor == 0{
7380
algorithmSuite := AlgorithmSuites.DBE_ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_SYMSIG_HMAC_SHA384;
7481
}
@@ -77,18 +84,29 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt
7784
}
7885

7986
var datakeys := deserializedHeader.Extract().dataKeys;
80-
var list : EncryptedDataKeyDescriptionList;
87+
var list : EncryptedDataKeyDescriptionList := [];
8188
for i := 0 to |datakeys| {
8289
var singleDataKeyOutput : EncryptedDataKeyDescriptionOutput;
90+
91+
:- Need(UTF8.Decode(datakeys[i].keyProviderId).Success?, E("error"));
92+
:- Need(UTF8.Decode(datakeys[i].keyProviderInfo).Success?, E("error"));
8393
if UTF8.Decode(datakeys[i].keyProviderId).Extract() == "aws-kms-hierarchy" {
84-
94+
:- Need(EdkWrapping.GetProviderWrappedMaterial(datakeys[i].ciphertext, algorithmSuite).Success?, E("error"));
95+
8596
var providerWrappedMaterial := EdkWrapping.GetProviderWrappedMaterial(datakeys[i].ciphertext, algorithmSuite).Extract();
8697

98+
// The ciphertext structure in the hierarchy keyring contains Salt and IV before Version.
99+
// The length of Salt is 16 and IV is 12 bytes.
100+
// https://github.com/awslabs/aws-encryption-sdk-specification/blob/master/framework/aws-kms/aws-kms-hierarchical-keyring.md#ciphertext
101+
87102
var EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX := 12 + 16;
88103
var EDK_CIPHERTEXT_VERSION_INDEX := EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX + 16;
89104

105+
:- Need(EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX < EDK_CIPHERTEXT_VERSION_INDEX, E("error"));
106+
:- Need(|providerWrappedMaterial| >= EDK_CIPHERTEXT_VERSION_INDEX, E("error"));
90107
var branchKeyVersionUuid := providerWrappedMaterial[EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX .. EDK_CIPHERTEXT_VERSION_INDEX];
91-
108+
:- Need(UUID.FromByteArray(branchKeyVersionUuid).Success?, E("error"));
109+
92110
singleDataKeyOutput := EncryptedDataKeyDescriptionOutput(
93111
keyProviderId := UTF8.Decode(datakeys[i].keyProviderId).Extract(),
94112
keyProviderInfo := UTF8.Decode(datakeys[i].keyProviderInfo).Extract(),

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy

-1
Original file line numberDiff line numberDiff line change
@@ -741,7 +741,6 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
741741
function method DefaultDynamoDbTablesEncryptionConfig(): AwsCryptographyDbEncryptionSdkDynamoDbTypes.DynamoDbTablesEncryptionConfig
742742
method DynamoDbEncryptionTransforms(config: AwsCryptographyDbEncryptionSdkDynamoDbTypes.DynamoDbTablesEncryptionConfig := DefaultDynamoDbTablesEncryptionConfig())
743743
returns (res: Result<IDynamoDbEncryptionTransformsClient, Error>)
744-
// BEGIN MANUAL EDIT
745744
requires var tmps0 := set t0 | t0 in config.tableEncryptionConfigs.Values;
746745
forall tmp0 :: tmp0 in tmps0 ==>
747746
tmp0.keyring.Some? ==>

‎DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy

+18-1
Original file line numberDiff line numberDiff line change
@@ -2,11 +2,15 @@
22
// SPDX-License-Identifier: Apache-2.0
33
include "../../DynamoDbEncryption/src/Index.dfy"
44
include "../../DynamoDbEncryptionTransforms/test/TestFixtures.dfy"
5-
5+
include "../../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EdkWrapping.dfy"
6+
include "../../../../submodules/MaterialProviders/StandardLibrary/src/UUID.dfy"
67
module DynamoDbItemEncryptorTest {
78
import opened Wrappers
89
import opened StandardLibrary.UInt
910
import opened DynamoDbItemEncryptorUtil
11+
import StructuredEncryptionHeader
12+
import EdkWrapping
13+
import UUID
1014
import MaterialProviders
1115
import DynamoDbItemEncryptor
1216
import AwsCryptographyMaterialProvidersTypes
@@ -442,6 +446,19 @@ module DynamoDbItemEncryptorTest {
442446

443447
var parsedHeader := decryptRes.value.parsedHeader;
444448
expect parsedHeader.Some?;
449+
// parsedHeader.value.getSomething();
450+
print "\n\n",UTF8.Decode(parsedHeader.value.encryptedDataKeys[0].keyProviderId).Extract();
451+
print "\n\n",UTF8.Decode(parsedHeader.value.encryptedDataKeys[0].keyProviderInfo).Extract();
452+
print "\n\n",parsedHeader.value.encryptedDataKeys[0].ciphertext;
453+
var providerWrappedMaterial := EdkWrapping.GetProviderWrappedMaterial(parsedHeader.value.encryptedDataKeys[0].ciphertext, AlgorithmSuites.DBE_ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384).Extract();
454+
455+
var EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX := 12 + 16;
456+
var EDK_CIPHERTEXT_VERSION_INDEX := EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX + 16;
457+
458+
var branchKeyVersionUuid := providerWrappedMaterial[EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX .. EDK_CIPHERTEXT_VERSION_INDEX];
459+
var version := UUID.FromByteArray(branchKeyVersionUuid).Extract();
460+
461+
print "\n\n",version;
445462
expect parsedHeader.value.algorithmSuiteId == AlgorithmSuites.DBE_ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384.id.DBE;
446463
expect parsedHeader.value.attributeActionsOnEncrypt == TestFixtures.GetSignedAttributeActions();
447464
// Expect the verification key in the context

‎DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy

+3
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,9 @@ module TestHeader {
3333
);
3434
var ser := head.serialize() + head.msgID; // msgID as fake commitment
3535
var orig :- expect PartialDeserialize(ser);
36+
print "\n\n SER: ", ser , "\n\n";
37+
print "\n\n keyProviderId:", Decode(orig.dataKeys[0].keyProviderId).Extract() , "\n\n";
38+
print "\n\n keyProviderId:", orig.dataKeys[0].keyProviderInfo , "\n\n";
3639
expect orig == head;
3740
}
3841

‎DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/DynamoDbEncryption.java

+12
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,8 @@
1212
import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.CreateDynamoDbEncryptionBranchKeyIdSupplierInput;
1313
import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.CreateDynamoDbEncryptionBranchKeyIdSupplierOutput;
1414
import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.DynamoDbEncryptionConfig;
15+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetEncryptedDataKeyDescriptionInput;
16+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetEncryptedDataKeyDescriptionOutput;
1517

1618
public class DynamoDbEncryption {
1719
private final IDynamoDbEncryptionClient _impl;
@@ -50,6 +52,16 @@ public CreateDynamoDbEncryptionBranchKeyIdSupplierOutput CreateDynamoDbEncryptio
5052
return ToNative.CreateDynamoDbEncryptionBranchKeyIdSupplierOutput(result.dtor_value());
5153
}
5254

55+
public GetEncryptedDataKeyDescriptionOutput GetEncryptedDataKeyDescription(
56+
GetEncryptedDataKeyDescriptionInput input) {
57+
software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionInput dafnyValue = ToDafny.GetEncryptedDataKeyDescriptionInput(input);
58+
Result<software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionOutput, Error> result = this._impl.GetEncryptedDataKeyDescription(dafnyValue);
59+
if (result.is_Failure()) {
60+
throw ToNative.Error(result.dtor_error());
61+
}
62+
return ToNative.GetEncryptedDataKeyDescriptionOutput(result.dtor_value());
63+
}
64+
5365
protected IDynamoDbEncryptionClient impl() {
5466
return this._impl;
5567
}

‎DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java

+54
Original file line numberDiff line numberDiff line change
@@ -27,11 +27,15 @@
2727
import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.DynamoDbEncryptionConfig;
2828
import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.DynamoDbTableEncryptionConfig;
2929
import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.DynamoDbTablesEncryptionConfig;
30+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.EncryptedDataKeyDescriptionOutput;
3031
import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.EncryptedPart;
3132
import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.Error;
3233
import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.Error_DynamoDbEncryptionException;
3334
import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetBranchKeyIdFromDdbKeyInput;
3435
import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetBranchKeyIdFromDdbKeyOutput;
36+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionInput;
37+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionOutput;
38+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionUnion;
3539
import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetPrefix;
3640
import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetSegment;
3741
import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetSegments;
@@ -238,6 +242,23 @@ public static DynamoDbTablesEncryptionConfig DynamoDbTablesEncryptionConfig(
238242
return new DynamoDbTablesEncryptionConfig(tableEncryptionConfigs);
239243
}
240244

245+
public static EncryptedDataKeyDescriptionOutput EncryptedDataKeyDescriptionOutput(
246+
software.amazon.cryptography.dbencryptionsdk.dynamodb.model.EncryptedDataKeyDescriptionOutput nativeValue) {
247+
DafnySequence<? extends Character> keyProviderId;
248+
keyProviderId = software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(nativeValue.keyProviderId());
249+
DafnySequence<? extends Character> keyProviderInfo;
250+
keyProviderInfo = software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(nativeValue.keyProviderInfo());
251+
Option<DafnySequence<? extends Character>> branchKeyId;
252+
branchKeyId = Objects.nonNull(nativeValue.branchKeyId()) ?
253+
Option.create_Some(software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(nativeValue.branchKeyId()))
254+
: Option.create_None();
255+
Option<DafnySequence<? extends Character>> branchKeyVersion;
256+
branchKeyVersion = Objects.nonNull(nativeValue.branchKeyVersion()) ?
257+
Option.create_Some(software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(nativeValue.branchKeyVersion()))
258+
: Option.create_None();
259+
return new EncryptedDataKeyDescriptionOutput(keyProviderId, keyProviderInfo, branchKeyId, branchKeyVersion);
260+
}
261+
241262
public static EncryptedPart EncryptedPart(
242263
software.amazon.cryptography.dbencryptionsdk.dynamodb.model.EncryptedPart nativeValue) {
243264
DafnySequence<? extends Character> name;
@@ -261,6 +282,20 @@ public static GetBranchKeyIdFromDdbKeyOutput GetBranchKeyIdFromDdbKeyOutput(
261282
return new GetBranchKeyIdFromDdbKeyOutput(branchKeyId);
262283
}
263284

285+
public static GetEncryptedDataKeyDescriptionInput GetEncryptedDataKeyDescriptionInput(
286+
software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetEncryptedDataKeyDescriptionInput nativeValue) {
287+
GetEncryptedDataKeyDescriptionUnion input;
288+
input = ToDafny.GetEncryptedDataKeyDescriptionUnion(nativeValue.input());
289+
return new GetEncryptedDataKeyDescriptionInput(input);
290+
}
291+
292+
public static GetEncryptedDataKeyDescriptionOutput GetEncryptedDataKeyDescriptionOutput(
293+
software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetEncryptedDataKeyDescriptionOutput nativeValue) {
294+
DafnySequence<? extends EncryptedDataKeyDescriptionOutput> encryptedDataKeyDescriptionOutput;
295+
encryptedDataKeyDescriptionOutput = ToDafny.EncryptedDataKeyDescriptionList(nativeValue.EncryptedDataKeyDescriptionOutput());
296+
return new GetEncryptedDataKeyDescriptionOutput(encryptedDataKeyDescriptionOutput);
297+
}
298+
264299
public static GetPrefix GetPrefix(
265300
software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetPrefix nativeValue) {
266301
Integer length;
@@ -506,6 +541,17 @@ public static BeaconStyle BeaconStyle(
506541
throw new IllegalArgumentException("Cannot convert " + nativeValue + " to software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconStyle.");
507542
}
508543

544+
public static GetEncryptedDataKeyDescriptionUnion GetEncryptedDataKeyDescriptionUnion(
545+
software.amazon.cryptography.dbencryptionsdk.dynamodb.model.GetEncryptedDataKeyDescriptionUnion nativeValue) {
546+
if (Objects.nonNull(nativeValue.header())) {
547+
return GetEncryptedDataKeyDescriptionUnion.create_header(software.amazon.smithy.dafny.conversion.ToDafny.Simple.ByteSequence(nativeValue.header()));
548+
}
549+
if (Objects.nonNull(nativeValue.plaintextItem())) {
550+
return GetEncryptedDataKeyDescriptionUnion.create_plaintextItem(software.amazon.cryptography.services.dynamodb.internaldafny.ToDafny.AttributeMap(nativeValue.plaintextItem()));
551+
}
552+
throw new IllegalArgumentException("Cannot convert " + nativeValue + " to software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetEncryptedDataKeyDescriptionUnion.");
553+
}
554+
509555
public static VirtualTransform VirtualTransform(
510556
software.amazon.cryptography.dbencryptionsdk.dynamodb.model.VirtualTransform nativeValue) {
511557
if (Objects.nonNull(nativeValue.upper())) {
@@ -567,6 +613,14 @@ public static DafnySequence<? extends ConstructorPart> ConstructorPartList(
567613
ConstructorPart._typeDescriptor());
568614
}
569615

616+
public static DafnySequence<? extends EncryptedDataKeyDescriptionOutput> EncryptedDataKeyDescriptionList(
617+
List<software.amazon.cryptography.dbencryptionsdk.dynamodb.model.EncryptedDataKeyDescriptionOutput> nativeValue) {
618+
return software.amazon.smithy.dafny.conversion.ToDafny.Aggregate.GenericToSequence(
619+
nativeValue,
620+
software.amazon.cryptography.dbencryptionsdk.dynamodb.ToDafny::EncryptedDataKeyDescriptionOutput,
621+
EncryptedDataKeyDescriptionOutput._typeDescriptor());
622+
}
623+
570624
public static DafnySequence<? extends EncryptedPart> EncryptedPartsList(
571625
List<software.amazon.cryptography.dbencryptionsdk.dynamodb.model.EncryptedPart> nativeValue) {
572626
return software.amazon.smithy.dafny.conversion.ToDafny.Aggregate.GenericToSequence(

0 commit comments

Comments
 (0)