Skip to content

Commit 9c61fcc

Browse files
SalusaSecondusSalusaSecondus
authored
Merge pull request #74 from slyubomirsky/more-jml-specs
JML Specifications for CipherBlockHeaders
2 parents 73e5e9f + 2989593 commit 9c61fcc

File tree

1 file changed

+167
-4
lines changed

1 file changed

+167
-4
lines changed

‎src/main/java/com/amazonaws/encryptionsdk/model/CipherBlockHeaders.java‎

Lines changed: 167 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -34,19 +34,30 @@
3434
* <li>length of content</li>
3535
* </ol>
3636
*/
37+
//@ non_null_by_default
3738
public final class CipherBlockHeaders {
39+
//@ spec_public nullable
3840
private byte[] nonce_;
41+
//@ spec_public
3942
private long contentLength_ = -1;
4043

4144
// This is set after the nonce length is parsed in the CiphertextHeaders
4245
// during decryption. This can be set only using its setter.
46+
//@ spec_public
4347
private short nonceLength_ = 0;
48+
//@ public invariant nonceLength_ >= 0;
4449

50+
//@ spec_public
4551
private boolean isComplete_;
4652

4753
/**
4854
* Default constructor.
4955
*/
56+
//@ public normal_behavior
57+
//@ ensures nonce_ == null;
58+
//@ ensures contentLength_ == -1;
59+
//@ ensures nonceLength_ == 0;
60+
//@ ensures isComplete_ == false;
5061
public CipherBlockHeaders() {
5162
}
5263

@@ -59,7 +70,18 @@ public CipherBlockHeaders() {
5970
* @param contentLen
6071
* the length of the content in the block.
6172
*/
62-
public CipherBlockHeaders(final byte[] nonce, final long contentLen) {
73+
//@ public normal_behavior
74+
//@ requires nonce != null && nonce.length <= Constants.MAX_NONCE_LENGTH;
75+
//@ ensures \fresh(nonce_) && nonce_.length == nonce.length;
76+
//@ ensures Arrays.equalArrays(nonce_, nonce);
77+
//@ ensures contentLength_ == contentLen;
78+
//@ ensures nonceLength_ == 0;
79+
//@ ensures isComplete_ == false;
80+
//@ also private exceptional_behavior
81+
//@ requires nonce == null || nonce.length > Constants.MAX_NONCE_LENGTH;
82+
//@ signals_only AwsCryptoException;
83+
//@ pure
84+
public CipherBlockHeaders(/*@ nullable @*/ final byte[] nonce, final long contentLen) {
6385
if (nonce == null) {
6486
throw new AwsCryptoException("Nonce cannot be null.");
6587
}
@@ -78,6 +100,17 @@ public CipherBlockHeaders(final byte[] nonce, final long contentLen) {
78100
* @return
79101
* the serialized bytes of the header.
80102
*/
103+
/*@ public normal_behavior
104+
@ requires nonce_ != null;
105+
@ old int nLen = nonce_.length;
106+
@ requires nonce_.length <= Integer.MAX_VALUE - (Long.SIZE / Byte.SIZE);
107+
@ ensures \result.length == nonce_.length + (Long.SIZE / Byte.SIZE);
108+
@ ensures (\forall int i; 0<=i && i<nonce_.length; \result[i] == nonce_[i]);
109+
@ ensures contentLength_ == Long.asLong(\result[nLen], \result[nLen+1], \result[nLen+2],
110+
@ \result[nLen+3], \result[nLen+4], \result[nLen+5],
111+
@ \result[nLen+6], \result[nLen+7]);
112+
@ pure
113+
@*/
81114
public byte[] toByteArray() {
82115
final int outLen = nonce_.length + (Long.SIZE / Byte.SIZE);
83116
final ByteBuffer out = ByteBuffer.allocate(outLen);
@@ -106,6 +139,19 @@ public byte[] toByteArray() {
106139
* @throws ParseException
107140
* if there are not sufficient bytes to parse the nonce.
108141
*/
142+
//@ private normal_behavior
143+
//@ requires nonceLength_ > 0;
144+
//@ requires 0 <= off;
145+
//@ requires b.length - off >= nonceLength_;
146+
//@ assignable nonce_;
147+
//@ ensures nonce_ != null && \fresh(nonce_);
148+
//@ ensures Arrays.equalArrays(b, off, nonce_, 0, nonceLength_);
149+
//@ ensures \result == nonceLength_;
150+
//@ also private exceptional_behavior
151+
//@ // add exceptions from arrays.copyofrange
152+
//@ requires b.length - off < nonceLength_;
153+
//@ assignable \nothing;
154+
//@ signals_only ParseException;
109155
private int parseNonce(final byte[] b, final int off) throws ParseException {
110156
final int bytesToParseLen = b.length - off;
111157
if (bytesToParseLen >= nonceLength_) {
@@ -136,6 +182,20 @@ private int parseNonce(final byte[] b, final int off) throws ParseException {
136182
* if there are not sufficient bytes to parse the content
137183
* length.
138184
*/
185+
//@ private behavior
186+
//@ requires off >= 0;
187+
//@ requires b.length - off >= Long.BYTES;
188+
//@ old long len = Long.asLong(b[off],b[off+1],b[off+2],b[off+3],b[off+4],b[off+5],b[off+6],b[off+7]);
189+
//@ assignable contentLength_;
190+
//@ ensures len >= 0;
191+
//@ ensures contentLength_ == len;
192+
//@ ensures \result == Long.BYTES;
193+
//@ signals_only BadCiphertextException;
194+
//@ signals (BadCiphertextException) len < 0 && contentLength_ == len;
195+
//@ also private exceptional_behavior
196+
//@ requires b.length - off < Long.BYTES;
197+
//@ assignable \nothing;
198+
//@ signals_only ParseException;
139199
private int parseContentLength(final byte[] b, final int off) throws ParseException {
140200
contentLength_ = PrimitivesParser.parseLong(b, off);
141201
if (contentLength_ < 0) {
@@ -160,11 +220,93 @@ private int parseContentLength(final byte[] b, final int off) throws ParseExcept
160220
* @return
161221
* the number of bytes consumed in deserialization.
162222
*/
163-
public int deserialize(final byte[] b, final int off) {
223+
/*@ public normal_behavior
224+
@ requires b == null;
225+
@ assignable \nothing;
226+
@ ensures \result == 0;
227+
@ also
228+
@ // case: do not need to parse either value
229+
@ public normal_behavior
230+
@ requires b != null && contentLength_ >= 0 && (nonce_ != null || nonceLength_ == 0);
231+
@ assignable isComplete_;
232+
@ ensures \result == 0;
233+
@ ensures isComplete_;
234+
@ also
235+
@ // case: parse nonce (parse exception)
236+
@ public normal_behavior
237+
@ requires b != null && nonce_ == null && nonceLength_ > 0;
238+
@ requires b.length - off < nonceLength_;
239+
@ assignable \nothing;
240+
@ ensures \result == 0;
241+
@ also
242+
@ // case: parse nonce (normally) and not content length
243+
@ public normal_behavior
244+
@ requires b != null && nonce_ == null && nonceLength_ > 0;
245+
@ requires off >= 0 && b.length - off >= nonceLength_;
246+
@ requires contentLength_ >= 0;
247+
@ assignable nonce_, isComplete_;
248+
@ ensures nonce_ != null && \fresh(nonce_);
249+
@ ensures Arrays.equalArrays(b, off, nonce_, 0, nonceLength_);
250+
@ ensures \result == nonceLength_;
251+
@ ensures isComplete_;
252+
@ also
253+
@ // case: do not parse nonce and parse content length (parse exception)
254+
@ public normal_behavior
255+
@ requires b != null && (nonce_ != null || nonceLength_ == 0);
256+
@ requires contentLength_ < 0;
257+
@ requires b.length - off < Long.BYTES;
258+
@ assignable \nothing;
259+
@ ensures \result == 0;
260+
@ also
261+
@ // case: parse nonce (normally) and parse content length (parse exception)
262+
@ public normal_behavior
263+
@ requires b != null && nonce_ == null && nonceLength_ > 0;
264+
@ requires off >= 0 && b.length - off >= nonceLength_;
265+
@ requires contentLength_ < 0;
266+
@ requires b.length - (off + nonceLength_) < Long.BYTES;
267+
@ assignable nonce_;
268+
@ ensures Arrays.equalArrays(b, off, nonce_, 0, nonceLength_);
269+
@ ensures \result == nonceLength_;
270+
@ also
271+
@ // case: do not parse nonce and parse content length (normally)
272+
@ public behavior
273+
@ requires b != null && (nonce_ != null || nonceLength_ == 0);
274+
@ requires contentLength_ < 0;
275+
@ requires off >= 0;
276+
@ requires b.length - off >= Long.BYTES;
277+
@ assignable contentLength_, isComplete_;
278+
@ ensures isComplete_ && contentLength_ >= 0;
279+
@ ensures contentLength_ == Long.asLong(b[off], b[off+1], b[off+2], b[off+3],
280+
@ b[off+4], b[off+5], b[off+6], b[off+7]);
281+
@ ensures \result == Long.BYTES;
282+
@ signals_only BadCiphertextException;
283+
@ signals (BadCiphertextException) contentLength_ < 0 && isComplete_ == \old(isComplete_);
284+
@ also
285+
@ // case: parse both normally
286+
@ public behavior
287+
@ old int nLen = nonceLength_;
288+
@ requires b != null;
289+
@ requires nonce_ == null && nonceLength_ > 0 && contentLength_ < 0;
290+
@ requires off >= 0 && b.length - off >= nonceLength_;
291+
@ requires b.length - (off + nonceLength_) >= Long.BYTES;
292+
@ requires nonceLength_ <= Integer.MAX_VALUE - Long.BYTES;
293+
@ assignable nonce_, contentLength_, isComplete_;
294+
@ ensures isComplete_ && contentLength_ >= 0;
295+
@ ensures Arrays.equalArrays(b, off, nonce_, 0, nonceLength_);
296+
@ ensures contentLength_ == Long.asLong(b[nLen+off], b[nLen+off+1], b[nLen+off+2],
297+
@ b[nLen+off+3], b[nLen+off+4], b[nLen+off+5],
298+
@ b[nLen+off+6], b[nLen+off+7]);
299+
@ ensures \result == nonceLength_ + Long.BYTES;
300+
@ signals_only BadCiphertextException;
301+
@ signals (BadCiphertextException) (contentLength_ < 0 && isComplete_ == \old(isComplete_)
302+
@ && Arrays.equalArrays(b, off, nonce_, 0, nonceLength_));
303+
@*/
304+
public int deserialize(/*@ nullable */ final byte[] b, final int off) {
164305
if (b == null) {
165306
return 0;
166307
}
167-
308+
309+
//@ assert b != null;
168310
int parsedBytes = 0;
169311
try {
170312
if (nonceLength_ > 0 && nonce_ == null) {
@@ -192,6 +334,9 @@ public int deserialize(final byte[] b, final int off) {
192334
* true if this object containing the single block header fields
193335
* is complete; false otherwise.
194336
*/
337+
//@ public normal_behavior
338+
//@ ensures \result == isComplete_;
339+
//@ pure
195340
public boolean isComplete() {
196341
return isComplete_;
197342
}
@@ -202,6 +347,17 @@ public boolean isComplete() {
202347
* @return
203348
* the bytes containing the nonce set in the single block header.
204349
*/
350+
//@ public normal_behavior
351+
//@ requires nonce_ == null;
352+
//@ ensures \result == null;
353+
//@ also public normal_behavior
354+
//@ requires nonce_ != null;
355+
//@ ensures \result != null;
356+
//@ ensures \fresh(\result);
357+
//@ ensures \result != null;
358+
//@ ensures \result.length == nonce_.length;
359+
//@ ensures java.util.Arrays.equalArrays(\result,nonce_);
360+
//@ pure nullable
205361
public byte[] getNonce() {
206362
return nonce_ != null ? nonce_.clone() : null;
207363
}
@@ -212,6 +368,9 @@ public byte[] getNonce() {
212368
* @return
213369
* the content length set in the single block header.
214370
*/
371+
//@ public normal_behavior
372+
//@ ensures \result == contentLength_;
373+
//@ pure
215374
public long getContentLength() {
216375
return contentLength_;
217376
}
@@ -224,7 +383,11 @@ public long getContentLength() {
224383
* the length of the nonce used in the encryption of the content
225384
* stored in the single block.
226385
*/
386+
//@ public normal_behavior
387+
//@ requires nonceLength >= 0;
388+
//@ assignable nonceLength_;
389+
//@ ensures nonceLength_ == nonceLength;
227390
public void setNonceLength(final short nonceLength) {
228391
nonceLength_ = nonceLength;
229392
}
230-
}
393+
}

0 commit comments

Comments
 (0)