Skip to content

Commit 920fa16

Browse files
ajewellamzajewellamz
authored
Merge branch 'main' into ajewell/simplify
2 parents 4fb4544 + 3ca15af commit 920fa16

File tree

10 files changed

+289
-21
lines changed

10 files changed

+289
-21
lines changed

‎.github/workflows/ci_todos.yml

+2-2
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,8 @@ jobs:
1717
shell: bash
1818
# TODOs may be committed as long as the same line contains a link to a Github Issue or refers to a CrypTool SIM.
1919
run: |
20-
ALL_TODO_COUNT=$( { grep -r "TODO" . --exclude-dir=./submodules --exclude-dir=./.git --exclude=./.github/workflows/ci_todos.yml || true; } | wc -l)
21-
GOOD_TODO_COUNT=$( { grep -r "TODO.*\(github.com\/.*issues.*\/[1-9][0-9]*\|CrypTool-[1-9][0-9]*\)" . --exclude-dir=./submodules --exclude-dir=./.git --exclude=./.github/workflows/ci_todos.yml || true; } | wc -l)
20+
ALL_TODO_COUNT=$( { grep -r "TODO" . --exclude-dir=./TestVectors/runtimes --exclude-dir=./submodules --exclude-dir=./.git --exclude=./.github/workflows/ci_todos.yml || true; } | wc -l)
21+
GOOD_TODO_COUNT=$( { grep -r "TODO.*\(github.com\/.*issues.*\/[1-9][0-9]*\|CrypTool-[1-9][0-9]*\)" . --exclude-dir=./submodules --exclude-dir=./.git --exclude-dir=./TestVectors/runtimes --exclude=./.github/workflows/ci_todos.yml || true; } | wc -l)
2222
if [ "$ALL_TODO_COUNT" != "$GOOD_TODO_COUNT" ]; then
2323
exit 1;
2424
fi

‎DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy

+56-8
Original file line numberDiff line numberDiff line change
@@ -155,7 +155,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
155155
DDBEncode(SE.ATTR_PREFIX + k)
156156
}
157157

158-
function method MakeEncryptionContext(
158+
function method MakeEncryptionContextForEncrypt(
159159
config : InternalConfig,
160160
item : DynamoToStruct.TerminalDataMap)
161161
: (ret : Result<CMP.EncryptionContext, Error>)
@@ -174,6 +174,36 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
174174
MakeEncryptionContextV1(config, item)
175175
}
176176

177+
function method MakeEncryptionContextForDecrypt(
178+
config : InternalConfig,
179+
header : seq<uint8>,
180+
item : DynamoToStruct.TerminalDataMap)
181+
: (ret : Result<CMP.EncryptionContext, Error>)
182+
requires 0 < |header|
183+
ensures ret.Success? ==>
184+
//= specification/dynamodb-encryption-client/decrypt-item.md#dynamodb-item-base-context
185+
//= type=implication
186+
//# If the Version Number is 2, then the base context MUST be the [version 2](./encrypt-item.md#dynamodb-item-base-context-version-2) context.
187+
&& (header[0] == 2 ==> ret == MakeEncryptionContextV2(config, item))
188+
//= specification/dynamodb-encryption-client/decrypt-item.md#dynamodb-item-base-context
189+
//= type=implication
190+
//# If the Version Number is 1, the base context MUST be the [version 1](./encrypt-item.md#dynamodb-item-base-context-version-1) context.
191+
&& (header[0] == 1 ==> ret == MakeEncryptionContextV1(config, item))
192+
&& ((header[0] == 1) || (header[0] == 2))
193+
194+
//= specification/dynamodb-encryption-client/decrypt-item.md#dynamodb-item-base-context
195+
//= type=implication
196+
//# If the Version Number is not 1 or 2, the operation MUST return an error.
197+
ensures ((header[0] != 1) && (header[0] != 2)) ==> ret.Failure?
198+
{
199+
if header[0] == 2 then
200+
MakeEncryptionContextV2(config, item)
201+
else if header[0] == 1 then
202+
MakeEncryptionContextV1(config, item)
203+
else
204+
Failure(E("Header attribute has unexpected version number"))
205+
}
206+
177207
function method {:opaque} {:vcs_split_on_every_assert} MakeEncryptionContextV1(
178208
config : InternalConfig,
179209
item : DynamoToStruct.TerminalDataMap)
@@ -751,9 +781,9 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
751781
//= specification/dynamodb-encryption-client/encrypt-item.md#behavior
752782
//= type=implication
753783
//# - Encryption Context MUST be this input Item's [DynamoDB Item Base Context](#dynamodb-item-base-context).
754-
&& MakeEncryptionContext(config, plaintextStructure).Success?
784+
&& MakeEncryptionContextForEncrypt(config, plaintextStructure).Success?
755785
&& Seq.Last(config.structuredEncryption.History.EncryptStructure).input.encryptionContext
756-
== Some(MakeEncryptionContext(config, plaintextStructure).value)
786+
== Some(MakeEncryptionContextForEncrypt(config, plaintextStructure).value)
757787

