Skip to content

Commit a43c5d3

Browse files
SalusaSecondusSalusaSecondus
authored
Merge pull request #72 from slyubomirsky/jml-annotated
JML Specifications for KeyBlob
2 parents 7344d35 + 32fa2ca commit a43c5d3

File tree

10 files changed

+1194
-14
lines changed

10 files changed

+1194
-14
lines changed

‎README-JML.md

Lines changed: 649 additions & 0 deletions
Large diffs are not rendered by default.

‎src/main/java/com/amazonaws/encryptionsdk/EncryptedDataKey.java

Lines changed: 102 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,10 +13,112 @@
1313

1414
package com.amazonaws.encryptionsdk;
1515

16+
//@ model import java.util.Arrays;
17+
//@ model import java.nio.charset.StandardCharsets;
18+
19+
20+
//@ nullable_by_default
1621
public interface EncryptedDataKey {
22+
23+
//@// An EncryptedDataKey object abstractly contains 3 pieces of data.
24+
//@// These are represented by 3 byte arrays:
25+
26+
//@ model public instance byte[] providerId;
27+
//@ model public instance byte[] providerInformation;
28+
//@ model public instance byte[] encryptedDataKey;
29+
30+
//@// The fields of an EncryptedDataKey may be populated via deserialization. The
31+
//@// Encryption SDK design allows the deserialization routine to be called repeatedly,
32+
//@// each call trying to fill in information that for some reason was not possible
33+
//@// with the previous call. In some such "intermediate" states, the deserialization
34+
//@// is incomplete in a way that other methods don't expect. Therefore, those methods
35+
//@// should not be called in these incomplete intermediate states. The model field
36+
//@// isDeserializing is true in those incomplete intermediate states, and it is used
37+
//@// in method specifications.
38+
//@ public model instance boolean isDeserializing;
39+
40+
//@// There are some complications surrounding the representations of strings versus
41+
//@// byte arrays. The serialized form in message headers is always a sequence of
42+
//@// bytes, but the EncryptedDataKey interface (and some other methods)
43+
//@// expose the provider ID as if it were a string. Conversions (using UTF-8)
44+
//@// between byte arrays and strings (which in Java use UTF-16) are not bijections.
45+
//@// For example, both "\u003f".getBytes() and "\ud800".getBytes() yield a 1-byte
46+
//@// array containing [0x3f], and calling `new String(..., StandardCharsets.UTF_8)`
47+
//@// with either the 1-byte array [0x80] or the 3-byte array [0xef,0xbf,0xbd] yields
48+
//@// the string "\ufffd". Therefore, all we can say about these conversions
49+
//@// is that a given byte[]-String pair satisfies a conversion relation.
50+
//@//
51+
//@// The model functions "ba2s" and "s2ba" are used to specify the conversions
52+
//@// between byte arrays and strings:
53+
/*@ public normal_behavior
54+
@ requires s != null;
55+
@ ensures \result != null;
56+
@ function
57+
@ public model static byte[] s2ba(String s) {
58+
@ return s.getBytes(StandardCharsets.UTF_8);
59+
@ }
60+
@*/
61+
/*@ public normal_behavior
62+
@ requires ba != null;
63+
@ ensures \result != null;
64+
@ function
65+
@ public model static String ba2s(byte[] ba) {
66+
@ return new String(ba, StandardCharsets.UTF_8);
67+
@ }
68+
@*/
69+
//@// The "ba2s" and "s2ba" are given function bodies above, but the verification
70+
//@// does not rely on these function bodies directly. Instead, the code (in KeyBlob)
71+
//@// uses "assume" statements when it necessary to connect these functions with
72+
//@// copies of their bodies that appear in the code. This is a limitation of JML.
73+
//@//
74+
//@// One of the properties that holds of "s2ba(s)" is that its result depends not
75+
//@// on the particular String reference "s" being passed in, but only the contents
76+
//@// of the string referenced by "s". This property is captured in the following
77+
//@// lemma:
78+
/*@ public normal_behavior
79+
@ requires s != null && t != null && String.equals(s, t);
80+
@ ensures Arrays.equalArrays(s2ba(s), s2ba(t));
81+
@ pure
82+
@ public model static void lemma_s2ba_depends_only_string_contents_only(String s, String t);
83+
@*/
84+
//@//
85+
//@// As a specification convenience, the model function "ba2s2ba" uses the two
86+
//@// model functions above to convert from a byte array to a String and then back
87+
//@// to a byte array. As mentioned above, this does not always result in a byte
88+
//@// array with the original contents. The "assume" statements about the conversion
89+
//@// functions need to be careful not to assume too much.
90+
/*@ public normal_behavior
91+
@ requires ba != null;
92+
@ ensures \result == s2ba(ba2s(ba));
93+
@ function
94+
@ public model static byte[] ba2s2ba(byte[] ba) {
95+
@ return s2ba(ba2s(ba));
96+
@ }
97+
@*/
98+
99+
//@// Here follows 3 methods that access the abstract values of interface properties.
100+
//@// Something to note about these methods is that each one requires the property
101+
//@// requested to be known to be non-null. For example, "getProviderId" is only allowed
102+
//@// to be called when "providerId" is known to be non-null.
103+
104+
//@ public normal_behavior
105+
//@ requires providerId != null;
106+
//@ ensures \result != null;
107+
//@ ensures String.equals(\result, ba2s(providerId));
108+
//@ pure
17109
public String getProviderId();
18110

111+
//@ public normal_behavior
112+
//@ requires providerInformation != null;
113+
//@ ensures \fresh(\result);
114+
//@ ensures Arrays.equalArrays(providerInformation, \result);
115+
//@ pure
19116
public byte[] getProviderInformation();
20117

118+
//@ public normal_behavior
119+
//@ requires encryptedDataKey != null;
120+
//@ ensures \fresh(\result);
121+
//@ ensures Arrays.equalArrays(encryptedDataKey, \result);
122+
//@ pure
21123
public byte[] getEncryptedDataKey();
22124
}

