Skip to content

Java: Adapt to unboxed Java primitives #127

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 4 commits into from
May 23, 2020
Merged

Java: Adapt to unboxed Java primitives #127

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
6111aa8
Java: Use new DafnySequence methods for UByte wrapping
Dec 19, 2019
e0263ef
Java: Adapt to unboxed primitives
Jan 7, 2020
ad457bb
Merge branch 'java' into java-new-dafny
Jan 15, 2020
6be4770
Adapt to change in Dafny unboxed-java branch
Feb 12, 2020
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
2 changes: 1 addition & 1 deletion bench/SDK/Bench.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
1 change: 1 addition & 0 deletions build.gradle
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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']
}
}
Expand Down
Empty file added src/extern/STL/__default.java
View file
Open in desktop
Empty file.
32 changes: 14 additions & 18 deletions src/extern/java/AESEncryption/AES_GCM.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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<EncryptionOutput> AESEncrypt(EncryptionSuites.EncryptionSuite encAlg,
DafnySequence<UByte> iv,
DafnySequence<UByte> key,
DafnySequence<UByte> msg,
DafnySequence<UByte> aad) {
DafnySequence<Byte> iv,
DafnySequence<Byte> key,
DafnySequence<Byte> msg,
DafnySequence<Byte> 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<EncryptionOutput>(__default.EncryptionOutputFromByteSeq(bytesToUByteSequence(c), encAlg));
return new STL.Result_Success<EncryptionOutput>(__default.EncryptionOutputFromByteSeq(DafnySequence.fromBytes(c), encAlg));
}
catch (InvalidCipherTextException e) {
return new STL.Result_Failure<EncryptionOutput>(DafnySequence.asString("aes encrypt err"));
}
}

public static STL.Result<DafnySequence<UByte>> AESDecrypt(EncryptionSuites.EncryptionSuite encAlg, DafnySequence<UByte> key, DafnySequence<UByte> cipherText, DafnySequence<UByte> authTag, DafnySequence<UByte> iv, DafnySequence<UByte> aad) {
public static STL.Result<DafnySequence<Byte>> AESDecrypt(EncryptionSuites.EncryptionSuite encAlg, DafnySequence<Byte> key, DafnySequence<Byte> cipherText, DafnySequence<Byte> authTag, DafnySequence<Byte> iv, DafnySequence<Byte> 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<UByte> ctx = cipherText.concatenate(authTag);
DafnySequence<Byte> 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<DafnySequence<UByte>>(bytesToUByteSequence(pt));
return new STL.Result_Success<DafnySequence<Byte>>(DafnySequence.fromBytes(pt));
} catch (InvalidCipherTextException macEx) {
return new STL.Result_Failure<DafnySequence<UByte>>(DafnySequence.asString(macEx.toString()));
return new STL.Result_Failure<DafnySequence<Byte>>(DafnySequence.asString(macEx.toString()));
} catch (Exception e) {
return new STL.Result_Failure<DafnySequence<UByte>>(DafnySequence.asString("aes decrypt err"));
return new STL.Result_Failure<DafnySequence<Byte>>(DafnySequence.asString("aes decrypt err"));
}
}
}
20 changes: 11 additions & 9 deletions src/extern/java/Arrays/Array.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,22 +1,24 @@
package Arrays;

import dafny.Type;

import java.math.BigInteger;

public class Array {
private Array() { }

public static <T> T[] copy(String td, T[] source, BigInteger length) {
if (length.intValue() == source.length) {
return source.clone();
public static <T> Object copy(Type<T> 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 <T> void copyTo(T[] source, T[] dest, BigInteger offset) {
System.arraycopy(source, 0, dest, offset.intValue(), source.length);
public static <T> void copyTo(Type<T> t, Object source, Object dest, BigInteger offset) {
t.copyArrayTo(source, 0, dest, offset.intValue(), t.getArrayLength(source));
}
}
16 changes: 7 additions & 9 deletions src/extern/java/BouncyCastleCryptoMac/HMac.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;

Expand Down Expand Up @@ -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);
}
}
Expand All @@ -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;
}

Expand Down
25 changes: 12 additions & 13 deletions src/extern/java/RSAEncryption/RSA.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand All @@ -23,7 +22,7 @@
import static Utils.Util.*;

