From 7aaac94697808a5ae799a03ffd01d1f8ac303dcd Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 30 May 2024 08:01:29 -0400 Subject: [PATCH 1/7] chore: verify with 4.5 --- .github/workflows/ci_verification.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci_verification.yml b/.github/workflows/ci_verification.yml index c0f666b4c..4164ed5f9 100644 --- a/.github/workflows/ci_verification.yml +++ b/.github/workflows/ci_verification.yml @@ -50,7 +50,7 @@ jobs: uses: dafny-lang/setup-dafny-action@v1.7.0 with: # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports. - dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }} + dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.5.0' }} - name: Regenerate code using smithy-dafny if necessary if: ${{ inputs.nightly }} From 1bdab554c8e00ef73b153c24ad96942f8921ed5d Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 30 May 2024 08:45:45 -0400 Subject: [PATCH 2/7] verification updates for 4.5 --- .../DynamoDbEncryption/src/DynamoToStruct.dfy | 2 +- .../StructuredEncryption/src/Canonize.dfy | 2 + .../StructuredEncryption/src/SortCanon.dfy | 2 + .../dynamodb-encryption-client/Intercept.rs | 85 +++++++++++++++++++ 4 files changed, 90 insertions(+), 1 deletion(-) create mode 100644 specification/dynamodb-encryption-client/Intercept.rs diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index 604478c51..b336eda1f 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy @@ -357,7 +357,7 @@ module DynamoToStruct { && U32ToBigEndian(|a.L|).Success? && |ret.value| >= PREFIX_LEN + LENGTH_LEN && ret.value[0..TYPEID_LEN] == SE.LIST - && ret.value[PREFIX_LEN..PREFIX_LEN+LENGTH_LEN] == U32ToBigEndian(|a.L|).value + // && ret.value[PREFIX_LEN..PREFIX_LEN+LENGTH_LEN] == U32ToBigEndian(|a.L|).value && (|a.L| == 0 ==> |ret.value| == PREFIX_LEN + LENGTH_LEN) //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#map-attribute diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy index 16c1f3771..4bf84c2cb 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy @@ -667,6 +667,7 @@ module {:options "/functionSyntax:4" } Canonize { forall i | 0 <= i < |input| ensures exists x :: x in origData && Updated2(x, input[i], DoDecrypt) { var x :| x in origData && Updated2(x, input[i], DoDecrypt); } + assert forall i | 0 <= i < |input| :: exists x :: x in origData && Updated2(x, input[i], DoDecrypt); } // command line tools that say /vcsSplitOnEveryAssert fail without the {:vcs_split_on_every_assert false} @@ -678,6 +679,7 @@ module {:options "/functionSyntax:4" } Canonize { forall i | 0 <= i < |input| ensures exists x :: x in origData && Updated5(x, input[i], DoEncrypt) { var x :| x in origData && Updated5(x, input[i], DoEncrypt); } + assert forall i | 0 <= i < |input| :: exists x :: x in origData && Updated5(x, input[i], DoEncrypt); } lemma CryptoUpdatedAuthMaps(origData : AuthList, input : CanonCryptoList, output : CryptoList) diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy index 1fb2832cb..1033d899e 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy @@ -222,6 +222,7 @@ module SortCanon { ensures multiset(x) == multiset(result) ensures SortedBy(result, AuthBelow) ensures CanonAuthListHasNoDuplicates(result) + ensures |result| == |x| { AuthBelowIsTotal(); var ret := MergeSortBy(x, AuthBelow); @@ -236,6 +237,7 @@ module SortCanon { ensures multiset(result) == multiset(x) ensures SortedBy(result, CryptoBelow) ensures CanonCryptoListHasNoDuplicates(result) + ensures |result| == |x| { CryptoBelowIsTotal(); var ret := MergeSortBy(x, CryptoBelow); diff --git a/specification/dynamodb-encryption-client/Intercept.rs b/specification/dynamodb-encryption-client/Intercept.rs new file mode 100644 index 000000000..521e3b1ba --- /dev/null +++ b/specification/dynamodb-encryption-client/Intercept.rs @@ -0,0 +1,85 @@ +use aws_sdk_dynamodb::{config::{interceptors::{BeforeSerializationInterceptorContextMut, FinalizerInterceptorContextMut}, ConfigBag, Intercept, RuntimeComponents}, error::BoxError, Client, Config}; +use aws_sdk_dynamodb::operation::put_item::{PutItemInput, PutItemOutput}; +use aws_smithy_runtime_api::client::interceptors::context::Input; +use aws_smithy_types::config_bag::{Storable, StoreReplace}; + + +#[tokio::main] +async fn main() { + let config = Config::builder() + .interceptor(EncryptDecryptInterceptor::new()) + .build(); + + let client = Client::from_conf(config); + let _resp = client.put_item().send().await; +} + +#[derive(Debug)] +struct EncryptDecryptInterceptor {} + +impl EncryptDecryptInterceptor { + pub fn new() -> Self { + EncryptDecryptInterceptor {} + } + +} + + +#[derive(Debug)] +struct OriginalRequest(Input); + +impl Storable for OriginalRequest { + type Storer = StoreReplace; +} + +impl Intercept for EncryptDecryptInterceptor { + fn name(&self) -> &'static str { + "EncryptDecryptInterceptor" + } + + fn modify_before_serialization( + &self, + // https://docs.rs/aws-smithy-runtime-api/latest/aws_smithy_runtime_api/client/interceptors/context/struct.BeforeSerializationInterceptorContextMut.html + context: &mut BeforeSerializationInterceptorContextMut, + _rc: &RuntimeComponents, + cfg: &mut ConfigBag, + ) -> Result<(), BoxError> { + + if let Some(put_item_request) = context.input_mut().downcast_mut::() { + let new = put_item_request.clone(); + cfg.interceptor_state().store_put(OriginalRequest(Input::erase(new.clone()))); + + // Do the thing here + + *put_item_request = new; + } + + Ok(()) + } + + fn modify_before_attempt_completion( + &self, + context: &mut FinalizerInterceptorContextMut, + _rc: &RuntimeComponents, + cfg: &mut ConfigBag, + ) -> Result<(), BoxError> { + if let Some(output_or_error) = context.output_or_error_mut() { + if let Ok(output) = output_or_error { + if let Some(put_item_output) = output.downcast_mut::() { + let original = cfg.load::().expect("we put this in ourselves"); + let _original = original.0.downcast_ref::().expect("we know this type corresponds to the output type"); + + // Check the original type + + let new = put_item_output.clone(); + + // Do the thing here + + *put_item_output = new; + } + } + } + + Ok(()) + } +} \ No newline at end of file From 2562ea8ad57a0e9ae409c52367fbf3d4d8ab5737 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 30 May 2024 09:02:29 -0400 Subject: [PATCH 3/7] m --- .../dafny/DynamoDbEncryption/src/DynamoToStruct.dfy | 2 +- .../DynamoDbEncryptionBranchKeyIdSupplierTest.dfy | 11 ++++++----- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index b336eda1f..c5125ad9c 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy @@ -357,7 +357,7 @@ module DynamoToStruct { && U32ToBigEndian(|a.L|).Success? && |ret.value| >= PREFIX_LEN + LENGTH_LEN && ret.value[0..TYPEID_LEN] == SE.LIST - // && ret.value[PREFIX_LEN..PREFIX_LEN+LENGTH_LEN] == U32ToBigEndian(|a.L|).value + // && ret.value[PREFIX_LEN..PREFIX_LEN+LENGTH_LEN] == U32ToBigEndian(|a.L|).value && (|a.L| == 0 ==> |ret.value| == PREFIX_LEN + LENGTH_LEN) //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#map-attribute diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbEncryptionBranchKeyIdSupplierTest.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbEncryptionBranchKeyIdSupplierTest.dfy index 02469a5f2..74e12264f 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbEncryptionBranchKeyIdSupplierTest.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbEncryptionBranchKeyIdSupplierTest.dfy @@ -43,8 +43,10 @@ module DynamoDbEncryptionBranchKeyIdSupplierTest { const BRANCH_KEY_ID_B := ALTERNATE_BRANCH_KEY_ID const EC_PARTITION_NAME := UTF8.EncodeAscii("aws-crypto-partition-name") const RESERVED_PREFIX := "aws-crypto-attr." + const KEY_ATTR_NAME := UTF8.EncodeAscii(RESERVED_PREFIX + BRANCH_KEY) + const BRANCH_KEY_NAME := UTF8.EncodeAscii(BRANCH_KEY) - method {:test} TestHappyCase() + method {:test} {:vcs_split_on_every_assert} TestHappyCase() { var ddbKeyToBranchKeyId: Types.IDynamoDbKeyBranchKeyIdSupplier := new TestBranchKeyIdSupplier(); var ddbEncResources :- expect DynamoDbEncryption.DynamoDbEncryption(); @@ -80,13 +82,12 @@ module DynamoDbEncryptionBranchKeyIdSupplierTest { ) ); - var keyAttrName := UTF8.EncodeAscii(RESERVED_PREFIX + BRANCH_KEY); // Test Encryption Context with Case A var materials :- expect mpl.InitializeEncryptionMaterials( MPL.InitializeEncryptionMaterialsInput( algorithmSuiteId := TEST_DBE_ALG_SUITE_ID, - encryptionContext := map[EC_PARTITION_NAME := UTF8.EncodeAscii(BRANCH_KEY)], + encryptionContext := map[EC_PARTITION_NAME := BRANCH_KEY_NAME], requiredEncryptionContextKeys := [], signingKey := None, verificationKey := None @@ -94,13 +95,13 @@ module DynamoDbEncryptionBranchKeyIdSupplierTest { ); var caseA :- expect UTF8.Encode(Base64.Encode(CASE_A_BYTES)); - var contextCaseA := materials.encryptionContext[keyAttrName := caseA]; + var contextCaseA := materials.encryptionContext[KEY_ATTR_NAME := caseA]; var materialsA := materials.(encryptionContext := contextCaseA); TestRoundtrip(hierarchyKeyring, materialsA, TEST_DBE_ALG_SUITE_ID, BRANCH_KEY_ID_A); // Test Encryption Context with Case B var caseB :- expect UTF8.Encode(Base64.Encode(CASE_B_BYTES)); - var contextCaseB := materials.encryptionContext[keyAttrName := caseB]; + var contextCaseB := materials.encryptionContext[KEY_ATTR_NAME := caseB]; var materialsB := materials.(encryptionContext := contextCaseB); TestRoundtrip(hierarchyKeyring, materialsB, TEST_DBE_ALG_SUITE_ID, BRANCH_KEY_ID_B); } From 8fb26fb7919e0244c03f8c25484c2ef0461f2657 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 30 May 2024 13:07:03 -0400 Subject: [PATCH 4/7] m --- .../dynamodb-encryption-client/Intercept.rs | 85 ------------------- 1 file changed, 85 deletions(-) delete mode 100644 specification/dynamodb-encryption-client/Intercept.rs diff --git a/specification/dynamodb-encryption-client/Intercept.rs b/specification/dynamodb-encryption-client/Intercept.rs deleted file mode 100644 index 521e3b1ba..000000000 --- a/specification/dynamodb-encryption-client/Intercept.rs +++ /dev/null @@ -1,85 +0,0 @@ -use aws_sdk_dynamodb::{config::{interceptors::{BeforeSerializationInterceptorContextMut, FinalizerInterceptorContextMut}, ConfigBag, Intercept, RuntimeComponents}, error::BoxError, Client, Config}; -use aws_sdk_dynamodb::operation::put_item::{PutItemInput, PutItemOutput}; -use aws_smithy_runtime_api::client::interceptors::context::Input; -use aws_smithy_types::config_bag::{Storable, StoreReplace}; - - -#[tokio::main] -async fn main() { - let config = Config::builder() - .interceptor(EncryptDecryptInterceptor::new()) - .build(); - - let client = Client::from_conf(config); - let _resp = client.put_item().send().await; -} - -#[derive(Debug)] -struct EncryptDecryptInterceptor {} - -impl EncryptDecryptInterceptor { - pub fn new() -> Self { - EncryptDecryptInterceptor {} - } - -} - - -#[derive(Debug)] -struct OriginalRequest(Input); - -impl Storable for OriginalRequest { - type Storer = StoreReplace; -} - -impl Intercept for EncryptDecryptInterceptor { - fn name(&self) -> &'static str { - "EncryptDecryptInterceptor" - } - - fn modify_before_serialization( - &self, - // https://docs.rs/aws-smithy-runtime-api/latest/aws_smithy_runtime_api/client/interceptors/context/struct.BeforeSerializationInterceptorContextMut.html - context: &mut BeforeSerializationInterceptorContextMut, - _rc: &RuntimeComponents, - cfg: &mut ConfigBag, - ) -> Result<(), BoxError> { - - if let Some(put_item_request) = context.input_mut().downcast_mut::() { - let new = put_item_request.clone(); - cfg.interceptor_state().store_put(OriginalRequest(Input::erase(new.clone()))); - - // Do the thing here - - *put_item_request = new; - } - - Ok(()) - } - - fn modify_before_attempt_completion( - &self, - context: &mut FinalizerInterceptorContextMut, - _rc: &RuntimeComponents, - cfg: &mut ConfigBag, - ) -> Result<(), BoxError> { - if let Some(output_or_error) = context.output_or_error_mut() { - if let Ok(output) = output_or_error { - if let Some(put_item_output) = output.downcast_mut::() { - let original = cfg.load::().expect("we put this in ourselves"); - let _original = original.0.downcast_ref::().expect("we know this type corresponds to the output type"); - - // Check the original type - - let new = put_item_output.clone(); - - // Do the thing here - - *put_item_output = new; - } - } - } - - Ok(()) - } -} \ No newline at end of file From f1f530a7d886c97667efa0111d776048c3c31e2c Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 30 May 2024 13:34:21 -0400 Subject: [PATCH 5/7] try 4.6 --- .github/workflows/ci_verification.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci_verification.yml b/.github/workflows/ci_verification.yml index 4164ed5f9..31b53fcae 100644 --- a/.github/workflows/ci_verification.yml +++ b/.github/workflows/ci_verification.yml @@ -50,7 +50,7 @@ jobs: uses: dafny-lang/setup-dafny-action@v1.7.0 with: # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports. - dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.5.0' }} + dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.6.0' }} - name: Regenerate code using smithy-dafny if necessary if: ${{ inputs.nightly }} From 30235cd3199c8302ca363dcae8122a776998edf7 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 30 May 2024 15:12:35 -0400 Subject: [PATCH 6/7] m --- .../dafny/DynamoDbEncryption/src/DynamoToStruct.dfy | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index c5125ad9c..56e08d6dd 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy @@ -357,7 +357,10 @@ module DynamoToStruct { && U32ToBigEndian(|a.L|).Success? && |ret.value| >= PREFIX_LEN + LENGTH_LEN && ret.value[0..TYPEID_LEN] == SE.LIST - // && ret.value[PREFIX_LEN..PREFIX_LEN+LENGTH_LEN] == U32ToBigEndian(|a.L|).value + && ListAttrToBytes(a.L, depth).Success? + && ret.value[PREFIX_LEN..] == ListAttrToBytes(a.L, depth).value + && ListAttrToBytes(a.L, depth).value[..LENGTH_LEN] == U32ToBigEndian(|a.L|).value + && ret.value[PREFIX_LEN..PREFIX_LEN+LENGTH_LEN] == U32ToBigEndian(|a.L|).value && (|a.L| == 0 ==> |ret.value| == PREFIX_LEN + LENGTH_LEN) //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#map-attribute @@ -492,6 +495,10 @@ module DynamoToStruct { } function method ListAttrToBytes(l: ListAttributeValue, depth : nat): (ret: Result, string>) + ensures ret.Success? ==> + && U32ToBigEndian(|l|).Success? + && LENGTH_LEN <= |ret.value| + && ret.value[..LENGTH_LEN] == U32ToBigEndian(|l|).value { var count :- U32ToBigEndian(|l|); var body :- CollectList(l, depth); From 061fe9b79f9f009e427c3f1441a8d0f465ecc33d Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 30 May 2024 15:19:44 -0400 Subject: [PATCH 7/7] m --- .../dafny/DynamoDbEncryption/src/DynamoToStruct.dfy | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy index 56e08d6dd..616dfe404 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy @@ -496,9 +496,9 @@ module DynamoToStruct { function method ListAttrToBytes(l: ListAttributeValue, depth : nat): (ret: Result, string>) ensures ret.Success? ==> - && U32ToBigEndian(|l|).Success? - && LENGTH_LEN <= |ret.value| - && ret.value[..LENGTH_LEN] == U32ToBigEndian(|l|).value + && U32ToBigEndian(|l|).Success? + && LENGTH_LEN <= |ret.value| + && ret.value[..LENGTH_LEN] == U32ToBigEndian(|l|).value { var count :- U32ToBigEndian(|l|); var body :- CollectList(l, depth);