Outline Proof Correctness Message Body #237

WouterSchols · 2020-03-20T22:05:47Z

feat(MessageBody): Added outline proving correctness EncryptMessageBody body. Includes all requirements, expected function definitions. Avoids arithmetic problems in EncryptMessageBody method

Includes all requirements, expected function definitions. Avoids arithmetic problems in EncryptMessageBody method

lavaleri · 2020-03-20T22:11:26Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: 35e6058
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

lavaleri

Great job so far interpreting the spec! The one big issue that needs to be fixed is the fact that frameLength isn't the length of the serialized frame (I know, bad name), but instead the length of the plaintext that is encrypted by that frame. That has some implications on what we are able to verify here because we can't assume that the encrypted content will have the same length as the plaintext.

If there is anywhere in the spec that is misleading on that point, please point it out so we can fix it.

src/SDK/MessageBody.dfy

lavaleri · 2020-03-24T21:38:49Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: 8ef5257
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

lavaleri · 2020-03-24T21:40:06Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: 116956c
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

Export does not support exporting predicates from datatypes. This will cause errors if the methods are called outside of the module.

lavaleri · 2020-03-25T18:04:12Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: 2be9ca7
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

lavaleri · 2020-03-27T00:22:36Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: cf0fbba
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

feat: Added draft of postconditions DecryptFrame

lavaleri · 2020-03-27T23:01:46Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: 90a01a6
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

fix: Finished the proof of DecryptFrame method

lavaleri · 2020-03-27T23:25:30Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: 176cd5b
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

feat: Proved all post conditions of MessageBody

lavaleri · 2020-03-28T01:05:38Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: f06c51b
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

lavaleri · 2020-03-28T01:09:21Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: a085df7
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

feat: Small strengtening encrypt post conditions

lavaleri · 2020-03-30T17:31:27Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: 89207e8
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

fix: Moved EncryptMock and DecryptMock yo AESEncryption

lavaleri · 2020-03-31T17:50:18Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: 8049dfb
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

fix:Added export back

lavaleri · 2020-04-13T19:35:41Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: 2f8140c
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

lavaleri · 2020-04-13T21:19:22Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: 5eb44d2
Result: FAILED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

lavaleri · 2020-04-13T22:11:34Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: 22c32df
Result: SUCCEEDED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

lavaleri

Finished review of Frame Decrypt operations.

Good job so far! The major things are I think we can still improve on readability by thinking about the names of ghosts a bit more. Finally, I just noticed that we are lacking unit tests here. Since this PR will change behavior (even if very slightly), it shouldn't go in until we have the framed encrypt/decrypt behavior covered by unit tests. I will ask team how we want to go forward with this.

src/SDK/MessageBody.dfy

lavaleri · 2020-04-13T23:29:33Z

src/SDK/MessageBody.dfy

    return Success(plaintext);
  }

+  datatype FrameWithGhostSeq = FrameWithGhostSeq(frame: Frame, ghost ciphertext: seq<uint8>)


Creating a new datatype to pair these together makes sense, but we should think about the name a bit. This is a thing that contains the ghost Frame representation of the data, and then that same data, but serialized and compiled into a seq. @RustanLeino Is there any idiom for naming a thing which is paired with some ghost representation of itself?

There's no such naming convention that I know of. Whatever the name, we could add such a type to the standard library, in a generic way. For example:

datatype ExtendWithGhost<A, B> = ExtendWithGhost(a: A, ghost b: B)

The use of this type in Wouter's code gives us a way to return some ghost value along with the result. With language support, a better solution would be for Dafny to allow :- to be used with more than one out-parameter. I just submitted an Issue to request such a feature, dafny-lang/dafny#603.

lavaleri · 2020-04-13T23:36:06Z

src/SDK/MessageBody.dfy

+           var decryptedFrame := frameWithGhostSeq.frame;
+           var ciphertext := frameWithGhostSeq.ciphertext;
+           var final := decryptedFrame.FinalFrameConstructor?;


I would expect these to line up with the &&s. @RustanLeino do you have preferences on this styling?