public class RSA {
public static Tuple2<UByte[], UByte[]> get_pem(KeyPair kp) {
public static Tuple2<byte[], byte[]> get_pem(KeyPair kp) {
try {
byte[] pk;
{
Expand All @@ -42,8 +41,8 @@ public static Tuple2<UByte[], UByte[]> 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);
}
Expand All @@ -55,7 +54,7 @@ public static Tuple2<UByte[], UByte[]> get_pem(KeyPair kp) {
@SuppressWarnings("unused")
public static final int RSA_CERTAINTY = 256;

public static Tuple2<DafnySequence<UByte>, DafnySequence<UByte>> GenerateKeyPairExtern(int bits, PaddingMode padding) {
public static Tuple2<DafnySequence<Byte>, DafnySequence<Byte>> GenerateKeyPairExtern(int bits, PaddingMode padding) {
KeyPairGenerator gen;
try {
gen = KeyPairGenerator.getInstance("RSA", BouncyCastleUtils.getProvider());
Expand All @@ -69,38 +68,38 @@ public static Tuple2<DafnySequence<UByte>, DafnySequence<UByte>> GenerateKeyPair
}

KeyPair kp = gen.generateKeyPair();
Tuple2<UByte[], UByte[]> pair = get_pem(kp);
return new Tuple2<>(DafnySequence.fromArray(pair.dtor__0()), DafnySequence.fromArray(pair.dtor__1()));
Tuple2<byte[], byte[]> pair = get_pem(kp);
return new Tuple2<>(DafnySequence.fromBytes(pair.dtor__0()), DafnySequence.fromBytes(pair.dtor__1()));
}

public static STL.Result<DafnySequence<UByte>> EncryptExtern(PaddingMode padding, DafnySequence<UByte> ek, DafnySequence<UByte> msg) {
public static STL.Result<DafnySequence<Byte>> EncryptExtern(PaddingMode padding, DafnySequence<Byte> ek, DafnySequence<Byte> 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"));
}

}

public static STL.Result<DafnySequence<UByte>> DecryptExtern(PaddingMode padding, DafnySequence<UByte> dk, DafnySequence<UByte> ctx) {
public static STL.Result<DafnySequence<Byte>> DecryptExtern(PaddingMode padding, DafnySequence<Byte> dk, DafnySequence<Byte> 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"));
Expand Down
6 changes: 2 additions & 4 deletions src/extern/java/Random/__default.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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<UByte> GenerateBytes(int i) {
public static DafnySequence<Byte> GenerateBytes(int i) {
Random rng = new Random();
byte[] z = new byte[i];
rng.nextBytes(z);
return Util.bytesToUByteSequence(z);
return DafnySequence.fromBytes(z);
}
}
37 changes: 16 additions & 21 deletions src/extern/java/Signature/ECDSA.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;
Expand All @@ -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<Tuple2<DafnySequence<UByte>, DafnySequence<UByte>>> KeyGen(ECDSAParams x) {
public static STL.Option<Tuple2<DafnySequence<Byte>, DafnySequence<Byte>>> KeyGen(ECDSAParams x) {
try {
ECKeyPairGenerator g = new ECKeyPairGenerator();
SecureRandom rng = new SecureRandom();
Expand All @@ -40,15 +35,15 @@ public static STL.Option<Tuple2<DafnySequence<UByte>, DafnySequence<UByte>>> Key
}
AsymmetricCipherKeyPair kp = g.generateKeyPair();
ECPoint pt = ((ECPublicKeyParameters)kp.getPublic()).getQ();
DafnySequence<UByte> vk = bytesToUByteSequence(pt.getEncoded());
DafnySequence<UByte> sk = bytesToUByteSequence(((ECPrivateKeyParameters)kp.getPrivate()).getD().toByteArray());
DafnySequence<Byte> vk = DafnySequence.fromBytes(pt.getEncoded());
DafnySequence<Byte> 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<UByte> vk, DafnySequence<UByte> digest, DafnySequence<UByte> sig) {
public static boolean Verify(ECDSAParams x, DafnySequence<Byte> vk, DafnySequence<Byte> digest, DafnySequence<Byte> sig) {
try {
ECNamedCurveParameterSpec p;
if (x.is_ECDSA__P384()) {
Expand All @@ -57,19 +52,19 @@ public static boolean Verify(ECDSAParams x, DafnySequence<UByte> 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<BigInteger, BigInteger> pair = DERDeserialize(uByteSequenceToBytes(sig));
return sign.verifySignature(uByteSequenceToBytes(digest), pair.dtor__0(), pair.dtor__1());
Tuple2<BigInteger, BigInteger> 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<DafnySequence<UByte>> Sign(ECDSAParams x, DafnySequence<UByte> sk, DafnySequence<UByte> digest) {
public static STL.Option<DafnySequence<Byte>> Sign(ECDSAParams x, DafnySequence<Byte> sk, DafnySequence<Byte> digest) {
try {
ECNamedCurveParameterSpec p;
if (x.is_ECDSA__P384()) {
Expand All @@ -78,21 +73,21 @@ public static STL.Option<DafnySequence<UByte>> 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);
Expand All @@ -101,15 +96,15 @@ public static STL.Option<DafnySequence<UByte>> Sign(ECDSAParams x, DafnySequence
}
}

public static DafnySequence<UByte> Digest(ECDSAParams x, DafnySequence<UByte> msg) {
public static DafnySequence<Byte> Digest(ECDSAParams x, DafnySequence<Byte> 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) {
Expand Down
Loading