758788
&& output.value.parsedHeader.Some?
759789
&& var structuredEncOut := Seq.Last(config.structuredEncryption.History.EncryptStructure).output.value;
@@ -826,7 +856,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
826856

827857
var plaintextStructure :- DynamoToStruct.ItemToStructured(input.plaintextItem)
828858
.MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
829-
var context :- MakeEncryptionContext(config, plaintextStructure);
859+
var context :- MakeEncryptionContextForEncrypt(config, plaintextStructure);
830860
var cryptoSchema :- ConfigToCryptoSchema(config, input.plaintextItem)
831861
.MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
832862

@@ -957,12 +987,25 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
957987
&& Seq.Last(config.structuredEncryption.History.DecryptStructure).input.encryptedStructure
958988
== plaintextStructure
959989

990+
//= specification/dynamodb-encryption-client/decrypt-item.md#dynamodb-item-base-context
991+
//= type=implication
992+
//# The item to be encrypted MUST have an attribute named `aws_dbe_head`.
993+
&& SE.HeaderField in input.encryptedItem
994+
&& var header := input.encryptedItem[SE.HeaderField];
995+
996+
//= specification/dynamodb-encryption-client/decrypt-item.md#dynamodb-item-base-context
997+
//= type=implication
998+
//# The attribute named `aws_dbe_head` MUST be of type `B` Binary.
999+
&& header.B?
1000+
&& 0 < |header.B|
1001+
9601002
//= specification/dynamodb-encryption-client/decrypt-item.md#behavior
9611003
//= type=implication
9621004
//# - Encryption Context MUST be the input Item's [DynamoDB Item Base Context](./encrypt-item.md#dynamodb-item-base-context).
963-
&& MakeEncryptionContext(config, plaintextStructure).Success?
1005+
&& MakeEncryptionContextForDecrypt(config, header.B, plaintextStructure).Success?
1006+
9641007
&& Seq.Last(config.structuredEncryption.History.DecryptStructure).input.encryptionContext
965-
== Some(MakeEncryptionContext(config, plaintextStructure).value)
1008+
== Some(MakeEncryptionContextForDecrypt(config, header.B, plaintextStructure).value)
9661009

9671010
//= specification/dynamodb-encryption-client/decrypt-item.md#output
9681011
//= type=implication
@@ -1055,15 +1098,20 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
10551098

10561099
var encryptedStructure :- DynamoToStruct.ItemToStructured(input.encryptedItem)
10571100
.MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
1058-
var context :- MakeEncryptionContext(config, encryptedStructure);
1101+
:- Need(SE.HeaderField in input.encryptedItem, E("Header field, \"aws_dbe_head\", not in item."));
1102+
var header := input.encryptedItem[SE.HeaderField];
1103+
:- Need(header.B?, E("Header field, \"aws_dbe_head\", not binary"));
1104+
assert header.B?;
1105+
:- Need(0 < |header.B|, E("Unexpected empty header field."));
1106+
var context :- MakeEncryptionContextForDecrypt(config, header.B, encryptedStructure);
10591107
var authenticateSchema := ConfigToAuthenticateSchema(config, input.encryptedItem);
10601108

