|
| 1 | +## DecryptWithPermute |
| 2 | + |
| 3 | +DB-ESDK for DynamoDB supports SIGN_ONLY and ENCRYPT_AND_SIGN attribute actions. |
| 4 | +In version 3.1.0 and below, when a Set type is assigned a SIGN_ONLY attribute action, |
| 5 | +there is a chance that signature validation of the record containing a Set will fail on read, |
| 6 | +even if the Set attributes contain the same values. |
| 7 | +The probability of a failure depends on the order of the elements in the Set |
| 8 | +combined with how DynamoDB returns this data, which is undefined. |
| 9 | + |
| 10 | +The 3.1.1 update addresses the issue by ensuring that any Set values are canonicalized |
| 11 | +in the same order while written to DynamoDB as when read back from DynamoDB. |
| 12 | + |
| 13 | +This project implements a slightly modified version of DecryptItem |
| 14 | +from the the AWS Database Encryption SDK for DynamoDB, |
| 15 | +which can validate an encrypted record that as written with 3.1.0, |
| 16 | +allowing it to be decrypted. |
| 17 | + |
| 18 | +PermuteDecrypt is exactly like the DynamoDbItemEncryptor's DecryptItem, |
| 19 | +with one exception : |
| 20 | +If the signature fails to match, and SIGN_ONLY Sets are involved, |
| 21 | +then other permutations of the members of those sets are tried, |
| 22 | +and the item is decrypted if any of those permutations allow the signature to match. |
| 23 | + |
| 24 | +If you would normally decrypt an item like this |
| 25 | +``` |
| 26 | +DynamoDbItemEncryptor itemEncryptor = DynamoDbItemEncryptor.builder() |
| 27 | + .DynamoDbItemEncryptorConfig(config) |
| 28 | + .build(); |
| 29 | +DecryptItemOutput decryptedItem = itemEncryptor.DecryptItem(myInput); |
| 30 | +``` |
| 31 | +You instead do this : |
| 32 | +``` |
| 33 | +DynamoDbPermuteDecryptor itemDecryptor = DynamoDbPermuteDecryptor.builder() |
| 34 | + .DynamoDbPermuteDecryptorConfig.builder() |
| 35 | + .inner(config) |
| 36 | + .build() |
| 37 | + .build(); |
| 38 | +PermuteDecryptOutput decryptedItem = itemDecryptor.PermuteDecrypt( |
| 39 | + PermuteDecryptInput.builder() |
| 40 | + .inner(myInput), |
| 41 | + .maxSetSize(7) |
| 42 | + .build() |
| 43 | + .build(); |
| 44 | +``` |
| 45 | +The PermuteDecryptInput holds a normal DecryptItemInput object, plus a `maxSetSize`. |
| 46 | +If any set in the item has more elements than `maxSetSize`, |
| 47 | +decryption of the item is attempted, but no permutations are attempted. |
| 48 | + |
| 49 | +The output of PermuteDecrypt holds two entries |
| 50 | +`inner` : a DecryptItemOutput object |
| 51 | +`didPermute` : if false, the item was validated and decrypted with no special handling. |
| 52 | +If true, some permutation of sets in the input allowed successful validation. |
| 53 | + |
| 54 | +If you think you know the set permutations with which the item was originally written, |
| 55 | +set that attribute of your item to the expected permutation, and call `PermuteDecrypt` |
| 56 | +with a `maxSetSize` of `1`. A single attempt will be made to validate and decrypt the record, |
| 57 | +which will quickly succeed or fail. |
| 58 | + |
| 59 | +To exhaustively try every permutation of a set of size N required N! (N factorial) attempts. |
| 60 | +As sets get large (over 7 or 8) this can start to take a considerable amount of time, |
| 61 | +so use `maxSetSize` to put a limit on the size of a set that will be attempted. |
| 62 | +A set as large as 9 can probably be handled, depending on your hardware, |
| 63 | +but over that is probably untenable. |
| 64 | + |
| 65 | + |
| 66 | +### Code Organization |
| 67 | + |
| 68 | +DecryptWithPermute is a project containing the following Dafny 'localServices' under `dafny`: |
| 69 | +- DecryptWithPermute: A single entry point : PermuteDecrypt described above. |
| 70 | + |
| 71 | +Currently this project only supports Java. |
| 72 | + |
| 73 | +#### Java |
| 74 | + |
| 75 | +`runtimes/java` contains the Java related code and build instructions for this project. |
| 76 | + |
| 77 | +Within `runtimes/java`: |
| 78 | + |
| 79 | +- `src/main/java` contains all hand written Java code, including externs. |
| 80 | +- `src/main/dafny-generated` contains all Dafny to Java transpiled code. |
| 81 | +- `src/main/smithy-generated` contains all Smithy to Java generated code. |
| 82 | + |
| 83 | +### Development |
| 84 | + |
| 85 | +Common Makefile targets are: |
| 86 | + |
| 87 | +- `make verify` verifies the whole project. You should specify a `CORES` that is as high as your |
| 88 | + computer supports in order to speed this up. However, this will still probably take long enough |
| 89 | + that your dev loop should instead use the following: |
| 90 | + - You can instead specify a single service to verify via: `make verify_service SERVICE=DecryptWithPermute` |
| 91 | + - You can also verify a specific file and output in a more help format via: `make verify_single FILE=<filename>`, |
| 92 | + where `<filename>` is the path to the file to verify relative to this directory (`DynamoDbEncryption`). |
| 93 | + You may optionally narrow down the scope by specifying a `PROC`. For example, if you just want to verify |
| 94 | + the method `EncryptStructure`, use `make verify_single FILE=<filename> PROC=EncryptStructure` |
| 95 | +- `make build_java` transpiles, builds, and tests everything from scratch in Java. |
| 96 | + You will need to run this the first time you clone this repo, and any time you introduce changes |
| 97 | + that end up adding or removing dafny-generated files. |
| 98 | + - The above command takes a while to complete. |
| 99 | + If you want to re-generate dafny code specific to a service for a service, use the following: |
| 100 | + `make local_transpile_impl_java_single SERVICE=DecryptWithPermute FILE=Index.dfy` |
| 101 | + and then `test_java` to build/test those changes. |
| 102 | + Using `Index.dfy` will end up transpiling the entire service, but you can also specify a different |
| 103 | + file to scope down the transpilation further. This target will transpile `FILE` and every |
| 104 | + "includes" in that `FILE`, recursively down to the bounds of the service namespace. |
| 105 | + Note that the `transpile_implementation_java_single` target is provided as a convenience, |
| 106 | + and is not guaranteed to be 100% consistent with output from the regular `build_java` target. |
| 107 | + The behavior SHOULD NOT be different, although if you are experiencing |
| 108 | + weird behavior, see if `build_java` resolves the issue. |
| 109 | + Only use this target for local testing. |
| 110 | + - `make local_transpile_test_java_single SERVICE=DecryptWithPermute FILE=Validate.dfy` |
| 111 | + may be used similar to above in order to re-transpile a specific test file |
| 112 | + (and any of that module's "includes" within `/test`). |
| 113 | + Note that this will clobber all other Dafny generated tests being run |
| 114 | + with `make test_java`. This target is useful to quickly iterate on changes |
| 115 | + to tests within a specific file, but you will need to `make build_java` |
| 116 | + again if you want to run the full test suite locally. |
| 117 | + Only use this target for local testing. |
| 118 | +- `make test_java` builds and tests the transpiled code in Java. |
| 119 | + |
| 120 | +### Development Requirements |
| 121 | + |
| 122 | +* Dafny 4.1.0: https://github.com/dafny-lang/dafny |
| 123 | +* A Java 8 or newer development environment |
| 124 | + |
| 125 | +#### (Optional) Dafny Report Generator Requirements |
| 126 | + |
| 127 | +Optionally, if you want to run the [Dafny Report Generator](#generate-dafny-report) |
| 128 | +you will need to install the `dafny-reportgenerator` dotnet tool |
| 129 | +(and make sure `.dotnet/tools` is within your `PATH`, |
| 130 | +see instructions in the output from running the following command): |
| 131 | + |
| 132 | +``` |
| 133 | +dotnet tool install --global dafny-reportgenerator --version 1.2.0 |
| 134 | +``` |
| 135 | + |
| 136 | +#### (Optional) Duvet Requirements |
| 137 | + |
| 138 | +Optionally, if you want to run [Duvet](https://github.com/awslabs/duvet) reports, |
| 139 | +you will need to use Cargo to install duvet. |
| 140 | + |
| 141 | +If you don't have it already, |
| 142 | +[get and install Cargo and Rust](https://doc.rust-lang.org/cargo/getting-started/installation.html). |
| 143 | + |
| 144 | +Then install duvet: |
| 145 | + |
| 146 | +``` |
| 147 | +cargo +stable install duvet |
| 148 | +``` |
| 149 | + |
| 150 | +#### System Dependencies - macOS only |
| 151 | + |
| 152 | +If you are using macOS then you must install OpenSSL 1.1, |
| 153 | +and the OpenSSL 1.1 `lib` directory must be on the dynamic linker path at runtime. |
| 154 | + |
| 155 | +If the .NET runtime cannot locate your OpenSSL 1.1 libraries, |
| 156 | +you may encounter an error that says: |
| 157 | + |
| 158 | +> No usable version of libssl was found |
| 159 | +
|
| 160 | +To resolve this, |
| 161 | +we recommend that you install OpenSSL via Homebrew using `brew install [email protected]`. |
| 162 | + |
| 163 | +## Security |
| 164 | + |
| 165 | +See [CONTRIBUTING](CONTRIBUTING.md#security-issue-notifications) for more information. |
| 166 | + |
| 167 | +## License |
| 168 | + |
| 169 | +This project is licensed under the Apache-2.0 License. |
| 170 | + |
0 commit comments