Skip to content

Commit 3ca15af

Browse files
ajewellamzajewellamz
authored
feat: more test vectors (#959)
* feat(TestVectors): extensive configuration coverage
1 parent 3f22abc commit 3ca15af

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
@@ -160,7 +160,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
160160
DDBEncode(SE.ATTR_PREFIX + k)
161161
}
162162

163-
function method MakeEncryptionContext(
163+
function method MakeEncryptionContextForEncrypt(
164164
config : InternalConfig,
165165
item : DynamoToStruct.TerminalDataMap)
166166
: (ret : Result<CMP.EncryptionContext, Error>)
@@ -179,6 +179,36 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
179179
MakeEncryptionContextV1(config, item)
180180
}
181181

182+
function method MakeEncryptionContextForDecrypt(
183+
config : InternalConfig,
184+
header : seq<uint8>,
185+
item : DynamoToStruct.TerminalDataMap)
186+
: (ret : Result<CMP.EncryptionContext, Error>)
187+
requires 0 < |header|
188+
ensures ret.Success? ==>
189+
//= specification/dynamodb-encryption-client/decrypt-item.md#dynamodb-item-base-context
190+
//= type=implication
191+
//# 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.
192+
&& (header[0] == 2 ==> ret == MakeEncryptionContextV2(config, item))
193+
//= specification/dynamodb-encryption-client/decrypt-item.md#dynamodb-item-base-context
194+
//= type=implication
195+
//# If the Version Number is 1, the base context MUST be the [version 1](./encrypt-item.md#dynamodb-item-base-context-version-1) context.
196+
&& (header[0] == 1 ==> ret == MakeEncryptionContextV1(config, item))
197+
&& ((header[0] == 1) || (header[0] == 2))
198+
199+
//= specification/dynamodb-encryption-client/decrypt-item.md#dynamodb-item-base-context
200+
//= type=implication
201+
//# If the Version Number is not 1 or 2, the operation MUST return an error.
202+
ensures ((header[0] != 1) && (header[0] != 2)) ==> ret.Failure?
203+
{
204+
if header[0] == 2 then
205+
MakeEncryptionContextV2(config, item)
206+
else if header[0] == 1 then
207+
MakeEncryptionContextV1(config, item)
208+
else
209+
Failure(E("Header attribute has unexpected version number"))
210+
}
211+
182212
function method {:opaque} {:vcs_split_on_every_assert} MakeEncryptionContextV1(
183213
config : InternalConfig,
184214
item : DynamoToStruct.TerminalDataMap)
@@ -770,9 +800,9 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
770800
//= specification/dynamodb-encryption-client/encrypt-item.md#behavior
771801
//= type=implication
772802
//# - Encryption Context MUST be this input Item's [DynamoDB Item Base Context](#dynamodb-item-base-context).
773-
&& MakeEncryptionContext(config, plaintextStructure).Success?
803+
&& MakeEncryptionContextForEncrypt(config, plaintextStructure).Success?
774804
&& Seq.Last(config.structuredEncryption.History.EncryptStructure).input.encryptionContext
775-
== Some(MakeEncryptionContext(config, plaintextStructure).value)
805+
== Some(MakeEncryptionContextForEncrypt(config, plaintextStructure).value)
776806

777807
&& output.value.parsedHeader.Some?
778808
&& var structuredEncParsed := Seq.Last(config.structuredEncryption.History.EncryptStructure).output.value.parsedHeader;
@@ -847,7 +877,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
847877

848878
var plaintextStructure :- DynamoToStruct.ItemToStructured(input.plaintextItem)
849879
.MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
850-
var context :- MakeEncryptionContext(config, plaintextStructure);
880+
var context :- MakeEncryptionContextForEncrypt(config, plaintextStructure);
851881
var cryptoSchema :- ConfigToCryptoSchema(config, input.plaintextItem)
852882
.MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
853883
var wrappedStruct := CSE.StructuredData(
@@ -977,12 +1007,25 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
9771007
content := CSE.StructuredDataContent.DataMap(plaintextStructure),
9781008
attributes := None)
9791009

1010+
//= specification/dynamodb-encryption-client/decrypt-item.md#dynamodb-item-base-context
1011+
//= type=implication
1012+
//# The item to be encrypted MUST have an attribute named `aws_dbe_head`.
1013+
&& SE.HeaderField in input.encryptedItem
1014+
&& var header := input.encryptedItem[SE.HeaderField];
1015+
1016+
//= specification/dynamodb-encryption-client/decrypt-item.md#dynamodb-item-base-context
1017+
//= type=implication
1018+
//# The attribute named `aws_dbe_head` MUST be of type `B` Binary.
1019+
&& header.B?
1020+
&& 0 < |header.B|
1021+
9801022
//= specification/dynamodb-encryption-client/decrypt-item.md#behavior
9811023
//= type=implication
9821024
//# - Encryption Context MUST be the input Item's [DynamoDB Item Base Context](./encrypt-item.md#dynamodb-item-base-context).
983-
&& MakeEncryptionContext(config, plaintextStructure).Success?
1025+
&& MakeEncryptionContextForDecrypt(config, header.B, plaintextStructure).Success?
1026+
9841027
&& Seq.Last(config.structuredEncryption.History.DecryptStructure).input.encryptionContext
985-
== Some(MakeEncryptionContext(config, plaintextStructure).value)
1028+
== Some(MakeEncryptionContextForDecrypt(config, header.B, plaintextStructure).value)
9861029

9871030
//= specification/dynamodb-encryption-client/decrypt-item.md#output
9881031
//= type=implication
@@ -1077,7 +1120,12 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
10771120

10781121
var encryptedStructure :- DynamoToStruct.ItemToStructured(input.encryptedItem)
10791122
.MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
1080-
var context :- MakeEncryptionContext(config, encryptedStructure);
1123+
:- Need(SE.HeaderField in input.encryptedItem, E("Header field, \"aws_dbe_head\", not in item."));
1124+
var header := input.encryptedItem[SE.HeaderField];
1125+
:- Need(header.B?, E("Header field, \"aws_dbe_head\", not binary"));
1126+
assert header.B?;
1127+
:- Need(0 < |header.B|, E("Unexpected empty header field."));
1128+
var context :- MakeEncryptionContextForDecrypt(config, header.B, encryptedStructure);
10811129
var authenticateSchema := ConfigToAuthenticateSchema(config, input.encryptedItem);
10821130
var wrappedStruct := CSE.StructuredData(
10831131
content := CSE.StructuredDataContent.DataMap(encryptedStructure),
@@ -1088,7 +1136,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
10881136
//# [Required Encryption Context CMM](https://github.com/awslabs/private-aws-encryption-sdk-specification-staging/blob/dafny-verified/framework/required-encryption-context-cmm.md)
10891137
//# with the following inputs:
10901138
//# - This item encryptor's [CMM](./ddb-table-encryption-config.md#cmm) as the underlying CMM.
1091-
//# - The keys from the [DynamoDB Item Base Context](./encrypt-item.md#dynamodb-item-base-context).
1139+
//# - The keys from the [DynamoDB Item Base Context](#dynamodb-item-base-context).
10921140

10931141
var reqCMMR := config.cmpClient.CreateRequiredEncryptionContextCMM(
10941142
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)