src/SDK/MessageBody.dfy

chore: Added extra comments chore: General refactoring

lavaleri · 2020-04-17T23:11:23Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: 5b3959b
Result: SUCCEEDED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

lavaleri

file .vs/EncryptionSDK/v16/.suo should be removed from this PR
and one small fix

src/SDK/MessageBody.dfy

This reverts commit 5b3959b.

Chore: Updated comments and removed unwanted commit Chore: Changed sloppy error message removed unwanted file changes

lavaleri · 2020-04-22T22:09:45Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: a00840f
Result: SUCCEEDED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

lavaleri · 2020-04-22T22:10:57Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: dda2caa
Result: SUCCEEDED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

lavaleri

lgtm! Thanks for the great work here. Make sure that @acioc takes a look at the updated documentation/comments and his concerns are addressed before merging.

acioc

Overall, looks good. A few np's but blocking change is the expect

src/Crypto/AESEncryption.dfy

src/SDK/MessageBody.dfy

lavaleri · 2020-04-29T20:25:48Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: 2dfbe9d
Result: SUCCEEDED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

lavaleri · 2020-04-29T20:36:17Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: 54c17d8
Result: SUCCEEDED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

acioc

LGTM! Thanks!

lavaleri · 2020-04-29T20:36:39Z

AWS CodeBuild CI Report

CodeBuild project: DafnyESDK
Commit ID: be95895
Result: SUCCEEDED
Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

Outline Proof Correctness Message Body

35e6058

Includes all requirements, expected function definitions. Avoids arithmetic problems in EncryptMessageBody method

robin-aws requested review from robin-aws, RustanLeino, lavaleri and acioc March 20, 2020 22:13

lavaleri reviewed Mar 21, 2020

View reviewed changes

RustanLeino reviewed Mar 24, 2020

View reviewed changes

src/SDK/MessageBody.dfy Outdated Show resolved Hide resolved

wouter added 2 commits March 24, 2020 14:33

Finished the proofs of encryption methods

8ef5257

Small refactoring

116956c

Small refactoring and removed export

2be9ca7

Export does not support exporting predicates from datatypes. This will cause errors if the methods are called outside of the module.

Initial Work Deserialize

cf0fbba

wouter added 2 commits March 27, 2020 13:25

Work in progress on MessageBody

ddc3391

feat: Added draft of postconditions DecryptFrame

Work in progress messagebody

90a01a6

Added proof Decrypt Frame

176cd5b

fix: Finished the proof of DecryptFrame method

wouter added 2 commits March 27, 2020 18:00

Finished Encrypt MessageBody

f06c51b

feat: Proved all post conditions of MessageBody

Set stream file to the needed file which is not merged yet

a085df7

Update MessageBody.dfy

89207e8

feat: Small strengtening encrypt post conditions

Moved facts from Encryption to AESEncrypt

8049dfb

fix: Moved EncryptMock and DecryptMock yo AESEncryption

Added export provides back

f006e0b

fix:Added export back

Bugfixes

5eb44d2

Bugfix changes cs file to match names

22c32df

WouterSchols requested review from acioc and lavaleri April 13, 2020 22:13

lavaleri suggested changes Apr 14, 2020

View reviewed changes

Updated MessageBody based on PR feedback

5b3959b

chore: Added extra comments chore: General refactoring

lavaleri suggested changes Apr 22, 2020

View reviewed changes

src/SDK/MessageBody.dfy Outdated Show resolved Hide resolved

wouter and others added 3 commits April 22, 2020 14:52

Revert "Updated MessageBody based on PR feedback"

6ca910d

This reverts commit 5b3959b.

Updates based on comments

a00840f

Chore: Updated comments and removed unwanted commit Chore: Changed sloppy error message removed unwanted file changes

Merge branch 'develop' into Wouter

dda2caa

lavaleri previously approved these changes Apr 22, 2020

View reviewed changes

acioc suggested changes Apr 29, 2020

View reviewed changes

Removed expect statements

2dfbe9d

WouterSchols dismissed lavaleri’s stale review via 2dfbe9d April 29, 2020 20:09

