Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: dotnet examples #482

Merged
merged 43 commits into from
Nov 18, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
43 commits
Select commit Hold shift + click to select a range
4cfdd09
feat: dotnet examples
ajewellamz Oct 8, 2023
db119f6
m
ajewellamz Oct 8, 2023
bea77c7
use new SDK features
ajewellamz Oct 9, 2023
31cfb7a
repair example numbering
ajewellamz Oct 9, 2023
7b8c56a
finish interceptor
ajewellamz Oct 10, 2023
0400242
searchable encryption example
ajewellamz Oct 10, 2023
6a229de
cleanup
ajewellamz Oct 10, 2023
9a997a9
allow empty in addition to None
ajewellamz Oct 11, 2023
2dc68e4
one more example
ajewellamz Oct 11, 2023
2048e56
another example, rerun polymorph
ajewellamz Oct 12, 2023
795c704
one more example, hack Scan for dotnet
ajewellamz Oct 12, 2023
1709850
more examples
ajewellamz Oct 16, 2023
090b5e4
more examples
ajewellamz Oct 16, 2023
1fb2704
new example
ajewellamz Oct 16, 2023
5d51f63
new example
ajewellamz Oct 16, 2023
adaa29c
test
ajewellamz Oct 17, 2023
1095a6d
more examples
ajewellamz Oct 17, 2023
cfd49a5
another example
ajewellamz Oct 17, 2023
8a8063f
complex example
ajewellamz Oct 18, 2023
c1f659a
cleanup
ajewellamz Oct 18, 2023
f66d4fe
cleanup
ajewellamz Oct 18, 2023
5ccb76b
final
ajewellamz Oct 20, 2023
070705e
m
ajewellamz Oct 20, 2023
43208e5
Merge branch 'main' into dotnet-example
ajewellamz Oct 26, 2023
829c067
Merge branch 'main' into dotnet-example
ajewellamz Nov 2, 2023
5b3e127
m
ajewellamz Nov 2, 2023
6280106
final
ajewellamz Nov 2, 2023
b2fd47f
add all appropriate constructors
ajewellamz Nov 3, 2023
001fb98
multi
ajewellamz Nov 5, 2023
5466816
m
ajewellamz Nov 5, 2023
274ca4e
add codebuild/net
ajewellamz Nov 7, 2023
d64aa85
Merge branch 'main' into dotnet-example
ajewellamz Nov 8, 2023
eb087fb
test vectors
ajewellamz Nov 10, 2023
e4dd117
enable dotnet test vectors
ajewellamz Nov 10, 2023
aee52e1
m
ajewellamz Nov 10, 2023
275e111
m
ajewellamz Nov 10, 2023
9b22219
m
ajewellamz Nov 10, 2023
6b5f25b
m
ajewellamz Nov 10, 2023
731b4e3
update polymorph, remove hacks
ajewellamz Nov 16, 2023
2a1c9f6
m
ajewellamz Nov 16, 2023
7cd49a7
Merge branch 'main' into dotnet-example
ajewellamz Nov 16, 2023
ae051c0
NoMap hack for dotnet
ajewellamz Nov 16, 2023
577e37d
PackageReference
ajewellamz Nov 17, 2023
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
69 changes: 69 additions & 0 deletions .github/workflows/ci_examples_net.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,69 @@
# This workflow performs tests in .NET.
name: dotnet examples

on:
pull_request:
push:
branches:
- main

jobs:
dotNetExamples:
# Don't run the nightly build on forks
if: (github.repository_owner == 'aws')
strategy:
matrix:
library: [
DynamoDbEncryption,
]
dotnet-version: [ '6.0.x' ]
os: [
# TODO windows-latest,
# ubuntu-latest,
macos-latest,
]
runs-on: ${{ matrix.os }}
permissions:
id-token: write
contents: read
env:
DOTNET_CLI_TELEMETRY_OPTOUT: 1
DOTNET_NOLOGO: 1
steps:
- uses: actions/checkout@v3
with:
submodules: recursive

- name: Setup .NET Core SDK ${{ matrix.dotnet-version }}
uses: actions/setup-dotnet@v3
with:
dotnet-version: ${{ matrix.dotnet-version }}

- name: Setup Dafny
uses: dafny-lang/[email protected]
with:
dafny-version: ${{ '4.2.0' }}

- name: Download Dependencies
working-directory: ./${{ matrix.library }}
run: make setup_net

