From 5fb4032085b5f051985417e17458741fcd70fbba Mon Sep 17 00:00:00 2001 From: seebees Date: Wed, 19 Mar 2025 09:34:15 -0700 Subject: [PATCH 1/2] chore: Fail verification on warnings If `{:only}` gets checked in it verification should fail. --- .../dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy | 2 +- AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy | 2 +- .../AwsEncryptionSdk/src/Serialize/SerializableTypes.dfy | 2 +- .../dafny/AwsEncryptionSdk/src/Serialize/V2HeaderBody.dfy | 2 +- .../dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy | 2 +- .../AwsEncryptionSdk/test/TestRequiredEncryptionContext.dfy | 2 +- SharedMakefileV2.mk | 6 +++--- 7 files changed, 9 insertions(+), 9 deletions(-) diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy index 4b3ddbca2..83be92768 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy @@ -652,7 +652,7 @@ module EncryptDecryptHelpers { ensures res.Success? ==> && mpl.EncryptionMaterialsHasPlaintextDataKey(res.value).Success? - && !res.value.algorithmSuite.commitment.IDENTITY?; + && !res.value.algorithmSuite.commitment.IDENTITY? ensures res.Success? ==> && SerializableTypes.IsESDKEncryptionContext(res.value.encryptionContext) diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy index a296fb99a..d60bad22c 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy @@ -251,7 +251,7 @@ module MessageBody { invariant |regularFrames| == (sequenceNumber - START_SEQUENCE_NUMBER) as nat invariant |crypto.History.AESEncrypt| - |old(crypto.History.AESEncrypt)| == |regularFrames| - invariant 0 < |regularFrames| ==> Seq.First(regularFrames).header == header; + invariant 0 < |regularFrames| ==> Seq.First(regularFrames).header == header invariant IsMessageRegularFrames(regularFrames) invariant forall i: nat, j: nat, frame: Frames.Frame, callEvent diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/SerializableTypes.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/SerializableTypes.dfy index 6816c077f..39fb4413b 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/SerializableTypes.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/SerializableTypes.dfy @@ -30,7 +30,7 @@ module SerializableTypes { // The AAD section is the total length|number of pairs|key|value|key|value... // The total length is uint16, so the maximum length for the keys and values // MUST be able to include the uint16 for the number of pairs. - const ESDK_CANONICAL_ENCRYPTION_CONTEXT_MAX_LENGTH := UINT16_LIMIT - 2; + const ESDK_CANONICAL_ENCRYPTION_CONTEXT_MAX_LENGTH := UINT16_LIMIT - 2 predicate method IsESDKEncryptionContext(ec: MPL.EncryptionContext) { && |ec| < UINT16_LIMIT diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/V2HeaderBody.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/V2HeaderBody.dfy index d41472be3..d34d8b9d5 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/V2HeaderBody.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/V2HeaderBody.dfy @@ -176,7 +176,7 @@ module V2HeaderBody { } // version + suiteId + messageId - const headerBytesToAADStart := 1 + 2 + 32; + const headerBytesToAADStart := 1 + 2 + 32 predicate IsV2ExpandedAADSection( buffer: ReadableBuffer ) diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy index 6dbe5b0df..f1a785247 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy @@ -47,7 +47,7 @@ module TestCreateEsdkClient { 71, 110, 211, 189, 2, 48, 99, 98, 250, 36, 53, 182, 2, 204, 198, 55, 150, 51, 159, 101, 231, 34, 42, 30, 57, 204, 88, 114, 138, 94, 12, 79, 52, 71, 178, 34, 61, 246, 55, 163, 145, 95, 80, 61, 85, 143, 32, 0, 98, 20, 88, 251, 204, 5 - ]; + ] method {:test} TestClientCreation() { var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig(); diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestRequiredEncryptionContext.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestRequiredEncryptionContext.dfy index 77d9ac2c3..a1ca5a6e7 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestRequiredEncryptionContext.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestRequiredEncryptionContext.dfy @@ -24,7 +24,7 @@ module TestRequiredEncryptionContext { // THIS IS A TESTING RESOURCE DO NOT USE IN A PRODUCTION ENVIRONMENT const keyArn := Fixtures.keyArn - const hierarchyKeyArn := Fixtures.hierarchyKeyArn; + const hierarchyKeyArn := Fixtures.hierarchyKeyArn const branchKeyStoreName: DDBTypes.TableName := Fixtures.branchKeyStoreName const logicalKeyStoreName := branchKeyStoreName // These tests require a keystore populated with these keys diff --git a/SharedMakefileV2.mk b/SharedMakefileV2.mk index 5c22396f6..66d54cf49 100644 --- a/SharedMakefileV2.mk +++ b/SharedMakefileV2.mk @@ -13,9 +13,9 @@ VERIFY_TIMEOUT := 150 include $(SMITHY_DAFNY_ROOT)/SmithyDafnyMakefile.mk -verify:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts -verify_single:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts -verify_service:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts +verify:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts +verify_single:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts +verify_service:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts transpile_implementation_net: DAFNY_OPTIONS=--allow-warnings --compile-suffix --legacy-module-names --allow-external-contracts transpile_test_net: DAFNY_OPTIONS=--allow-warnings --include-test-runner --compile-suffix --legacy-module-names --allow-external-contracts From b98f46a5d0b09fdd6d93c0b2e7d10f1be5cf1fb4 Mon Sep 17 00:00:00 2001 From: seebees Date: Wed, 19 Mar 2025 10:32:50 -0700 Subject: [PATCH 2/2] try latest .NET --- .github/workflows/library_dafny_verification.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/library_dafny_verification.yml b/.github/workflows/library_dafny_verification.yml index ff596f61d..b347a506c 100644 --- a/.github/workflows/library_dafny_verification.yml +++ b/.github/workflows/library_dafny_verification.yml @@ -40,7 +40,7 @@ jobs: - name: Setup .NET Core SDK '6.0.x' uses: actions/setup-dotnet@v3 with: - dotnet-version: "6.0.x" + dotnet-version: "9.0.x" - name: Setup Dafny uses: dafny-lang/setup-dafny-action@v1.8.0