‎src/main/java/com/amazonaws/encryptionsdk/exception/AwsCryptoException.java

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,25 +16,41 @@
1616
/**
1717
* This is the parent class of the runtime exceptions thrown by the AWS Encryption SDK.
1818
*/
19+
//@ non_null_by_default
1920
public class AwsCryptoException extends RuntimeException {
2021
private static final long serialVersionUID = -1L;
2122

23+
//@ public normal_behavior
24+
//@ ensures standardThrowable();
25+
//@ pure
2226
public AwsCryptoException() {
2327
super();
2428
}
2529

30+
//@ public normal_behavior
31+
//@ ensures standardThrowable(message);
32+
//@ pure
2633
public AwsCryptoException(final String message) {
2734
super(message);
2835
}
2936

37+
//@ public normal_behavior
38+
//@ ensures standardThrowable(cause);
39+
//@ pure
3040
public AwsCryptoException(final Throwable cause) {
3141
super(cause);
3242
}
3343

44+
//@ public normal_behavior
45+
//@ ensures standardThrowable(message,cause);
46+
//@ pure
3447
public AwsCryptoException(final String message, final Throwable cause) {
3548
super(message, cause);
3649
}
3750

51+
//@ public normal_behavior
52+
//@ ensures standardThrowable(message,cause);
53+
//@ pure // TODO
3854
public AwsCryptoException(final String message, final Throwable cause, final boolean enableSuppression,
3955
final boolean writableStackTrace) {
4056
super(message, cause, enableSuppression, writableStackTrace);

‎src/main/java/com/amazonaws/encryptionsdk/exception/BadCiphertextException.java

Lines changed: 18 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,22 +17,39 @@
1717
* This exception is thrown when the values found in a ciphertext message are
1818
* invalid or corrupt.
1919
*/
20+
//@ non_null_by_default
2021
public class BadCiphertextException extends AwsCryptoException {
2122
private static final long serialVersionUID = -1L;
2223

24+
/*@ public normal_behavior
25+
@ ensures standardThrowable();
26+
@*/
27+
//@ pure
2328
public BadCiphertextException() {
2429
super();
2530
}
2631

32+
/*@ public normal_behavior
33+
@ ensures standardThrowable(message);
34+
@*/
35+
//@ pure
2736
public BadCiphertextException(final String message) {
2837
super(message);
2938
}
3039

40+
/*@ public normal_behavior
41+
@ ensures standardThrowable(cause);
42+
@*/
43+
//@ pure
3144
public BadCiphertextException(final Throwable cause) {
3245
super(cause);
3346
}
3447

48+
/*@ public normal_behavior
49+
@ ensures standardThrowable(message,cause);
50+
@*/
51+
//@ pure
3552
public BadCiphertextException(final String message, final Throwable cause) {
3653
super(message, cause);
3754
}
38-
}
55+
}

‎src/main/java/com/amazonaws/encryptionsdk/exception/CannotUnwrapDataKeyException.java

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,21 +18,38 @@
1818
/**
1919
* This exception is thrown when there are no {@link DataKey}s which can be decrypted.
2020
*/
21+
//@ non_null_by_default
2122
public class CannotUnwrapDataKeyException extends AwsCryptoException {
2223
private static final long serialVersionUID = -1L;
2324

25+
/*@ public normal_behavior
26+
@ ensures standardThrowable();
27+
@*/
28+
//@ pure
2429
public CannotUnwrapDataKeyException() {
2530
super();
2631
}
2732

33+
/*@ public normal_behavior
34+
@ ensures standardThrowable(message);
35+
@*/
36+
//@ pure
2837
public CannotUnwrapDataKeyException(final String message) {
2938
super(message);
3039
}
3140

41+
/*@ public normal_behavior
42+
@ ensures standardThrowable(cause);
43+
@*/
44+
//@ pure
3245
public CannotUnwrapDataKeyException(final Throwable cause) {
3346
super(cause);
3447
}
3548

49+
/*@ public normal_behavior
50+
@ ensures standardThrowable(message,cause);
51+
@*/
52+
//@ pure
3653
public CannotUnwrapDataKeyException(final String message, final Throwable cause) {
3754
super(message, cause);
3855
}

‎src/main/java/com/amazonaws/encryptionsdk/exception/NoSuchMasterKeyException.java

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,24 +19,45 @@
1919
* This exception is thrown when the SDK attempts to use a {@link MasterKey} which either doesn't
2020
* exist or to which it doesn't have access.
2121
*/
22+
//@ non_null_by_default
2223
public class NoSuchMasterKeyException extends AwsCryptoException {
2324
private static final long serialVersionUID = -1L;
2425

26+
/*@ public normal_behavior
27+
@ ensures standardThrowable();
28+
@*/
29+
//@ pure
2530
public NoSuchMasterKeyException() {
2631
}
2732

33+
/*@ public normal_behavior
34+
@ ensures standardThrowable(message);
35+
@*/
36+
//@ pure
2837
public NoSuchMasterKeyException(final String message) {
2938
super(message);
3039
}
3140

41+
/*@ public normal_behavior
42+
@ ensures standardThrowable(cause);
43+
@*/
44+
//@ pure
3245
public NoSuchMasterKeyException(final Throwable cause) {
3346
super(cause);
3447
}
3548

49+
/*@ public normal_behavior
50+
@ ensures standardThrowable(message,cause);
51+
@*/
52+
//@ pure
3653
public NoSuchMasterKeyException(final String message, final Throwable cause) {
3754
super(message, cause);
3855
}
3956

57+
/*@ public normal_behavior
58+
@ ensures standardThrowable(message,cause);
59+
@*/
60+
//@ pure // TODO
4061
public NoSuchMasterKeyException(final String message, final Throwable cause,
4162
final boolean enableSuppression, final boolean writableStackTrace) {
4263
super(message, cause, enableSuppression, writableStackTrace);

‎src/main/java/com/amazonaws/encryptionsdk/exception/ParseException.java

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,12 +17,17 @@
1717
* This exception is thrown when there are not enough bytes to parse a primitive, a specified number
1818
* of bytes, or the bytes does not properly represent the desired object.
1919
*/
20+
//@ non_null_by_default
2021
public class ParseException extends AwsCryptoException {
2122
private static final long serialVersionUID = -1L;
2223

2324
/**
2425
* Constructs a new exception with no detail message.
2526
*/
27+
/*@ public normal_behavior
28+
@ ensures standardThrowable();
29+
@*/
30+
//@ pure
2631
public ParseException() {
2732
super();
2833
}
@@ -33,6 +38,10 @@ public ParseException() {
3338
* @param message
3439
* the detail message.
3540
*/
41+
/*@ public normal_behavior
42+
@ ensures standardThrowable(message);
43+
@*/
44+
//@ pure
3645
public ParseException(final String message) {
3746
super(message);
3847
}
@@ -47,6 +56,10 @@ public ParseException(final String message) {
4756
* method). (A <tt>null</tt> value is permitted, and indicates that the cause is
4857
* nonexistent or unknown.)
4958
*/
59+
/*@ public normal_behavior
60+
@ ensures standardThrowable(cause);
61+
@*/
62+
//@ pure
5063
public ParseException(final Throwable cause) {
5164
super(cause);
5265
}
@@ -67,6 +80,10 @@ public ParseException(final Throwable cause) {
6780
* method). (A <tt>null</tt> value is permitted, and indicates that the cause is
6881
* nonexistent or unknown.)
6982
*/
83+
/*@ public normal_behavior
84+
@ ensures standardThrowable(message,cause);
85+
@*/
86+
//@ pure
7087
public ParseException(final String message, final Throwable cause) {
7188
super(message, cause);
7289
}

‎src/main/java/com/amazonaws/encryptionsdk/exception/UnsupportedProviderException.java

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,24 +19,45 @@
1919
* This exception is thrown when there are no {@link MasterKeyProvider}s which which support the
2020
* requested {@code provider} value.
2121
*/
22+
//@ non_null_by_default
2223
public class UnsupportedProviderException extends AwsCryptoException {
2324
private static final long serialVersionUID = -1L;
2425

26+
/*@ public normal_behavior
27+
@ ensures standardThrowable();
28+
@*/
29+
//@ pure
2530
public UnsupportedProviderException() {
2631
}
2732

33+
/*@ public normal_behavior
34+
@ ensures standardThrowable(message);
35+
@*/
36+
//@ pure
2837
public UnsupportedProviderException(final String message) {
2938
super(message);
3039
}
3140

41+
/*@ public normal_behavior
42+
@ ensures standardThrowable(cause);
43+
@*/
44+
//@ pure
3245
public UnsupportedProviderException(final Throwable cause) {
3346
super(cause);
3447
}
3548

49+
/*@ public normal_behavior
50+
@ ensures standardThrowable(message,cause);
51+
@*/
52+
//@ pure
3653
public UnsupportedProviderException(final String message, final Throwable cause) {
3754
super(message, cause);
3855
}
3956

57+
/*@ public normal_behavior
58+
@ ensures standardThrowable(message,cause);
59+
@*/
60+
//@ pure // TODO
4061
public UnsupportedProviderException(final String message, final Throwable cause,
4162
final boolean enableSuppression, final boolean writableStackTrace) {
4263
super(message, cause, enableSuppression, writableStackTrace);

0 commit comments

Comments
 (0)