diff --git a/bench/SDK/Bench.dfy b/bench/SDK/Bench.dfy index b20374581..c40d20b53 100644 --- a/bench/SDK/Bench.dfy +++ b/bench/SDK/Bench.dfy @@ -63,7 +63,7 @@ module {:extern "Bench"} Bench { var keyring := new RawRSAKeyringDef.RawRSAKeyring(namespace.value, name.value, RSAEncryption.PaddingMode.PKCS1, Some(ek), Some(dk)); var cmm := new DefaultCMMDef.DefaultCMM.OfKeyring(keyring); - var n := 200 * 1024; + var n := 1024 * 1024; var msg := Replicate("lorem ipsum dolor sit amet ", n); var originalPlaintext := UTF8.Encode(msg).value; diff --git a/build.gradle b/build.gradle index 5213e0084..ab43995a6 100644 --- a/build.gradle +++ b/build.gradle @@ -21,6 +21,7 @@ project.buildDir = 'build/java' sourceSets { main { java { + // TODO: Properly split things out into main and test srcDirs = ['src/extern/java', 'test/extern/java', 'build/java/src/main'] } } diff --git a/src/extern/STL/__default.java b/src/extern/STL/__default.java new file mode 100644 index 000000000..e69de29bb diff --git a/src/extern/java/AESEncryption/AES_GCM.java b/src/extern/java/AESEncryption/AES_GCM.java index a25754e0a..893e0b39e 100644 --- a/src/extern/java/AESEncryption/AES_GCM.java +++ b/src/extern/java/AESEncryption/AES_GCM.java @@ -1,53 +1,49 @@ package AESEncryption; import dafny.DafnySequence; -import dafny.UByte; import org.bouncycastle.crypto.InvalidCipherTextException; import org.bouncycastle.crypto.engines.AESEngine; import org.bouncycastle.crypto.modes.GCMBlockCipher; import org.bouncycastle.crypto.params.AEADParameters; import org.bouncycastle.crypto.params.KeyParameter; -import static Utils.Util.bytesToUByteSequence; -import static Utils.Util.uByteSequenceToBytes; - //TODO This code has yet to be reviewed. See issue #36 public class AES_GCM { public static STL.Result AESEncrypt(EncryptionSuites.EncryptionSuite encAlg, - DafnySequence iv, - DafnySequence key, - DafnySequence msg, - DafnySequence aad) { + DafnySequence iv, + DafnySequence key, + DafnySequence msg, + DafnySequence aad) { try { GCMBlockCipher cipher = new GCMBlockCipher(new AESEngine()); - AEADParameters param = new AEADParameters(new KeyParameter(uByteSequenceToBytes(key)), encAlg.tagLen.intValue() * 8, uByteSequenceToBytes(iv), uByteSequenceToBytes(aad)); + AEADParameters param = new AEADParameters(new KeyParameter(DafnySequence.toByteArray(key)), encAlg.tagLen * 8, DafnySequence.toByteArray(iv), DafnySequence.toByteArray(aad)); cipher.init(true, param); byte[] c = new byte[cipher.getOutputSize(msg.length())]; - int len = cipher.processBytes(uByteSequenceToBytes(msg), 0, msg.length(), c, 0); + int len = cipher.processBytes(DafnySequence.toByteArray(msg), 0, msg.length(), c, 0); cipher.doFinal(c, len); //Append authentication tag to `c` - return new STL.Result_Success(__default.EncryptionOutputFromByteSeq(bytesToUByteSequence(c), encAlg)); + return new STL.Result_Success(__default.EncryptionOutputFromByteSeq(DafnySequence.fromBytes(c), encAlg)); } catch (InvalidCipherTextException e) { return new STL.Result_Failure(DafnySequence.asString("aes encrypt err")); } } - public static STL.Result> AESDecrypt(EncryptionSuites.EncryptionSuite encAlg, DafnySequence key, DafnySequence cipherText, DafnySequence authTag, DafnySequence iv, DafnySequence aad) { + public static STL.Result> AESDecrypt(EncryptionSuites.EncryptionSuite encAlg, DafnySequence key, DafnySequence cipherText, DafnySequence authTag, DafnySequence iv, DafnySequence aad) { try { GCMBlockCipher cipher = new GCMBlockCipher(new AESEngine()); - AEADParameters param = new AEADParameters(new KeyParameter(uByteSequenceToBytes(key)), encAlg.tagLen.intValue() * 8, uByteSequenceToBytes(iv), uByteSequenceToBytes(aad)); + AEADParameters param = new AEADParameters(new KeyParameter(DafnySequence.toByteArray(key)), encAlg.tagLen * 8, DafnySequence.toByteArray(iv), DafnySequence.toByteArray(aad)); cipher.init(false, param); - DafnySequence ctx = cipherText.concatenate(authTag); + DafnySequence ctx = cipherText.concatenate(authTag); byte[] pt = new byte[cipher.getOutputSize(ctx.length())]; - int len = cipher.processBytes(uByteSequenceToBytes(ctx), 0, ctx.length(), pt, 0); + int len = cipher.processBytes(DafnySequence.toByteArray(ctx), 0, ctx.length(), pt, 0); cipher.doFinal(pt, len); //Check message authentication tag - return new STL.Result_Success>(bytesToUByteSequence(pt)); + return new STL.Result_Success>(DafnySequence.fromBytes(pt)); } catch (InvalidCipherTextException macEx) { - return new STL.Result_Failure>(DafnySequence.asString(macEx.toString())); + return new STL.Result_Failure>(DafnySequence.asString(macEx.toString())); } catch (Exception e) { - return new STL.Result_Failure>(DafnySequence.asString("aes decrypt err")); + return new STL.Result_Failure>(DafnySequence.asString("aes decrypt err")); } } } diff --git a/src/extern/java/Arrays/Array.java b/src/extern/java/Arrays/Array.java index c090f1627..b44ba8117 100644 --- a/src/extern/java/Arrays/Array.java +++ b/src/extern/java/Arrays/Array.java @@ -1,22 +1,24 @@ package Arrays; +import dafny.Type; + import java.math.BigInteger; public class Array { private Array() { } - public static T[] copy(String td, T[] source, BigInteger length) { - if (length.intValue() == source.length) { - return source.clone(); + public static Object copy(Type t, Object source, BigInteger length) { + assert t.arrayType().isInstance(source); + + if (length.intValue() == t.getArrayLength(source)) { + return t.cloneArray(source); } else { - @SuppressWarnings("unchecked") - T[] dest = (T[]) java.lang.reflect.Array.newInstance( - source.getClass().getComponentType(), length.intValue()); - System.arraycopy(source, 0, dest, 0, length.intValue()); + Object dest = t.newArray(length.intValue()); + t.copyArrayTo(source, 0, dest, 0, length.intValue()); return dest; } } - public static void copyTo(T[] source, T[] dest, BigInteger offset) { - System.arraycopy(source, 0, dest, offset.intValue(), source.length); + public static void copyTo(Type t, Object source, Object dest, BigInteger offset) { + t.copyArrayTo(source, 0, dest, offset.intValue(), t.getArrayLength(source)); } } diff --git a/src/extern/java/BouncyCastleCryptoMac/HMac.java b/src/extern/java/BouncyCastleCryptoMac/HMac.java index c4d50cb23..57ce37bcf 100644 --- a/src/extern/java/BouncyCastleCryptoMac/HMac.java +++ b/src/extern/java/BouncyCastleCryptoMac/HMac.java @@ -1,11 +1,9 @@ package BouncyCastleCryptoMac; -import BouncyCastleCryptoMac.CipherParameters; import Digests.HMAC_ALGORITHM; import Utils.AlgorithmNotSupportedException; import Utils.Util; import dafny.DafnySequence; -import dafny.UByte; import java.math.BigInteger; @@ -39,7 +37,7 @@ public BigInteger getMacSize() { @Override public void init(CipherParameters ps) { if(ps.is_KeyParameter()) { - org.bouncycastle.crypto.params.KeyParameter bcKeyParameter = new org.bouncycastle.crypto.params.KeyParameter(Util.uBytesToBytes(ps.key)); + org.bouncycastle.crypto.params.KeyParameter bcKeyParameter = new org.bouncycastle.crypto.params.KeyParameter(ps.key); bcHMac.init(bcKeyParameter); } } @@ -50,20 +48,20 @@ public void reset() { } @Override - public void updateSingle(UByte input) { - bcHMac.update(input.byteValue()); + public void updateSingle(byte input) { + bcHMac.update(input); } @Override - public void update(UByte[] input , BigInteger inOff, BigInteger len) { - bcHMac.update(Util.uBytesToBytes(input), Util.bigIntegerToInt(inOff), Util.bigIntegerToInt(len)); + public void update(byte[] input , BigInteger inOff, BigInteger len) { + bcHMac.update(input, Util.bigIntegerToInt(inOff), Util.bigIntegerToInt(len)); } @Override - public BigInteger doFinal(UByte[] output, BigInteger outOff) { + public BigInteger doFinal(byte[] output, BigInteger outOff) { byte[] bytes = new byte[output.length - Util.bigIntegerToInt(outOff)]; BigInteger ans = BigInteger.valueOf(bcHMac.doFinal(bytes, 0)); - System.arraycopy(Util.bytesToUBytes(bytes), 0, output, outOff.intValue(), bytes.length); + System.arraycopy(bytes, 0, output, outOff.intValue(), bytes.length); return ans; } diff --git a/src/extern/java/RSAEncryption/RSA.java b/src/extern/java/RSAEncryption/RSA.java index dce261e6d..30fc75cf0 100644 --- a/src/extern/java/RSAEncryption/RSA.java +++ b/src/extern/java/RSAEncryption/RSA.java @@ -3,7 +3,6 @@ import Utils.BouncyCastleUtils; import dafny.DafnySequence; import dafny.Tuple2; -import dafny.UByte; import org.bouncycastle.openssl.PEMReader; import org.bouncycastle.openssl.PEMWriter; @@ -23,7 +22,7 @@ import static Utils.Util.*; public class RSA { - public static Tuple2 get_pem(KeyPair kp) { + public static Tuple2 get_pem(KeyPair kp) { try { byte[] pk; { @@ -42,8 +41,8 @@ public static Tuple2 get_pem(KeyPair kp) { pemWriter.flush(); sk = stringWriter.toString().getBytes(StandardCharsets.UTF_8); } - - return new Tuple2<>(bytesToUBytes(pk), bytesToUBytes(sk)); + + return new Tuple2<>(pk, sk); } catch (IOException e) { throw new RuntimeException(e); } @@ -55,7 +54,7 @@ public static Tuple2 get_pem(KeyPair kp) { @SuppressWarnings("unused") public static final int RSA_CERTAINTY = 256; - public static Tuple2, DafnySequence> GenerateKeyPairExtern(int bits, PaddingMode padding) { + public static Tuple2, DafnySequence> GenerateKeyPairExtern(int bits, PaddingMode padding) { KeyPairGenerator gen; try { gen = KeyPairGenerator.getInstance("RSA", BouncyCastleUtils.getProvider()); @@ -69,21 +68,21 @@ public static Tuple2, DafnySequence> GenerateKeyPair } KeyPair kp = gen.generateKeyPair(); - Tuple2 pair = get_pem(kp); - return new Tuple2<>(DafnySequence.fromArray(pair.dtor__0()), DafnySequence.fromArray(pair.dtor__1())); + Tuple2 pair = get_pem(kp); + return new Tuple2<>(DafnySequence.fromBytes(pair.dtor__0()), DafnySequence.fromBytes(pair.dtor__1())); } - public static STL.Result> EncryptExtern(PaddingMode padding, DafnySequence ek, DafnySequence msg) { + public static STL.Result> EncryptExtern(PaddingMode padding, DafnySequence ek, DafnySequence msg) { try { java.security.PublicKey pub; - PEMReader pemReader = new PEMReader(new StringReader(uByteSequenceToString(ek))); + PEMReader pemReader = new PEMReader(new StringReader(byteSequenceToString(ek))); Object pemObject = pemReader.readObject(); pub = ((java.security.PublicKey)pemObject); Cipher engine = createEngine(padding); engine.init(Cipher.ENCRYPT_MODE, pub); - return new STL.Result_Success<>(bytesToUByteSequence(engine.doFinal(uByteSequenceToBytes(msg)))); + return new STL.Result_Success<>(DafnySequence.fromBytes(engine.doFinal(DafnySequence.toByteArray(msg)))); } catch (IOException | InvalidKeyException | IllegalBlockSizeException | BadPaddingException e){ return new STL.Result_Failure<>(DafnySequence.asString("rsa encrypt error")); @@ -91,16 +90,16 @@ public static STL.Result> EncryptExtern(PaddingMode padding } - public static STL.Result> DecryptExtern(PaddingMode padding, DafnySequence dk, DafnySequence ctx) { + public static STL.Result> DecryptExtern(PaddingMode padding, DafnySequence dk, DafnySequence ctx) { try { KeyPair keyPair; Cipher engine = createEngine(padding); - Reader txtreader = new StringReader(uByteSequenceToString(dk)); + Reader txtreader = new StringReader(byteSequenceToString(dk)); keyPair = (KeyPair) new PEMReader(txtreader).readObject(); engine.init(Cipher.DECRYPT_MODE, keyPair.getPrivate()); - return new STL.Result_Success<>(bytesToUByteSequence(engine.doFinal(uByteSequenceToBytes(ctx)))); + return new STL.Result_Success<>(DafnySequence.fromBytes(engine.doFinal(DafnySequence.toByteArray(ctx)))); } catch (IOException | InvalidKeyException | IllegalBlockSizeException | BadPaddingException e){ return new STL.Result_Failure<>(DafnySequence.asString("rsa decrypt error")); diff --git a/src/extern/java/Random/__default.java b/src/extern/java/Random/__default.java index d1318f46e..a46726fbf 100644 --- a/src/extern/java/Random/__default.java +++ b/src/extern/java/Random/__default.java @@ -1,16 +1,14 @@ package Random; -import Utils.Util; import dafny.DafnySequence; -import dafny.UByte; import java.util.Random; public class __default { - public static DafnySequence GenerateBytes(int i) { + public static DafnySequence GenerateBytes(int i) { Random rng = new Random(); byte[] z = new byte[i]; rng.nextBytes(z); - return Util.bytesToUByteSequence(z); + return DafnySequence.fromBytes(z); } } diff --git a/src/extern/java/Signature/ECDSA.java b/src/extern/java/Signature/ECDSA.java index 194b2bf08..66778d1a9 100644 --- a/src/extern/java/Signature/ECDSA.java +++ b/src/extern/java/Signature/ECDSA.java @@ -1,9 +1,7 @@ package Signature; -import Utils.Util; import dafny.DafnySequence; import dafny.Tuple2; -import dafny.UByte; import org.bouncycastle.asn1.*; import org.bouncycastle.crypto.AsymmetricCipherKeyPair; import org.bouncycastle.crypto.generators.ECKeyPairGenerator; @@ -22,11 +20,8 @@ import java.security.MessageDigest; import java.security.SecureRandom; -import static Utils.Util.bytesToUByteSequence; -import static Utils.Util.uByteSequenceToBytes; - public class ECDSA { - public static STL.Option, DafnySequence>> KeyGen(ECDSAParams x) { + public static STL.Option, DafnySequence>> KeyGen(ECDSAParams x) { try { ECKeyPairGenerator g = new ECKeyPairGenerator(); SecureRandom rng = new SecureRandom(); @@ -40,15 +35,15 @@ public static STL.Option, DafnySequence>> Key } AsymmetricCipherKeyPair kp = g.generateKeyPair(); ECPoint pt = ((ECPublicKeyParameters)kp.getPublic()).getQ(); - DafnySequence vk = bytesToUByteSequence(pt.getEncoded()); - DafnySequence sk = bytesToUByteSequence(((ECPrivateKeyParameters)kp.getPrivate()).getD().toByteArray()); + DafnySequence vk = DafnySequence.fromBytes(pt.getEncoded()); + DafnySequence sk = DafnySequence.fromBytes(((ECPrivateKeyParameters) kp.getPrivate()).getD().toByteArray()); return new STL.Option_Some<>(new Tuple2<>(vk, sk)); } catch (RuntimeException e) { return new STL.Option_None<>(); } } - public static boolean Verify(ECDSAParams x, DafnySequence vk, DafnySequence digest, DafnySequence sig) { + public static boolean Verify(ECDSAParams x, DafnySequence vk, DafnySequence digest, DafnySequence sig) { try { ECNamedCurveParameterSpec p; if (x.is_ECDSA__P384()) { @@ -57,19 +52,19 @@ public static boolean Verify(ECDSAParams x, DafnySequence vk, DafnySequen p = ECNamedCurveTable.getParameterSpec("secp256r1"); } ECDomainParameters dp = new ECDomainParameters(p.getCurve(), p.getG(), p.getN(), p.getH()); - ECPoint pt = p.getCurve().decodePoint(uByteSequenceToBytes(vk)); + ECPoint pt = p.getCurve().decodePoint(DafnySequence.toByteArray(vk)); ECPublicKeyParameters vkp = new ECPublicKeyParameters(pt, dp); ECDSASigner sign = new ECDSASigner(); sign.init(false, vkp); BigInteger r, s; - Tuple2 pair = DERDeserialize(uByteSequenceToBytes(sig)); - return sign.verifySignature(uByteSequenceToBytes(digest), pair.dtor__0(), pair.dtor__1()); + Tuple2 pair = DERDeserialize(DafnySequence.toByteArray(sig)); + return sign.verifySignature(DafnySequence.toByteArray(digest), pair.dtor__0(), pair.dtor__1()); } catch (Exception e) { return false; } } - public static STL.Option> Sign(ECDSAParams x, DafnySequence sk, DafnySequence digest) { + public static STL.Option> Sign(ECDSAParams x, DafnySequence sk, DafnySequence digest) { try { ECNamedCurveParameterSpec p; if (x.is_ECDSA__P384()) { @@ -78,21 +73,21 @@ public static STL.Option> Sign(ECDSAParams x, DafnySequence p = ECNamedCurveTable.getParameterSpec("secp256r1"); } ECDomainParameters dp = new ECDomainParameters(p.getCurve(), p.getG(), p.getN(), p.getH()); - ECPrivateKeyParameters skp = new ECPrivateKeyParameters(new BigInteger(uByteSequenceToBytes(sk)), dp); + ECPrivateKeyParameters skp = new ECPrivateKeyParameters(new BigInteger(DafnySequence.toByteArray(sk)), dp); ECDSASigner sign = new ECDSASigner(); sign.init(true, skp); do { - BigInteger[] sig = sign.generateSignature(uByteSequenceToBytes(digest)); + BigInteger[] sig = sign.generateSignature(DafnySequence.toByteArray(digest)); byte[] bytes = DERSerialize(sig[0], sig[1]); - if (bytes.length != x.SignatureLength().intValue()) { + if (bytes.length != x.SignatureLength()) { // Most of the time, a signature of the wrong length can be fixed // by negating s in the signature relative to the group order. bytes = DERSerialize(sig[0], p.getN().subtract(sig[1])); } - if (bytes.length == x.SignatureLength().intValue()) { + if (bytes.length == x.SignatureLength()) { // This will meet the method postcondition, which says that a Some? return must // contain a sequence of bytes whose length is x.SignatureLength(). - return new STL.Option_Some<>(bytesToUByteSequence(bytes)); + return new STL.Option_Some<>(DafnySequence.fromBytes(bytes)); } // We only get here with low probability, so try again (forever, if we have really bad luck). } while (true); @@ -101,15 +96,15 @@ public static STL.Option> Sign(ECDSAParams x, DafnySequence } } - public static DafnySequence Digest(ECDSAParams x, DafnySequence msg) { + public static DafnySequence Digest(ECDSAParams x, DafnySequence msg) { MessageDigest alg; if (x.is_ECDSA__P384()) { alg = new JDKMessageDigest.SHA384(); } else { alg = new JDKMessageDigest.SHA256(); } - byte[] digest = alg.digest(uByteSequenceToBytes(msg)); - return bytesToUByteSequence(digest); + byte[] digest = alg.digest(DafnySequence.toByteArray(msg)); + return DafnySequence.fromBytes(digest); } private static byte[] DERSerialize(BigInteger r, BigInteger s) { diff --git a/src/extern/java/UTF8/__default.java b/src/extern/java/UTF8/__default.java index 5e33265f3..eb588d580 100644 --- a/src/extern/java/UTF8/__default.java +++ b/src/extern/java/UTF8/__default.java @@ -1,15 +1,13 @@ package UTF8; -import Utils.Util; import dafny.DafnySequence; -import dafny.UByte; import java.nio.ByteBuffer; import java.nio.CharBuffer; import java.nio.charset.*; public class __default extends _ExternBase___default { - public static STL.Result> Encode(DafnySequence str) { + public static STL.Result> Encode(DafnySequence str) { CharsetEncoder utf8 = StandardCharsets.UTF_8.newEncoder(); utf8.onMalformedInput(CodingErrorAction.REPORT); utf8.onUnmappableCharacter(CodingErrorAction.REPORT); @@ -17,18 +15,18 @@ public static STL.Result> Encode(DafnySequence s ByteBuffer utf8Buf = utf8.encode(CharBuffer.wrap(str.verbatimString())); byte[] utf8Bytes = new byte[utf8Buf.limit()]; utf8Buf.get(utf8Bytes); - return new STL.Result_Success<>(Util.bytesToUByteSequence(utf8Bytes)); + return new STL.Result_Success<>(DafnySequence.fromBytes(utf8Bytes)); } catch (CharacterCodingException e) { return new STL.Result_Failure<>(DafnySequence.asString("Input contains invalid Unicode characters")); } } - public static STL.Result> Decode(DafnySequence bytes) { + public static STL.Result> Decode(DafnySequence bytes) { CharsetDecoder utf8 = StandardCharsets.UTF_8.newDecoder(); utf8.onMalformedInput(CodingErrorAction.REPORT); utf8.onUnmappableCharacter(CodingErrorAction.REPORT); try { - String decoded = utf8.decode(ByteBuffer.wrap(Util.uByteSequenceToBytes(bytes))).toString(); + String decoded = utf8.decode(ByteBuffer.wrap(DafnySequence.toByteArray(bytes))).toString(); return new STL.Result_Success<>(DafnySequence.asString(decoded)); } catch (CharacterCodingException e) { return new STL.Result_Failure<>(DafnySequence.asString("Input contains an invalid Unicode code point")); diff --git a/src/extern/java/Utils/Util.java b/src/extern/java/Utils/Util.java index 2bee54990..fe200747f 100644 --- a/src/extern/java/Utils/Util.java +++ b/src/extern/java/Utils/Util.java @@ -1,7 +1,6 @@ package Utils; import dafny.DafnySequence; -import dafny.UByte; import java.math.BigInteger; import java.nio.charset.StandardCharsets; @@ -19,43 +18,7 @@ public static int bigIntegerToInt(BigInteger x) { } } - public static UByte[] bytesToUBytes(byte[] bytes) { - int len = bytes.length; - UByte[] ans = new UByte[len]; - for (int i = 0; i < len; i++) { - ans[i] = new UByte(bytes[i]); - } - return ans; - } - - public static byte[] uBytesToBytes(UByte[] uBytes) { - int len = uBytes.length; - byte[] ans = new byte[len]; - for (int i = 0; i < len; i++) { - ans[i] = uBytes[i].byteValue(); - } - return ans; - } - - public static DafnySequence bytesToUByteSequence(byte[] bytes) { - return DafnySequence.fromArray(bytesToUBytes(bytes)); - } - - public static byte[] uByteSequenceToBytes(DafnySequence seq) { - int len = seq.length(); - byte[] ans = new byte[len]; - int i = 0; - for (UByte b : seq) { - ans[i++] = b.byteValue(); - } - return ans; - } - - public static DafnySequence stringToUByteSequence(String string) { - return bytesToUByteSequence(string.getBytes(StandardCharsets.UTF_8)); - } - - public static String uByteSequenceToString(DafnySequence uBytes) { - return new String(uByteSequenceToBytes(uBytes), StandardCharsets.UTF_8); + public static String byteSequenceToString(DafnySequence bytes) { + return new String(DafnySequence.toByteArray(bytes), StandardCharsets.UTF_8); } }