@@ -65,8 +65,142 @@ module UpdateItemTransform {
65
65
66
66
method Output (config: Config , input: UpdateItemOutputTransformInput )
67
67
returns (output: Result< UpdateItemOutputTransformOutput, Error> )
68
- ensures output. Success? && output. value. transformedOutput == input. sdkOutput
68
+
69
+ // = specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-updateitem
70
+ // = type=implication
71
+ // # After a [UpdateItem](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_UpdateItem.html)
72
+ // # call is made to DynamoDB,
73
+ // # the resulting response MUST be modified before
74
+ // # being returned to the caller if:
75
+ // - there exists an Item Encryptor specified within the
76
+ // [DynamoDB Encryption Client Config](#dynamodb-encryption-client-configuration)
77
+ // with a [DynamoDB Table Name](./ddb-item-encryptor.md#dynamodb-table-name)
78
+ // equal to the `TableName` on the UpdateItem request.
79
+ // - the response contains [Attributes](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_UpdateItem.html#DDB-UpdateItem-response-Attributes).
80
+ // - the original UpdateItem request had a
81
+ // [ReturnValues](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_UpdateItem.html#DDB-UpdateItem-request-ReturnValues)
82
+ // with a value of `ALL_OLD` or `ALL_NEW`.
83
+ ensures (
84
+ && output.Success?
85
+ && input.originalInput.TableName in config.tableEncryptionConfigs
86
+ && input.sdkOutput.Attributes.Some?
87
+ && input.originalInput.ReturnValues.Some?
88
+ && (
89
+ || input.originalInput.ReturnValues.value.ALL_OLD?
90
+ || input.originalInput.ReturnValues.value.ALL_NEW?
91
+ )
92
+ ) ==>
93
+ && var tableConfig := config. tableEncryptionConfigs[input. originalInput. TableName];
94
+ && var oldHistory := old (tableConfig. itemEncryptor. History. DecryptItem);
95
+ && var newHistory := tableConfig. itemEncryptor. History. DecryptItem;
96
+
97
+ && |newHistory| == |oldHistory|+ 1
98
+ && Seq. Last (newHistory). output. Success?
99
+
100
+ // = specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-updateitem
101
+ // = type=implication
102
+ // # In this case, the [Item Encryptor](./ddb-item-encryptor.md) MUST perform
103
+ // # [Decrypt Item](./decrypt-item.md) where the input
104
+ // # [DynamoDB Item](./decrypt-item.md#dynamodb-item)
105
+ // # is the `Attributes` field in the original response
106
+ && Seq. Last (newHistory). input. encryptedItem == input. sdkOutput. Attributes. value
107
+
108
+ // = specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-updateitem
109
+ // = type=implication
110
+ // # Beacons MUST be [removed](ddb-support.md#removebeacons) from the result.
111
+ && RemoveBeacons (tableConfig, Seq.Last(newHistory). output. value. plaintextItem). Success?
112
+ && var item := RemoveBeacons (tableConfig, Seq.Last(newHistory). output. value. plaintextItem). value;
113
+
114
+ // = specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-updateitem
115
+ // = type=implication
116
+ // # The UpdateItem response's `Attributes` field MUST be
117
+ // # replaced by the encrypted DynamoDb Item outputted above.
118
+ && output. value. transformedOutput. Attributes. Some?
119
+ && (item == output. value. transformedOutput. Attributes. value)
120
+
121
+ // = specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-updateitem
122
+ // = type=implication
123
+ // # In all other cases, the UpdateItem response MUST NOT be modified.
124
+ ensures (
125
+ && output.Success?
126
+ && (
127
+ || input.originalInput.TableName !in config.tableEncryptionConfigs
128
+ || input.sdkOutput.Attributes.None?
129
+ )
130
+ ) ==> (
131
+ && output. value. transformedOutput == input. sdkOutput
132
+ )
133
+
134
+ ensures (
135
+ && output.Success?
136
+ && input.originalInput.TableName in config.tableEncryptionConfigs
137
+ && input.sdkOutput.Attributes.Some?
138
+ && (input.originalInput.ReturnValues.Some? ==> (
139
+ || input.originalInput.ReturnValues.value.UPDATED_NEW?
140
+ || input.originalInput.ReturnValues.value.UPDATED_OLD?
141
+ )
142
+ )
143
+ ) ==> (
144
+ && var tableConfig := config. tableEncryptionConfigs[input. originalInput. TableName];
145
+ && output. value. transformedOutput == input. sdkOutput
146
+ && forall k < - input. sdkOutput. Attributes. value. Keys :: ! IsSigned (tableConfig, k)
147
+ )
148
+
149
+ // = specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-updateitem
150
+ // = type=implication
151
+ // # Additionally, if a value of `UPDATED_OLD` or `UPDATED_NEW` was used,
152
+ // # and any Attributes in the response are authenticated
153
+ // # per the [DynamoDB Encryption Client Config](#dynamodb-encryption-client-configuration),
154
+ // # an error MUST be raised.
155
+ ensures (
156
+ && input.originalInput.TableName in config.tableEncryptionConfigs
157
+ && var tableConfig := config.tableEncryptionConfigs[input.originalInput.TableName];
158
+ && input.sdkOutput.Attributes.Some?
159
+ && (input.originalInput.ReturnValues.Some? ==> (
160
+ || input.originalInput.ReturnValues.value.UPDATED_NEW?
161
+ || input.originalInput.ReturnValues.value.UPDATED_OLD?
162
+ )
163
+ )
164
+ && exists k < - input. sdkOutput. Attributes. value. Keys :: IsSigned (tableConfig, k)
165
+ ) ==>
166
+ output. Failure?
167
+
168
+ requires ValidConfig?(config)
169
+ ensures ValidConfig?(config)
170
+ modifies ModifiesConfig (config)
69
171
{
70
- return Success (UpdateItemOutputTransformOutput(transformedOutput := input.sdkOutput));
172
+ var tableName := input. originalInput. TableName;
173
+
174
+ if
175
+ || tableName ! in config. tableEncryptionConfigs
176
+ || input. sdkOutput. Attributes. None?
177
+ {
178
+ return Success (UpdateItemOutputTransformOutput(transformedOutput := input.sdkOutput));
179
+ }
180
+
181
+ var tableConfig := config. tableEncryptionConfigs[tableName];
182
+ var attributes := input. sdkOutput. Attributes. value;
183
+
184
+ if ! (
185
+ && input. originalInput. ReturnValues. Some?
186
+ && (
187
+ || input. originalInput. ReturnValues. value. ALL_NEW?
188
+ || input. originalInput. ReturnValues. value. ALL_OLD?)
189
+ )
190
+ {
191
+ // This error should not be possible to reach if we assume the DDB API contract is correct.
192
+ // We include this runtime check for defensive purposes.
193
+ :- Need (forall k <- attributes.Keys :: !IsSigned(tableConfig, k),
194
+ E ("UpdateItems response contains signed attributes, but does not include the entire item which is required for verification."));
195
+
196
+ return Success (UpdateItemOutputTransformOutput(transformedOutput := input.sdkOutput));
197
+ }
198
+
199
+ var decryptRes := tableConfig. itemEncryptor. DecryptItem (
200
+ EncTypes.DecryptItemInput(encryptedItem:=attributes)
201
+ );
202
+ var decrypted :- MapError (decryptRes);
203
+ var item :- RemoveBeacons (tableConfig, decrypted.plaintextItem);
204
+ return Success (UpdateItemOutputTransformOutput(transformedOutput := input.sdkOutput.(Attributes := Some(item))));
71
205
}
72
206
}
0 commit comments