diff --git a/BouncyCastle-JCA/src/PrivateKey.crysl b/BouncyCastle-JCA/src/PrivateKey.crysl new file mode 100644 index 00000000..ec3008cb --- /dev/null +++ b/BouncyCastle-JCA/src/PrivateKey.crysl @@ -0,0 +1,14 @@ +SPEC java.security.PrivateKey + +OBJECTS + byte[] keyMaterial; + +EVENTS + ge1: keyMaterial = getEncoded(); + GetEnc := ge1; + +ORDER + GetEnc* + +ENSURES + preparedKeyMaterial[keyMaterial] after GetEnc; diff --git a/BouncyCastle-JCA/src/PublicKey.crysl b/BouncyCastle-JCA/src/PublicKey.crysl new file mode 100644 index 00000000..e2733159 --- /dev/null +++ b/BouncyCastle-JCA/src/PublicKey.crysl @@ -0,0 +1,14 @@ +SPEC java.security.PublicKey + +OBJECTS + byte[] keyMaterial; + +EVENTS + ge1: keyMaterial = getEncoded(); + GetEnc := ge1; + +ORDER + GetEnc* + +ENSURES + preparedKeyMaterial[keyMaterial] after GetEnc; diff --git a/BouncyCastle/src/AESEngine.crysl b/BouncyCastle/src/AESEngine.crysl index 09ad7d6b..17ccd17f 100644 --- a/BouncyCastle/src/AESEngine.crysl +++ b/BouncyCastle/src/AESEngine.crysl @@ -1,10 +1,10 @@ SPEC org.bouncycastle.crypto.engines.AESEngine -OBJECTS - int dummy; //This section can't be empty or else the rule is marked with an error. +FORBIDDEN + AESEngine(); EVENTS - c1: AESEngine(); + c1: newInstance(); Con := c1; ORDER diff --git a/BouncyCastle/src/AESFastEngine.crysl b/BouncyCastle/src/AESFastEngine.crysl index 4fee91e9..57318cc6 100644 --- a/BouncyCastle/src/AESFastEngine.crysl +++ b/BouncyCastle/src/AESFastEngine.crysl @@ -1,17 +1,5 @@ //The AESFastEngine class is deprecated and insecure. This crysl rule ensures that a AESFastEngine object is considered insecure. SPEC org.bouncycastle.crypto.engines.AESFastEngine - -OBJECTS - int dummy; //This section can't be empty or else the rule is marked with an error. FORBIDDEN - AESFastEngine() ; - -EVENTS - c1: AESFastEngine(); - Con := c1; - -ORDER - Con - - + AESFastEngine(); diff --git a/BouncyCastle/src/AESLightEngine.crysl b/BouncyCastle/src/AESLightEngine.crysl index 5a3f529d..d65fdf50 100644 --- a/BouncyCastle/src/AESLightEngine.crysl +++ b/BouncyCastle/src/AESLightEngine.crysl @@ -1,8 +1,5 @@ SPEC org.bouncycastle.crypto.engines.AESLightEngine -OBJECTS - int dummy; //This section can't be empty or else the rule is marked with an error. - EVENTS c1: AESLightEngine(); Con := c1; diff --git a/BouncyCastle/src/BufferedBlockCipher.crysl b/BouncyCastle/src/BufferedBlockCipher.crysl index e23f5e20..aa59bc01 100644 --- a/BouncyCastle/src/BufferedBlockCipher.crysl +++ b/BouncyCastle/src/BufferedBlockCipher.crysl @@ -1,49 +1,5 @@ +// Deprecated SPEC org.bouncycastle.crypto.BufferedBlockCipher -OBJECTS - org.bouncycastle.crypto.BlockCipher cipher; - org.bouncycastle.crypto.CipherParameters params; - - byte plainTextByte; - byte[] plainText; - int plainTextOffset; - int plainTextLen; - - byte[] cipherText; - int cipherTextOffset; - - boolean isEncryption; - - -EVENTS - c1: BufferedBlockCipher(cipher); - Con := c1; - - i1: init(isEncryption, params); - Init := i1; - -// @return the number of output bytes copied to out. - p1: processByte(plainTextByte, cipherText, cipherTextOffset); - p2: processBytes(plainText, plainTextOffset, plainTextLen, cipherText, cipherTextOffset); - Proc := p1 | p2; - -// @return the number of output bytes copied to out. - df1: doFinal(cipherText, cipherTextOffset); - DoFinal := df1; - -ORDER - Con, (Init, Proc, DoFinal)+ - -CONSTRAINTS - length[plainText] >= plainTextOffset + plainTextLen; - length[cipherText] >= cipherTextOffset; - plainTextOffset >= 0; - plainTextLen > 0; - cipherTextOffset >= 0; - -REQUIRES - generatedGCMBlockCipher[cipher]; - generatedCipherParams[params]; - -ENSURES - encrypted[cipherText]; +FORBIDDEN + BufferedBlockCipher(org.bouncycastle.crypto.BlockCipher); diff --git a/BouncyCastle/src/CBCBlockCipher.crysl b/BouncyCastle/src/CBCBlockCipher.crysl index 72e2cb4c..cd0a0328 100644 --- a/BouncyCastle/src/CBCBlockCipher.crysl +++ b/BouncyCastle/src/CBCBlockCipher.crysl @@ -2,12 +2,15 @@ SPEC org.bouncycastle.crypto.modes.CBCBlockCipher OBJECTS org.bouncycastle.crypto.BlockCipher engine; + +FORBIDDEN + CBCBlockCipher(org.bouncycastle.crypto.BlockCipher); EVENTS - c1: CBCBlockCipher(engine); + c1: newInstance(engine); Con := c1; -//No need to specify the order, must be wrapped in PaddedBufferedCipher! +// No need to specify the order, must be wrapped in PaddedBufferedCipher! ORDER Con diff --git a/BouncyCastle/src/CCMBlockCipher.crysl b/BouncyCastle/src/CCMBlockCipher.crysl index 8373a847..72bb745d 100644 --- a/BouncyCastle/src/CCMBlockCipher.crysl +++ b/BouncyCastle/src/CCMBlockCipher.crysl @@ -18,9 +18,12 @@ OBJECTS int cipherTextOffset; boolean isEncryption; + +FORBIDDEN + CCMBlockCipher(org.bouncycastle.crypto.BlockCipher); EVENTS - c1: CCMBlockCipher(engine); + c1: newInstance(engine); Con := c1; i1: init(isEncryption, params); diff --git a/BouncyCastle/src/DefaultBufferedBlockCipher.crysl b/BouncyCastle/src/DefaultBufferedBlockCipher.crysl new file mode 100644 index 00000000..6011ba8b --- /dev/null +++ b/BouncyCastle/src/DefaultBufferedBlockCipher.crysl @@ -0,0 +1,48 @@ +SPEC org.bouncycastle.crypto.DefaultBufferedBlockCipher + +OBJECTS + org.bouncycastle.crypto.BlockCipher cipher; + org.bouncycastle.crypto.CipherParameters params; + + byte plainTextByte; + byte[] plainText; + int plainTextOffset; + int plainTextLen; + + byte[] cipherText; + int cipherTextOffset; + + boolean isEncryption; + +EVENTS + c1: DefaultBufferedBlockCipher(cipher); + Con := c1; + + i1: init(isEncryption, params); + Init := i1; + +// @return the number of output bytes copied to out. + p1: processByte(plainTextByte, cipherText, cipherTextOffset); + p2: processBytes(plainText, plainTextOffset, plainTextLen, cipherText, cipherTextOffset); + Proc := p1 | p2; + +// @return the number of output bytes copied to out. + df1: doFinal(cipherText, cipherTextOffset); + DoFinal := df1; + +ORDER + Con, (Init, Proc, DoFinal)+ + +CONSTRAINTS + length[plainText] >= plainTextOffset + plainTextLen; + length[cipherText] >= cipherTextOffset; + plainTextOffset >= 0; + plainTextLen > 0; + cipherTextOffset >= 0; + +REQUIRES + generatedGCMBlockCipher[cipher]; + generatedCipherParams[params]; + +ENSURES + encrypted[cipherText]; diff --git a/BouncyCastle/src/GCMBlockCipher.crysl b/BouncyCastle/src/GCMBlockCipher.crysl index 77e76194..d1e007d5 100644 --- a/BouncyCastle/src/GCMBlockCipher.crysl +++ b/BouncyCastle/src/GCMBlockCipher.crysl @@ -18,9 +18,12 @@ OBJECTS int cipherTextOffset; boolean isEncryption; + +FORBIDDEN + GCMBlockCipher(org.bouncycastle.crypto.BlockCipher); EVENTS - c1: GCMBlockCipher(engine); + c1: newInstance(engine); Con := c1; i1: init(isEncryption, params); diff --git a/BouncyCastle/src/SHA256Digest.crysl b/BouncyCastle/src/SHA256Digest.crysl index 89f39369..e9f803bc 100644 --- a/BouncyCastle/src/SHA256Digest.crysl +++ b/BouncyCastle/src/SHA256Digest.crysl @@ -37,7 +37,7 @@ CONSTRAINTS inputBytesOffset >= 0; inputBytesLen > 0; length[outputBytes] >= outputBytesOffset; - outputBytesOffset > 0; + outputBytesOffset >= 0; REQUIRES generatedSHA256Digest[digest]; diff --git a/BouncyCastle/src/SICBlockCipher.crysl b/BouncyCastle/src/SICBlockCipher.crysl index c755da73..e648d281 100644 --- a/BouncyCastle/src/SICBlockCipher.crysl +++ b/BouncyCastle/src/SICBlockCipher.crysl @@ -1,15 +1,16 @@ SPEC org.bouncycastle.crypto.modes.SICBlockCipher OBJECTS - org.bouncycastle.crypto.BlockCipher engine; + +FORBIDDEN + SICBlockCipher(org.bouncycastle.crypto.BlockCipher); EVENTS - c1: SICBlockCipher(engine); + c1: newInstance(engine); Con := c1; -//No need to specify the order, must be wrapped in BufferedCipher - +// No need to specify the order, must be wrapped in BufferedCipher ORDER Con diff --git a/JavaCryptographicArchitecture/src/PrivateKey.crysl b/JavaCryptographicArchitecture/src/PrivateKey.crysl new file mode 100644 index 00000000..ec3008cb --- /dev/null +++ b/JavaCryptographicArchitecture/src/PrivateKey.crysl @@ -0,0 +1,14 @@ +SPEC java.security.PrivateKey + +OBJECTS + byte[] keyMaterial; + +EVENTS + ge1: keyMaterial = getEncoded(); + GetEnc := ge1; + +ORDER + GetEnc* + +ENSURES + preparedKeyMaterial[keyMaterial] after GetEnc; diff --git a/JavaCryptographicArchitecture/src/PublicKey.crysl b/JavaCryptographicArchitecture/src/PublicKey.crysl new file mode 100644 index 00000000..e2733159 --- /dev/null +++ b/JavaCryptographicArchitecture/src/PublicKey.crysl @@ -0,0 +1,14 @@ +SPEC java.security.PublicKey + +OBJECTS + byte[] keyMaterial; + +EVENTS + ge1: keyMaterial = getEncoded(); + GetEnc := ge1; + +ORDER + GetEnc* + +ENSURES + preparedKeyMaterial[keyMaterial] after GetEnc;