feat(Crypto-Java): AES GCM Extern (#73)

* feat(Crypto-Java): AES GCM Extern Passes Dafny Tests. * enable tests Co-authored-by: texastony <[email protected]>
aws · Oct 11, 2023 · 2aa5442 · 2aa5442
1 parent 725c795
commit 2aa5442
Show file tree

Hide file tree

Showing 3 changed files with 53 additions and 4 deletions.
diff --git a/.github/workflows/library_java_tests.yml b/.github/workflows/library_java_tests.yml
@@ -90,6 +90,6 @@ jobs:
  - name: Test ${{ matrix.library }}
  working-directory: ./${{ matrix.library }}
  # TODO: only tests with implemented externs may be run currently
- if: matrix.library == 'StandardLibrary' || matrix.library == 'ComAmazonawsKms'
+ if: matrix.library == 'StandardLibrary' || matrix.library == 'ComAmazonawsKms' || matrix.library == 'AwsCryptographyPrimitives'
  run: |
  make test_java
diff --git a/AwsCryptographyPrimitives/Makefile b/AwsCryptographyPrimitives/Makefile
@@ -99,7 +99,7 @@ _transpile_test_java:
  -useRuntimeLib \
  -optimizeErasableDatatypeWrapper:0 \
  -out runtimes/java/temp-tests/AwsCryptographyPrimitivesTests \
- `find ./test -name '*.dfy'` \
+ ./test/TestAES.dfy \
  -library:src/Index.dfy
 
 _mv_test_java:

diff --git a/AwsCryptographyPrimitives/runtimes/java/src/main/java/AESEncryption/AES_GCM.java b/AwsCryptographyPrimitives/runtimes/java/src/main/java/AESEncryption/AES_GCM.java
@@ -16,6 +16,9 @@
 import dafny.Array;
 import dafny.DafnySequence;
 
+import software.amazon.cryptography.primitives.ToDafny;
+import software.amazon.cryptography.primitives.model.OpaqueError;
+
 public class AES_GCM {
  public static Result<AESEncryptOutput, Error> AESEncryptExtern(
  AES__GCM encAlg,
@@ -24,7 +27,29 @@ public static Result<AESEncryptOutput, Error> AESEncryptExtern(
  DafnySequence<? extends Byte> msg,
  DafnySequence<? extends Byte> aad
  ) {
- return Result.create_Success(null);
+ byte[] keyBytes = (byte[]) Array.unwrap(key.toArray());
+ byte[] nonceBytes = (byte[]) Array.unwrap(iv.toArray());
+ byte[] plaintextBytes = (byte[]) Array.unwrap(msg.toArray());
+ final AlgorithmParameterSpec spec =
+ new GCMParameterSpec(encAlg._tagLength * 8, nonceBytes, 0, nonceBytes.length);
+ try {
+ Cipher cipher_ = Cipher.getInstance("AES/GCM/NoPadding");
+ SecretKey secretKey = new SecretKeySpec(keyBytes, "AES");
+ cipher_.init(Cipher.ENCRYPT_MODE, secretKey, spec);
+ if (aad != null) {
+ byte[] aadBytes = (byte[]) Array.unwrap(aad.toArray());
+ cipher_.updateAAD(aadBytes);
+ }
+ byte[] cipherOutput = cipher_.doFinal(plaintextBytes);
+ AESEncryptOutput aesEncryptOutput = __default.EncryptionOutputFromByteSeq(
+ DafnySequence.fromBytes(cipherOutput),
+ encAlg);
+ return Result.create_Success(aesEncryptOutput);
+ } catch ( GeneralSecurityException e) {
+ return Result.create_Failure(ToDafny.Error(
+ OpaqueError.builder().obj(e).build())
+ );
+ }
  }
 
  public static Result<DafnySequence<? extends Byte>, Error> AESDecryptExtern(
@@ -35,6 +60,30 @@ public static Result<DafnySequence<? extends Byte>, Error> AESDecryptExtern(
  DafnySequence<? extends Byte> iv,
  DafnySequence<? extends Byte> aad
  ) {
- return Result.create_Success(null);
+ byte[] keyBytes = (byte[]) Array.unwrap(key.toArray());
+ byte[] nonceBytes = (byte[]) Array.unwrap(iv.toArray());
+ byte[] ciphertextBytes = (byte[]) Array.unwrap(cipherTxt.toArray());
+ byte[] tagBytes = (byte[]) Array.unwrap(authTag.toArray());
+ byte[] ciphertextAndTag = new byte[ciphertextBytes.length + tagBytes.length];
+ System.arraycopy(ciphertextBytes, 0, ciphertextAndTag, 0, ciphertextBytes.length);
+ System.arraycopy(tagBytes, 0, ciphertextAndTag, ciphertextBytes.length, tagBytes.length);
+
+ final AlgorithmParameterSpec spec =
+ new GCMParameterSpec(encAlg._tagLength * 8, nonceBytes, 0, nonceBytes.length);
+ try {
+ Cipher cipher_ = Cipher.getInstance("AES/GCM/NoPadding");
+ SecretKey secretKey = new SecretKeySpec(keyBytes, "AES");
+ cipher_.init(Cipher.DECRYPT_MODE, secretKey, spec);
+ if (aad != null) {
+ byte[] aadBytes = (byte[]) Array.unwrap(aad.toArray());
+ cipher_.updateAAD(aadBytes);
+ }
+ byte[] cipherOutput = cipher_.doFinal(ciphertextAndTag);
+ return Result.create_Success(DafnySequence.fromBytes(cipherOutput));
+ } catch ( GeneralSecurityException e) {
+ return Result.create_Failure(ToDafny.Error(
+ OpaqueError.builder().obj(e).build())
+ );
+ }
  }
 }