10611109
//= specification/dynamodb-encryption-client/decrypt-item.md#behavior
10621110
//# This operation MUST create a
10631111
//# [Required Encryption Context CMM](https://github.com/awslabs/private-aws-encryption-sdk-specification-staging/blob/dafny-verified/framework/required-encryption-context-cmm.md)
10641112
//# with the following inputs:
10651113
//# - This item encryptor's [CMM](./ddb-table-encryption-config.md#cmm) as the underlying CMM.
1066-
//# - The keys from the [DynamoDB Item Base Context](./encrypt-item.md#dynamodb-item-base-context).
1114+
//# - The keys from the [DynamoDB Item Base Context](#dynamodb-item-base-context).
10671115

10681116
var reqCMMR := config.cmpClient.CreateRequiredEncryptionContextCMM(
10691117
CMP.CreateRequiredEncryptionContextCMMInput(

‎TestVectors/README.md

+22
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,28 @@ This validates the Database Encryption SDK's cross-version compatibility.
1818
1. Start in the root `./TestVectors` directory
1919
2. Run `make build_java`
2020
3. Run `make test_java`
21+
4. Run `make transpile_net`
22+
5. Run `cd runtimes/net`
23+
6. Run `dotnet run --framework net6.0`
24+
25+
### Saving results for later
26+
27+
Running the above commands will create `runtimes/java/decrypt.json` and `runtimes/net/decrypt.json`.
28+
29+
These files should be permanently saved before a release.
30+
31+
For example, if we're on version 3.4 and are getting close to a new release, we would
32+
33+
`cp runtimes/java/decrypt.json runtimes/java/decrypt_java_34.json`
34+
35+
`cp runtimes/net/decrypt.json runtimes/java/decrypt_dotnet_34.json`
36+
37+
and then modify `RunAllTests` in `dafny/DDBEncryption/src/TestVectors.dfy` to explicitly check these two files.
38+
39+
As other languages are supported, we will also deal with runtimes/XXX/decrypt.json and runtimes/java/decrypt_XXX_34.json
40+
in a simlar manner.
41+
42+
This ensures that records written in any version in any language can be read by the current version in any language.
2143

2244
## Security
2345

‎TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy

+1-1
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,6 @@ module {:options "-functionSyntax:4"} DecryptManifest {
5353
method OneTest(name : string, value : JSON) returns (output : Result<bool, string>)
5454
{
5555
:- Need(value.Object?, "Test must be an object");
56-
print "Decrypting ", name, "\n";
5756

5857
var types : Option<string> := None;
5958
var description : Option<string> := None;
@@ -99,6 +98,7 @@ module {:options "-functionSyntax:4"} DecryptManifest {
9998

10099
method Decrypt(inFile : string) returns (output : Result<bool, string>)
101100
{
101+
print "Decrypt : ", inFile, "\n";
102102
var configBv :- expect FileIO.ReadBytesFromFile(inFile);
103103
var configBytes := BvToBytes(configBv);
104104
var json :- expect API.Deserialize(configBytes);

‎TestVectors/dafny/DDBEncryption/src/EncryptManifest.dfy

+1-1
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,6 @@ module {:options "-functionSyntax:4"} EncryptManifest {
8282
method OneTest(name : string, value : JSON) returns (output : Result<Option<(string, JSON)>, string>)
8383
{
8484
:- Need(value.Object?, "Test must be an object");
85-
print "Examining ", name, "\n";
8685

8786
var types : Option<string> := None;
8887
var description : Option<string> := None;
@@ -132,6 +131,7 @@ module {:options "-functionSyntax:4"} EncryptManifest {
132131

133132
method Encrypt(inFile : string, outFile : string, lang : string, version : string) returns (output : Result<bool, string>)
134133
{
134+
print "Encrypt : ", inFile, "\n";
135135
var configBv :- expect FileIO.ReadBytesFromFile(inFile);
136136
var configBytes := BvToBytes(configBv);
137137
var json :- expect API.Deserialize(configBytes);

‎TestVectors/dafny/DDBEncryption/src/TestVectors.dfy

+3-1
Original file line numberDiff line numberDiff line change
@@ -90,8 +90,10 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
9090
var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json");
9191
var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json");
9292
var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json");
93+
var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json");
94+
var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json");
9395
var _ :- expect WriteManifest.Write("encrypt.json");
94-
var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.2");
96+
var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3");
9597
var _ :- expect DecryptManifest.Decrypt("decrypt.json");
9698
if |globalRecords| + |tableEncryptionConfigs| + |queries| == 0 {
9799
print "\nRunning no tests\n";

0 commit comments

Comments
 (0)