Skip to content

feat: index support for beacons #73

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.

Sign up for GitHub

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

Merged
merged 2 commits into from
Mar 27, 2023
Merged

feat: index support for beacons #73

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
111aee2
feat: index support for beacons
ajewellamz Mar 27, 2023
db3fb43
m
ajewellamz Mar 27, 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
1 change: 1 addition & 0 deletions DynamoDbEncryptionMiddlewareInternal/src/DdbMiddlewareConfig.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ module DdbMiddlewareConfig {
var encryptorConfig := config.itemEncryptor.config;
&& config.partitionKeyName == encryptorConfig.partitionKeyName
&& config.sortKeyName == encryptorConfig.sortKeyName
&& config.itemEncryptor.ValidState()
}

type ValidTableConfig = c: TableConfig | ValidTableConfig?(c) witness *
Expand Down
35 changes: 27 additions & 8 deletions DynamoDbItemEncryptor/src/AwsCryptographyDynamoDbItemEncryptorOperations.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,12 @@
include "../Model/AwsCryptographyDynamoDbItemEncryptorTypes.dfy"
include "../../private-aws-encryption-sdk-dafny-staging/AwsCryptographicMaterialProviders/src/CMMs/ExpectedEncryptionContextCMM.dfy"
include "DynamoToStruct.dfy"
include "Util.dfy"
include "../../StructuredEncryption/src/SearchInfo.dfy"

module AwsCryptographyDynamoDbItemEncryptorOperations refines AbstractAwsCryptographyDynamoDbItemEncryptorOperations {
import opened StructuredEncryptionUtil
import ComAmazonawsDynamodbTypes
import opened DynamoDbItemEncryptorUtil
import CMP = AwsCryptographyMaterialProvidersTypes
import StructuredEncryption
import DynamoToStruct
Expand All @@ -16,10 +17,10 @@ module AwsCryptographyDynamoDbItemEncryptorOperations refines AbstractAwsCryptog
import opened StandardLibrary
import Seq
import CSE = AwsCryptographyStructuredEncryptionTypes
import SE = StructuredEncryptionUtil
import MaterialProviders
import ExpectedEncryptionContextCMM
import opened SearchableEncryptionInfo
import SET = AwsCryptographyStructuredEncryptionTypes

datatype Config = Config(
nameonly cmpClient : MaterialProviders.MaterialProvidersClient,
Expand All @@ -38,6 +39,24 @@ module AwsCryptographyDynamoDbItemEncryptorOperations refines AbstractAwsCryptog
)

type InternalConfig = Config
type ValidConfig = x : Config | ValidInternalConfig?(x) witness *

predicate method IsEncrypted(config : ValidConfig, attr : string)
{
&& attr in config.attributeActions
&& config.attributeActions[attr] == SET.ENCRYPT_AND_SIGN
}

predicate method IsSigned(config : ValidConfig, attr : string)
{
&& attr in config.attributeActions
&& config.attributeActions[attr] != SET.DO_NOTHING
}

const DoNotSign :=
CSE.AuthenticateSchema(content := CSE.AuthenticateSchemaContent.Action(CSE.AuthenticateAction.DO_NOT_SIGN), attributes := None)
const DoSign :=
CSE.AuthenticateSchema(content := CSE.AuthenticateSchemaContent.Action(CSE.AuthenticateAction.SIGN), attributes := None)

// constant attribute names for the encryption context
const TABLE_NAME : seq<uint8> := UTF8.EncodeAscii("aws-crypto-table-name");
Expand All @@ -52,7 +71,7 @@ module AwsCryptographyDynamoDbItemEncryptorOperations refines AbstractAwsCryptog
{
|| (unauthenticatedAttributes.Some? && attr in unauthenticatedAttributes.value)
|| (unauthenticatedPrefix.Some? && unauthenticatedPrefix.value <= attr)
|| SE.ReservedPrefix <= attr
|| ReservedPrefix <= attr
// Attributes with the reserved prefix are "allowed unauthenticated" in that
// they are not specified as signed within attributeActions.
// These attributes MAY still be authenticated via other methods,
Expand Down Expand Up @@ -105,7 +124,7 @@ module AwsCryptographyDynamoDbItemEncryptorOperations refines AbstractAwsCryptog
else if unauthenticatedPrefix.Some? && unauthenticatedPrefix.value <= attr then
"it also begins with the unauthenticatedPrefix."
else
assert SE.ReservedPrefix <= attr;
assert ReservedPrefix <= attr;
"it also begins with the reserved prefix."
}

Expand Down Expand Up @@ -298,7 +317,7 @@ module AwsCryptographyDynamoDbItemEncryptorOperations refines AbstractAwsCryptog

// It is forbidden to explicitly configure an attribute with the reserved prefix
&& (forall attribute <- config.attributeActions.Keys ::
!(SE.ReservedPrefix <= attribute))
!(ReservedPrefix <= attribute))

&& (config.beacons.Some? ==> config.beacons.value.ValidState())
}
Expand Down Expand Up @@ -355,13 +374,13 @@ module AwsCryptographyDynamoDbItemEncryptorOperations refines AbstractAwsCryptog
//= type=implication
//# Otherwise, Attributes MUST be considered as within the signature scope.
ensures ret.Success? ==>
((ret.value == SE.DoNotSign) <==> !InSignatureScope(config, attr))
((ret.value == DoNotSign) <==> !InSignatureScope(config, attr))
{
:- Need(!UnknownAttribute(config, attr), "Attribute " + attr + " is not configured");
if InSignatureScope(config, attr) then
Success(SE.DoSign)
Success(DoSign)
else
Success(SE.DoNotSign)
Success(DoNotSign)
}

// get CryptoSchema for this item
Expand Down
Loading