Simple reformatting changes

be95895

WouterSchols requested review from acioc and lavaleri April 29, 2020 20:20

Merge branch 'develop' into Wouter

54c17d8

acioc approved these changes Apr 29, 2020

View reviewed changes

lavaleri approved these changes Apr 29, 2020

View reviewed changes

WouterSchols merged commit ff7f001 into aws:develop Apr 29, 2020

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Outline Proof Correctness Message Body #237

Outline Proof Correctness Message Body #237

WouterSchols commented Mar 20, 2020

lavaleri commented Mar 20, 2020

lavaleri left a comment

lavaleri commented Mar 24, 2020

lavaleri commented Mar 24, 2020

lavaleri commented Mar 25, 2020

lavaleri commented Mar 27, 2020

lavaleri commented Mar 27, 2020

lavaleri commented Mar 27, 2020

lavaleri commented Mar 28, 2020

lavaleri commented Mar 28, 2020

lavaleri commented Mar 30, 2020

lavaleri commented Mar 31, 2020

lavaleri commented Apr 13, 2020

lavaleri commented Apr 13, 2020

lavaleri commented Apr 13, 2020

lavaleri left a comment

lavaleri Apr 13, 2020

RustanLeino Apr 22, 2020

lavaleri Apr 13, 2020

lavaleri commented Apr 17, 2020

lavaleri left a comment •

edited

Loading

lavaleri commented Apr 22, 2020

lavaleri commented Apr 22, 2020

lavaleri left a comment

acioc left a comment

lavaleri commented Apr 29, 2020

lavaleri commented Apr 29, 2020

acioc left a comment

lavaleri commented Apr 29, 2020

Outline Proof Correctness Message Body #237

Outline Proof Correctness Message Body #237

Conversation

WouterSchols commented Mar 20, 2020

lavaleri commented Mar 20, 2020

AWS CodeBuild CI Report

lavaleri left a comment

Choose a reason for hiding this comment

lavaleri commented Mar 24, 2020

AWS CodeBuild CI Report

lavaleri commented Mar 24, 2020

AWS CodeBuild CI Report

lavaleri commented Mar 25, 2020

AWS CodeBuild CI Report

lavaleri commented Mar 27, 2020

AWS CodeBuild CI Report

lavaleri commented Mar 27, 2020

AWS CodeBuild CI Report

lavaleri commented Mar 27, 2020

AWS CodeBuild CI Report

lavaleri commented Mar 28, 2020

AWS CodeBuild CI Report

lavaleri commented Mar 28, 2020

AWS CodeBuild CI Report

lavaleri commented Mar 30, 2020

AWS CodeBuild CI Report

lavaleri commented Mar 31, 2020

AWS CodeBuild CI Report

lavaleri commented Apr 13, 2020

AWS CodeBuild CI Report

lavaleri commented Apr 13, 2020

AWS CodeBuild CI Report

lavaleri commented Apr 13, 2020

AWS CodeBuild CI Report

lavaleri left a comment

Choose a reason for hiding this comment

lavaleri Apr 13, 2020

Choose a reason for hiding this comment

RustanLeino Apr 22, 2020

Choose a reason for hiding this comment

lavaleri Apr 13, 2020

Choose a reason for hiding this comment

lavaleri commented Apr 17, 2020

AWS CodeBuild CI Report

lavaleri left a comment • edited Loading

Choose a reason for hiding this comment

lavaleri commented Apr 22, 2020

AWS CodeBuild CI Report

lavaleri commented Apr 22, 2020

AWS CodeBuild CI Report

lavaleri left a comment

Choose a reason for hiding this comment

acioc left a comment

Choose a reason for hiding this comment

lavaleri commented Apr 29, 2020

AWS CodeBuild CI Report

lavaleri commented Apr 29, 2020

AWS CodeBuild CI Report

acioc left a comment

Choose a reason for hiding this comment

lavaleri commented Apr 29, 2020

AWS CodeBuild CI Report

lavaleri left a comment •

edited

Loading