- name: Configure AWS Credentials
uses: aws-actions/configure-aws-credentials@v2
with:
aws-region: us-west-2
role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2
role-session-name: DDBEC-Dafny-Net-Tests

- name: Compile ${{ matrix.library }} implementation
shell: bash
working-directory: ./${{ matrix.library }}
run: |
# This works because `node` is installed by default on GHA runners
CORES=$(node -e 'console.log(os.cpus().length)')
make transpile_net CORES=$CORES
- name: Run Examples
working-directory: ./Examples/runtimes/net
shell: bash
run: |
dotnet run
64 changes: 64 additions & 0 deletions .github/workflows/ci_test_vector_net.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,64 @@
# This workflow performs test vectors in DotNet.
name: Library DotNet Test Vectors

on:
pull_request:
push:
branches:
- main

jobs:
testDotNet:
strategy:
matrix:
dotnet-version: [ '6.0.x' ]
os: [
# Run on ubuntu image that comes pre-configured with docker
ubuntu-latest
]
runs-on: ${{ matrix.os }}
permissions:
id-token: write
contents: read
steps:
- name: Setup DynamoDB Local
uses: rrainn/[email protected]
with:
port: 8000
cors: '*'

- name: Configure AWS Credentials
uses: aws-actions/configure-aws-credentials@v2
with:
aws-region: us-west-2
role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2
role-session-name: DDBEC-Dafny-DotNet-Tests

- uses: actions/checkout@v3
with:
submodules: recursive

- name: Setup Dafny
uses: dafny-lang/[email protected]
with:
dafny-version: '4.2.0'

- name: Setup .NET Core SDK ${{ matrix.dotnet-version }}
uses: actions/setup-dotnet@v3
with:
dotnet-version: ${{ matrix.dotnet-version }}

- name: Build TestVectors implementation
shell: bash
working-directory: ./TestVectors
run: |
# This works because `node` is installed by default on GHA runners
make transpile_net

- name: Test TestVectors
working-directory: ./TestVectors/runtimes/net
run: |
cp ../java/*.json .
# dotnet run
echo can't build until we make type conversions public
echo can't run until we update MPL/ComAmazonawsDynamodb
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ module BatchGetItemTransform {
&& output.value.transformedOutput.Responses.Some?
// true but expensive -- input.sdkOutput.Responses.value.Keys == output.value.transformedOutput.Responses.value.Keys
{
if input.sdkOutput.Responses.None? {
if NoMap(input.sdkOutput.Responses) {
return Success(BatchGetItemOutputTransformOutput(transformedOutput := input.sdkOutput));
}
var tableNames := input.sdkOutput.Responses.value.Keys;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ module DeleteItemTransform {
//= type=implication
//# The DeleteItem request MUST NOT refer to any legacy parameters,
//# specifically Expected and ConditionalOperator MUST NOT be set.
&& input.sdkInput.Expected.None?
&& NoMap(input.sdkInput.Expected)
&& input.sdkInput.ConditionalOperator.None?

//= specification/dynamodb-encryption-client/ddb-sdk-integration.md#validate-before-deleteitem
Expand All @@ -52,7 +52,7 @@ module DeleteItemTransform {

{
if input.sdkInput.TableName in config.tableEncryptionConfigs {
:- Need(input.sdkInput.Expected.None?, E("Legacy parameter 'Expected' not supported in UpdateItem with Encryption"));
:- Need(NoMap(input.sdkInput.Expected), E("Legacy parameter 'Expected' not supported in UpdateItem with Encryption"));
:- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in UpdateItem with Encryption"));

var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName];
Expand Down Expand Up @@ -84,7 +84,7 @@ module DeleteItemTransform {
ensures (
&& output.Success?
&& input.originalInput.TableName in config.tableEncryptionConfigs
&& input.sdkOutput.Attributes.Some?
&& !NoMap(input.sdkOutput.Attributes)
) ==>
&& var tableConfig := config.tableEncryptionConfigs[input.originalInput.TableName];
&& var oldHistory := old(tableConfig.itemEncryptor.History.DecryptItem);
Expand Down Expand Up @@ -129,7 +129,7 @@ module DeleteItemTransform {
modifies ModifiesConfig(config)
{
var tableName := input.originalInput.TableName;
if tableName !in config.tableEncryptionConfigs || input.sdkOutput.Attributes.None?
if tableName !in config.tableEncryptionConfigs || NoMap(input.sdkOutput.Attributes)
{
return Success(DeleteItemOutputTransformOutput(transformedOutput := input.sdkOutput));
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,17 @@ module DynamoDbMiddlewareSupport {
import Util = DynamoDbEncryptionUtil
import SI = SearchableEncryptionInfo


predicate method NoMap<X,Y>(m : Option<map<X,Y>>)
{
m.None? || |m.value| == 0
}

predicate method NoList<X>(m : Option<seq<X>>)
{
m.None? || |m.value| == 0
}

// IsWritable examines an AttributeMap and fails if it is unsuitable for writing.
// Generally this means that no attribute names starts with "aws_dbe_"
function method {:opaque} IsWriteable(config : ValidTableConfig, item : DDB.AttributeMap)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -32,8 +32,8 @@ module GetItemTransform {
//# with a [DynamoDB Table Name](./ddb-item-encryptor.md#dynamodb-table-name)
//# equal to the `TableName` on the GetItem request.
ensures output.Success? && input.originalInput.TableName !in config.tableEncryptionConfigs ==> output.value.transformedOutput == input.sdkOutput
ensures output.Success? && input.sdkOutput.Item.None? ==> output.value.transformedOutput.Item.None?
ensures output.Success? && input.originalInput.TableName in config.tableEncryptionConfigs && input.sdkOutput.Item.Some? ==>
ensures output.Success? && NoMap(input.sdkOutput.Item) ==> NoMap(output.value.transformedOutput.Item)
ensures output.Success? && input.originalInput.TableName in config.tableEncryptionConfigs && !NoMap(input.sdkOutput.Item) ==>
var tableConfig := config.tableEncryptionConfigs[input.originalInput.TableName];
var oldHistory := old(tableConfig.itemEncryptor.History.DecryptItem);
var newHistory := tableConfig.itemEncryptor.History.DecryptItem;
Expand Down Expand Up @@ -67,7 +67,7 @@ module GetItemTransform {
modifies ModifiesConfig(config)
{
var tableName := input.originalInput.TableName;
if tableName !in config.tableEncryptionConfigs || input.sdkOutput.Item.None? {
if tableName !in config.tableEncryptionConfigs || NoMap(input.sdkOutput.Item) {
return Success(GetItemOutputTransformOutput(transformedOutput := input.sdkOutput));
}
var tableConfig := config.tableEncryptionConfigs[tableName];
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ module PutItemTransform {
//= type=implication
//# The PutItem request MUST NOT refer to any legacy parameters,
//# specifically Expected and ConditionalOperator MUST NOT be set.
&& input.sdkInput.Expected.None? && input.sdkInput.ConditionalOperator.None?
&& NoMap(input.sdkInput.Expected) && input.sdkInput.ConditionalOperator.None?
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wow. If this is all that is needed to handle empty, we should change Java.
(But treat DDB's AttributeValue specially)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For an optional map or list, the dotnet AWS SDK can't distinguish empty from None (since it hides the IsSet method).
This should be safe for java, since the smithy says "Optional non-empty".
I don't understand what you mean by "we should change java" -- as far as I can tell, Java is right and dotnet is wrong.


// && var oldHistory := old(tableConfig.itemEncryptor.History.EncryptItem);
// && var newHistory := tableConfig.itemEncryptor.History.EncryptItem;
Expand Down Expand Up @@ -60,12 +60,9 @@ module PutItemTransform {
}
var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName];

if input.sdkInput.Expected.Some? {
return MakeError("Legacy parameter 'Expected' not supported in PutItem with Encryption.");
}
if input.sdkInput.ConditionalOperator.Some? {
return MakeError("Legacy parameter 'ConditionalOperator' not supported in PutItem with Encryption.");
}
:- Need(NoMap(input.sdkInput.Expected), E("Legacy parameter 'Expected' not supported in PutItem with Encryption."));
:- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in PutItem with Encryption."));

var _ :- IsWriteable(tableConfig, input.sdkInput.Item);
var _ :- TestConditionExpression(tableConfig,
input.sdkInput.ConditionExpression,
Expand Down Expand Up @@ -101,7 +98,7 @@ module PutItemTransform {
ensures (
&& output.Success?
&& input.originalInput.TableName in config.tableEncryptionConfigs
&& input.sdkOutput.Attributes.Some?
&& !NoMap(input.sdkOutput.Attributes)
) ==>
&& var tableConfig := config.tableEncryptionConfigs[input.originalInput.TableName];
&& var oldHistory := old(tableConfig.itemEncryptor.History.DecryptItem);
Expand Down Expand Up @@ -146,7 +143,7 @@ module PutItemTransform {
modifies ModifiesConfig(config)
{
var tableName := input.originalInput.TableName;
if tableName !in config.tableEncryptionConfigs || input.sdkOutput.Attributes.None?
if tableName !in config.tableEncryptionConfigs || NoMap(input.sdkOutput.Attributes)
{
return Success(PutItemOutputTransformOutput(transformedOutput := input.sdkOutput));
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -23,27 +23,28 @@ module QueryTransform {
//# If the `TableName` in the request does not refer to an [encrypted-table](#encrypted-table),
//# the Query request MUST be unchanged.
ensures input.sdkInput.TableName !in config.tableEncryptionConfigs ==>
&& output.Success?
&& output.value.transformedInput == input.sdkInput
&& output.Success?
&& output.value.transformedInput == input.sdkInput

ensures output.Success? && input.sdkInput.TableName in config.tableEncryptionConfigs ==>
//= specification/dynamodb-encryption-client/ddb-sdk-integration.md#modify-before-query
//= type=implication
//# The Query request MUST NOT refer to any legacy parameters,
//# specifically AttributesToGet, KeyConditions, QueryFilter and ConditionalOperator MUST NOT be set.
&& input.sdkInput.AttributesToGet.None?
&& input.sdkInput.KeyConditions.None?
&& input.sdkInput.QueryFilter.None?
&& input.sdkInput.ConditionalOperator.None?
//= specification/dynamodb-encryption-client/ddb-sdk-integration.md#modify-before-query
//= type=implication
//# The Query request MUST NOT refer to any legacy parameters,
//# specifically AttributesToGet, KeyConditions, QueryFilter and ConditionalOperator MUST NOT be set.
&& NoList(input.sdkInput.AttributesToGet)
&& NoMap(input.sdkInput.KeyConditions)
&& NoMap(input.sdkInput.QueryFilter)
&& input.sdkInput.ConditionalOperator.None?
{
if input.sdkInput.TableName !in config.tableEncryptionConfigs {
return Success(QueryInputTransformOutput(transformedInput := input.sdkInput));
} else {
:- Need(input.sdkInput.AttributesToGet.None?, E("Legacy parameter 'AttributesToGet' not supported in UpdateItem with Encryption"));
:- Need(input.sdkInput.KeyConditions.None?, E("Legacy parameter 'ScanFilter' not supported in UpdateItem with Encryption"));
:- Need(input.sdkInput.QueryFilter.None?, E("Legacy parameter 'ScanFilter' not supported in UpdateItem with Encryption"));
:- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in UpdateItem with Encryption"));
:- Need(NoList(input.sdkInput.AttributesToGet), E("Legacy parameter 'AttributesToGet' not supported in Query with Encryption"));
:- Need(NoMap(input.sdkInput.KeyConditions), E("Legacy parameter 'KeyConditions' not supported in Query with Encryption"));
:- Need(NoMap(input.sdkInput.QueryFilter), E("Legacy parameter 'QueryFilter' not supported in Query with Encryption"));
:- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in Query with Encryption"));
var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName];

var finalResult :- QueryInputForBeacons(tableConfig, input.sdkInput);
return Success(QueryInputTransformOutput(transformedInput := finalResult));
}
Expand All @@ -61,15 +62,15 @@ module QueryTransform {
ensures ValidConfig?(config)
modifies ModifiesConfig(config)

ensures input.originalInput.TableName !in config.tableEncryptionConfigs || input.sdkOutput.Items.None? ==>
&& output.Success?
&& output.value.transformedOutput == input.sdkOutput
ensures input.originalInput.TableName !in config.tableEncryptionConfigs || NoList(input.sdkOutput.Items) ==>
&& output.Success?
&& output.value.transformedOutput == input.sdkOutput

ensures output.Success? && input.sdkOutput.Items.Some? ==> output.value.transformedOutput.Items.Some?
ensures output.Success? && input.sdkOutput.Items.None? ==> output.value.transformedOutput.Items.None?
ensures output.Success? && NoList(input.sdkOutput.Items) ==> NoList(output.value.transformedOutput.Items)
{
var tableName := input.originalInput.TableName;
if tableName !in config.tableEncryptionConfigs || input.sdkOutput.Items.None? {
if tableName !in config.tableEncryptionConfigs || NoList(input.sdkOutput.Items) {
return Success(QueryOutputTransformOutput(transformedOutput := input.sdkOutput));
}
var tableConfig := config.tableEncryptionConfigs[tableName];
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -31,17 +31,18 @@ module ScanTransform {
//# The Scan request MUST NOT refer to any legacy parameters,
//# specifically AttributesToGet, ScanFilter and ConditionalOperator MUST NOT be set.
ensures output.Success? && input.sdkInput.TableName in config.tableEncryptionConfigs ==>
&& input.sdkInput.AttributesToGet.None?
&& input.sdkInput.ScanFilter.None?
&& NoList(input.sdkInput.AttributesToGet)
&& NoMap(input.sdkInput.ScanFilter)
&& input.sdkInput.ConditionalOperator.None?
{
if input.sdkInput.TableName !in config.tableEncryptionConfigs {
return Success(ScanInputTransformOutput(transformedInput := input.sdkInput));
} else {
:- Need(input.sdkInput.AttributesToGet.None?, E("Legacy parameter 'AttributesToGet' not supported in UpdateItem with Encryption"));
:- Need(input.sdkInput.ScanFilter.None?, E("Legacy parameter 'ScanFilter' not supported in UpdateItem with Encryption"));
:- Need(NoList(input.sdkInput.AttributesToGet), E("Legacy parameter 'AttributesToGet' not supported in UpdateItem with Encryption"));
:- Need(NoMap(input.sdkInput.ScanFilter), E("Legacy parameter 'ScanFilter' not supported in UpdateItem with Encryption"));
:- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in UpdateItem with Encryption"));
var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName];

var finalResult :- ScanInputForBeacons(tableConfig, input.sdkInput);
return Success(ScanInputTransformOutput(transformedInput := finalResult));
}
Expand All @@ -59,15 +60,15 @@ module ScanTransform {
ensures ValidConfig?(config)
modifies ModifiesConfig(config)

ensures input.originalInput.TableName !in config.tableEncryptionConfigs || input.sdkOutput.Items.None? ==>
ensures input.originalInput.TableName !in config.tableEncryptionConfigs || NoList(input.sdkOutput.Items) ==>
&& output.Success?
&& output.value.transformedOutput == input.sdkOutput

ensures output.Success? && input.sdkOutput.Items.None? ==> output.value.transformedOutput.Items.None?
ensures output.Success? && NoList(input.sdkOutput.Items) ==> NoList(output.value.transformedOutput.Items)
ensures output.Success? && input.sdkOutput.Items.Some? ==> output.value.transformedOutput.Items.Some?
{
var tableName := input.originalInput.TableName;
if tableName !in config.tableEncryptionConfigs || input.sdkOutput.Items.None? {
if tableName !in config.tableEncryptionConfigs || NoList(input.sdkOutput.Items) {
return Success(ScanOutputTransformOutput(transformedOutput := input.sdkOutput));
}
var tableConfig := config.tableEncryptionConfigs[tableName];
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -25,15 +25,15 @@ module TransactGetItemsTransform {
ensures ValidConfig?(config)
modifies ModifiesConfig(config)

ensures input.sdkOutput.Responses.None? ==>
ensures NoList(input.sdkOutput.Responses) ==>
&& output.Success?
&& output.value.transformedOutput == input.sdkOutput

ensures output.Success? && input.sdkOutput.Responses.Some? ==>
&& output.value.transformedOutput.Responses.Some?
&& |output.value.transformedOutput.Responses.value| == |input.originalInput.TransactItems|
{
if input.sdkOutput.Responses.None? {
if NoList(input.sdkOutput.Responses) {
return Success(TransactGetItemsOutputTransformOutput(transformedOutput := input.sdkOutput));
}
if |input.sdkOutput.Responses.value| != |input.originalInput.TransactItems| {
Expand All @@ -50,7 +50,7 @@ module TransactGetItemsTransform {
decryptedItems := decryptedItems + [encryptedItems[x]];
} else {
var tableConfig := config.tableEncryptionConfigs[tableName];
if encryptedItems[x].Item.None? {
if NoMap(encryptedItems[x].Item) {
decryptedItems := decryptedItems + [DDB.ItemResponse(Item := None)];
} else {
//= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-transactgetitems
Expand Down
Loading
Loading