Verify message-header serialization and deserialization #47

RustanLeino · 2019-09-28T04:37:54Z

Description of changes:

This PR brings in the serialization and deserialization of message headers,
with specifications, implementations, and proof of correctness.

The previous version had not been fully verified. It had been written with
AAD as array of pairs of byte arrays. This had led to many tricky issues with
framing. The new version instead uses a sequence of pairs of byte sequences,
matching what the CMM and Keyring part of this ESDK does.

This new version also uses Dafny's new error-handling assignment, :-,
which drastically reduces the number of source lines needed to serialize
and deserialize (in one place reducing 90 lines to 10). This was enabled
by changing return types to use Result<A> instead of Either<A,Error>.

Finally, the code has been reformatted to adhere to the Dafny style guide.

Organization of changes:

This is a large PR, containing 8 sequentially dependent commits. To have
made those commits independent of each other would have been difficult, and
later trying to incorporate PR review comments for a particular commit
and then keeping up with merges would have been very difficult. So, instead
I plan to act on any PR review comments in further commits, so that all
of these changes can be processed at once.

To review the changes, you can either look at each commit separately or
just look at the final code. For anyone lacking familiarity with the
original code, I think reading the final code makes more sense.

Testing and verification:

The code all verifies and compiles with make all in about 4 minutes.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

* Remove `noverif` build target, since it duplicates `build`. * Update .PHONY target. * Add SRCS_DONT_VERIFY (which is empty for now).

Mostly indentation changes. Capitalize method names.

Include AAD Length in AAD Validity. Corrected definition of AAD Length to include the two bytes that record the number of key/value pairs. State and prove some needed lemmas.

Include SDK/MessageHeader/*.dfy in build, fixing up renamed definitions and adding temporary Assume calls to silence verifier. Include Util/Streams.dfy and Util/UTF8.dfy. Add make target buildcs, which only calls C# compiler (on the Main.cs in the file system). The DEPS and DEPS_CS targets should be merged as some point. Remove call to deprecated Util.BigIntegerToInt in Arrays-extern.cs. Add Client.dfy file. Define EncryptionContextKeys and ReservedKeyValues in Materials.dfy.

This change also eliminated the need for `reads` clauses and many of its supporting `Repr...` functions.

MatthewBennington

Looks like the branch isn't building right now. I left a few comments, but I think this will take a couple of passes to fully grok.

MatthewBennington · 2019-09-30T15:56:27Z

Makefile

@@ -17,27 +17,42 @@ SRCS = \
 	   src/Crypto/Signature.dfy \
 	   src/Main.dfy \
 	   src/SDK/AlgorithmSuite.dfy \
+	   src/SDK/Client.dfy \


This causes the build to fail on my machine. Looks like a file didn't get commited?

Indeed. I'll remove this line, since the file Client.dfy doesn't contribute to this PR. I'll add it as a separate PR later.

MatthewBennington · 2019-09-30T16:32:20Z

src/SDK/MessageHeader/Definitions.dfy

+  type T_Reserved              = x: seq<uint8> | x == [0,0,0,0] witness [0,0,0,0]
+  datatype T_ContentType       = NonFramed | Framed
+  type EncCtx                  = Materials.EncryptionContext
+  type T_AAD                   = EncCtx


It appears these lines create nested type synonyms. What is the rational for doing this instead of using the same type over and over?

I was just following and evolving the previous T_* types. I agree it would be better to remove the synonyms EncCtx and T_AAD.

MatthewBennington · 2019-09-30T16:34:09Z

src/SDK/MessageHeader/Definitions.dfy

-                                frameLength: uint32)
+  datatype HeaderBody          = HeaderBody(
+                                   version: T_Version,
+                                   typ: T_Type,


typ

Is this a typo? Or are there issues with having a field named type?

type is a keyword in Dafny.

MatthewBennington · 2019-09-30T16:46:35Z

src/SDK/MessageHeader/Serialize.dfy

-        reveal ValidHeaderBody();
-        reveal ValidAAD();
-        reveal ValidEncryptedDataKeys();
-        {


Removing all this boilerplate error handling is a win.

Remove Client.dfy from Makefile (since Client.dfy isn't part of this PR) Remove the type synonyms `EncCtx` and `T_ADD` in MessageHeader/Definitions.dfy, which stand for `Materials.EncryptionContext`.

lavaleri

Partial review.

Makefile

src/SDK/AlgorithmSuite.dfy

lavaleri · 2019-10-01T19:42:23Z

src/SDK/Materials.dfy

@@ -10,11 +10,25 @@ module Materials {

  type EncryptionContext = seq<(seq<uint8>, seq<uint8>)>

+
+  function method EncryptionContextKeys(encryptionContext: EncryptionContext): set<seq<uint8>> {


This name should be clearer. GetKeysFromEncryptionContext? Is there a more conventional way in dafny to get keys in something that looks like a map, or does a new function like this need to be defined for each specific type that you define?

I renamed it. We should consider using a map in a later PR.

lavaleri · 2019-10-01T19:44:33Z

src/SDK/Materials.dfy


  datatype EncryptedDataKey = EncryptedDataKey(providerID : string,
                                               providerInfo : seq<uint8>,
                                               ciphertext : seq<uint8>)
+  {
+    predicate Valid() {
+      StringIs8Bit(providerID) &&


We should drill down on how this repo will represent/validate UTF8.

Yes. Let's do that in a separate PR. Very few things are still string.

src/SDK/MessageHeader/Definitions.dfy

src/SDK/MessageHeader/MessageHeader.dfy

lavaleri · 2019-10-01T20:50:53Z

src/SDK/Materials.dfy

@@ -10,11 +10,25 @@ module Materials {

  type EncryptionContext = seq<(seq<uint8>, seq<uint8>)>


From meeting: To follow the spec, this should be a map<seq<uint8>, seq<uint8>>., with a wrapping datatype with functions like GetSortedKeyValues and Add, and a Valid() predicate.

Additionally we need to update to ensure it is valid UTF8 encoding, and sort according to UTF8 binary representation.

Validity does ensure it's UTF8. I added sorting upon deserialization.

Let's do the conversion to map and wrapping in a datatype with members in a separate PR.

Fix deserialization of header authentication (first IV, then authTag). Change HeaderAuthentication datatype to use seq instead of array.

Change definition of Header as a class (in MessageHeader.dfy) to a datatype (in Definitions.dfy). Define ValidHeader (in Validity.dfy). Simplify specification of method SerializeHeaderBody (in Serialize.dfy). Rewrite Serialize and Deserialize methods (in MessageHeader.dfy) to use standard error reporting (using type `Result`).

lavaleri

Note that the src/Util/* files were reviewed only for style changes. Complete reviews of those files will have to be completed as part of a seperate issue.

Finally, before this is approved we should test it with some test vectors.

lavaleri · 2019-10-01T21:36:24Z

src/SDK/MessageHeader/Deserialize.dfy

-                }
-            case Right(e) => return Right(e);
-        }
+  import opened Definitions


We should be wary of importing anything but stdlibrary things opened. What from Definitions are we using? Does this belong in a seperate file and how cumbersome would it be to not import this opened?

We can discuss this further, but I felt that those things defined in Definitions.dfy were so universal to all of the src/SDK/MessageHeader files that I allowed myself to import them as opened.

No, you're right. We should stick to our rule. I changed it and I think it looks better. I used the local names Msg and V for the imported modules Definitions and Validity.

src/SDK/MessageHeader/Deserialize.dfy

lavaleri · 2019-10-01T21:43:44Z

src/SDK/MessageHeader/Deserialize.dfy

+    ensures is.Valid()
+  {
+    var version :- Utils.ReadFixedLengthFromStreamOrFail(is, 1);
+    if version[0] == 0x01 {


We should pull 0x01 into a constant. Or even more appropriate is to verify that it is the T_Version datatype.

The latter happens on line 38, where it's being cast to a Version. For this case, I feel okay with leaving the 0x01 as is, since "version 1" seems so very close to 0x01.

lavaleri · 2019-10-01T21:44:14Z

src/SDK/MessageHeader/Deserialize.dfy

+    ensures is.Valid()
+  {
+    var typ :- Utils.ReadFixedLengthFromStreamOrFail(is, 1);
+    if typ[0] == 0x80 {


Same here, we should verify that this value is valid T_Type, not compare against a constant.

The cast to a Type happens. But perhaps we want a constant here?

Ugh! I tried a constant, but there are some aesthetics issues. Lets discuss in person.

lavaleri · 2019-10-01T21:47:44Z

src/SDK/MessageHeader/Deserialize.dfy

+    modifies is
+    ensures is.Valid()
+    ensures match ret
+      case Success(algorithmSuiteID) => ValidAlgorithmID(algorithmSuiteID)


Is this needed? Is there anyway for something of type AlgorithmSuite.ID to not be ValidAlgorithmID?

As these are defined in AlgorithmSuite now, there could be a difference between the keys of the map Suite and the allowed values of an ID. Maybe we should address that there (in AlgorithmSuite.dfy)?

lavaleri · 2019-10-01T23:14:32Z

src/SDK/MessageHeader/Utils.dfy

-    {
-        forall j :: 0 < j < n ==> lexCmpArrays(a[j-1].0, a[j].0, ltByte)
-    }
+  predicate SortedKVPairsUpTo(a: seq<(seq<uint8>, seq<uint8>)>, n: nat)


The KV pair methods should be a part of messageHeader serialization validity, not this file.

lavaleri · 2019-10-01T23:16:18Z

src/SDK/MessageHeader/Validity.dfy

+  /*
+   * Validity of the message header
+   * The validity depends on predicates and on the types of the fields
+   */


Let me know if I am wrong, but the "dafny" way to do this is to have the validity alongside where we actually define these things. i.e. we should move this logic into the files where we actually reference these fields and structures.

lavaleri · 2019-10-01T23:17:23Z

src/SDK/MessageHeader/Validity.dfy

+  // TODO: strengthen spec when available
+  predicate UniquelyIdentifiesMessage(id: T_MessageID)      { true }
+  predicate WeaklyBindsHeaderToHeaderBody(id: T_MessageID)  { true }
+  predicate EnablesSecureReuse(id: T_MessageID)             { true }
+  predicate ProtectsAgainstAccidentalReuse(id: T_MessageID) { true }
+  predicate ProtectsAgainstWearingOut(id: T_MessageID)      { true }


We should remove these unless we think we have a path forward for implementing them soon. Otherwise, elsewhere in the code where these are referenced we might give ourselves false confidence about what we are actually proving.

lavaleri · 2019-10-01T23:19:16Z

src/SDK/MessageHeader/Validity.dfy

+  predicate {:opaque} ValidEncryptedDataKeys(encryptedDataKeys: T_EncryptedDataKeys) {
+    && |encryptedDataKeys.entries| < UINT16_LIMIT
+    && (forall i :: 0 <= i < |encryptedDataKeys.entries| ==> encryptedDataKeys.entries[i].Valid())
+    // TODO: well-formedness of EDK


What work do we think is missing here? Or can we remove this TODO?

lavaleri · 2019-10-01T23:23:49Z

src/SDK/MessageHeader/SerializeAAD.dfy

+
+  // ----- Specification -----
+
+  function SerializeAAD(kvPairs: Materials.EncryptionContext): seq<uint8>


We need to enforce that the AAD is serialized in canonical form.

Remove postcondition of AlgorithmSuite.ID.KeyLength. Rename EncryptionContextKeys(...) to GetKeysFromEncryptionContext(...). Remove EDKEntry type synonym. Remove T_ prefix of all types in MessagerHeader/Definitions.dfy. Add constant MESSAGE_ID_LEN, used in type MessageId. Remove the short-lived SRCS_DONT_VERIFY from Makefile.

Don't `import opened` for `MessageHeader.Definitions` and `MessageHeaderValidity` (instead, I used the local names `Msg` and `V`, respectively). This caused the need for some other imports that previously had been available via these opened imports.

Remove Deserialize.IsValidMsgID. Rename *Id to *ID. Remove lemma UTF8.ValidUTF8ArraySeq (and also change Deserialize.DeserializeUTF8 to return a seq, since that's what all call sites need). Rename LexCmpSeqs to LexicographicLessOrEqual, and add some descriptive comments.

Add VERSION_1 and TYPE_CUSTOMER_AED. Change base type of Version and Type to uint8. Add conversion functions ContentTypeToUInt8 and UInt8ToContentType, and an associated correctness lemma.

Note, the names of some routines are not yet style-guide compliant. Also, improve some definitions, especially using Dafny's sequence constructor instead of recursive function definitions. Removed some routines that are no longer used (there may be others that are unused, too).

Remove Stream trait, because the commonality between StringReader and StringWriter is rather superficial. Make StringReader.data field a `const`. Add to StringReader the methods ReadSeq, ReadExact, and ReadUInt16. Remove ReadFixedLengthFromStreamOrFail and various commented-out methods from MessageHeader/Utils.dfy. Use the new Read* methods in Deserialize.dfy.

This commit only does this renaming, but it touches many lines. Old names were `is` and `os`. Not only are these overloaded in computer-science speak, but `rd` and `wr` are more straightforward in the first place.

Combine contents of Definitions.dfy, Validity.dfy, and Utils.dfy into Format.dfy. Combine contents of Serialize.dfy, SerializeAAD.dfy, and SerializeEDK.dfy into Serialize.dfy. No other changes were made. In particular, this commit does not change the names of modules.

Combine Definitions, Validity, and Utils into Format. Combine Serialize, SerializeAAD, and SerializeEDK into Serialize. Changed predicates ValidXYZ() into a member predicate Valid() of datatype XYZ, when possible. Two things left for future improvements: * Some ValidXYZ() predicates were previous marked as {:opaque} and required a `reveal` to obtain the definition. These {:opaque} annotations seem to have no effect when Valid() is a member of type XYZ. Such support is probably forthcoming in a future version of Dafny, but for now, everything verifies without needing the definitions to be {:opaque}. * As a shorter local name when importing Format, I continued to use `Msg`. Perhaps we should change this in the future (perhaps to `F`?).

src/SDK/MessageHeader/Deserialize.dfy

lavaleri · 2019-10-04T17:43:22Z

src/SDK/MessageHeader/Deserialize.dfy

+      case Success(edks) => edks.Valid()
+      case Failure(_) => true
+  {
+    //reveal Msg.EncryptedDataKeys.Valid();


remove comment

lavaleri · 2019-10-04T17:51:04Z

src/SDK/MessageHeader/Deserialize.dfy

+    return Success(msgID);
+  }
+
+  method DeserializeUTF8(rd: Streams.StringReader, n: nat) returns (ret: Result<seq<uint8>>)


Does this method actually belong in Stream.dfy?

lavaleri · 2019-10-04T17:57:39Z

src/SDK/MessageHeader/Deserialize.dfy

+    ensures rd.Valid()
+    modifies rd
+    ensures match ret
+      case Success(ivLength) => Msg.ValidIVLength(ivLength, algorithmSuiteID)


Should this method contain this validation logic? Or should whatever is calling this method need to ensure this property?

lavaleri · 2019-10-04T17:58:16Z

src/SDK/MessageHeader/Deserialize.dfy

+    modifies rd
+    ensures rd.Valid()
+    ensures match ret
+      case Success(frameLength) => Msg.ValidFrameLength(frameLength, contentType)


Same here, I'm not sure this is exactly structured the way we want it to be.

lavaleri · 2019-10-04T19:10:15Z

src/SDK/MessageHeader/Serialize.dfy

+  import opened UInt = StandardLibrary.UInt
+  import Materials
+
+  function {:opaque} Serialize(hb: Msg.HeaderBody): seq<uint8>


This should be named more clearly.

lavaleri · 2019-10-04T19:11:11Z

src/SDK/MessageHeader/Serialize.dfy

+    len :- wr.WriteSimpleSeq(hb.messageID);
+    totalWritten := totalWritten + len;
+
+    //reveal Msg.HeaderBody.Valid();


lavaleri · 2019-10-04T19:21:57Z

src/SDK/MessageHeader/Serialize.dfy

+  function SerializeEDKs(encryptedDataKeys: Msg.EncryptedDataKeys): seq<uint8>
+    requires encryptedDataKeys.Valid()
+  {
+    //reveal Msg.EncryptedDataKeys.Valid();


remove comment

lavaleri · 2019-10-04T19:30:40Z

src/SDK/MessageHeader/Serialize.dfy

+        && wr.data == old(wr.data) + serEDK
+      case Failure(e) => true
+  {
+    //reveal Msg.EncryptedDataKeys.Valid();


remove comment

lavaleri · 2019-10-04T19:35:11Z

src/SDK/MessageHeader/Serialize.dfy

+      bytes := UInt16ToArray(|entry.providerInfo| as uint16);
+      len :- wr.WriteSimple(bytes);
+      totalWritten := totalWritten + len;


We are reusing this pattern constantly throughout this PR. Is there any way to make it cleaner/shorter? I'd like to avoid using the same bytes and len variables within the same function. It's fine as is, but I'm not sure this is a pattern we want to encourage. Thoughts?

AlgorithmSuite related: * Rename validIDs to ValidIDs. * Add lemmas SuiteIsComplete and ValidIDsAreSuiteKeys, to state and check the intention that map Suite contains an entry for every ID. * Remove predicate ValidAlgorithmID, which is really just `true`. * Added members IVLength() and TagLength() to type ID. MessageHeader: * Fix specification of ValidFrameLength. * Remove ValidMessageID and its 5 companion predicates, all of which were and would always have remained `true`. * Move contents of HeaderAuthentication.Valid into its enclosing type, Header. Deserialize: * Add export declaration in Deserialize to make helper routines private. * Perform inter-field checks after reading (for IV Length and Frame Length). StringReader: * Add methods ReadByte and ReadUInt32. * Rename out-parameter `ret` to `res`. StringWriter: * Change Capacity() to HasRemainingCapacity(n), because the previous Capacity() == 0 caused the StringWriter never to write anything. Even the new HasRemainingCapacity(n) is rather meaningless at this time, but it least it allows writing. * Remove non-...Simple... methods, and rename ...Simple... methods to names without "Simple". * Add methods WriteUInt16 and WriteUInt32 (implementations can be made more efficient later). General: * Remove {:opaque} and reveal annotations where they are not needed. * Remove two stale TODO comments.

First of two steps: Remove existing MessageHeader.dfy file.

Second of two steps, in src/SDK/MessageHeader: Rename Format.dfy to MessageHeader.dfy. Move/rename modules: * MessageHeader.Format -> MessageHeader * MessageHeader.Deserialize -> Deserialize * MessageHeader.Serialize -> Serialize Move InsertNewEntry method from MessageHeader into Deserialize. Move serialization specification functions into MessageHeader module. Change name of SerializeXYZ functions to XYZToSeq. Remove "Impl" from the names of Serialize methods.

src/SDK/AlgorithmSuite.dfy

MatthewBennington · 2019-10-07T15:39:13Z

src/SDK/MessageHeader/MessageHeader.dfy

+    && AADLength(kvPairs) < UINT16_LIMIT
+  }
+
+  predicate ValidIVLength(ivLength: uint8, algorithmSuiteID: AlgorithmSuite.ID) {


This should probably live in AlgorithmSuite.dfy

So this might be exceedingly pedantic, but the question this predicate should be answering is: "does the value of IVLength field in the message header match the IVLength of the AlgorithmSuiteID in the header", not "is this a valid IVLength for this algorithmSuite". If we were answering the latter, then yes, I agree that belongs in AlgorithmSuite.dfy. However, I think this belongs here if we are answering the former. Maybe a more appropriate place for this is actually to move this into the MessageHeader dataType, and use the datatype's IVLength and AlgorithmSuiteID fields. Thoughts?

I inlined ValidIVLength(...) into the one place where it was used, HeaderBody.Valid().

MatthewBennington · 2019-10-07T15:55:10Z

src/Util/Streams.dfy

-        var n := min(req, available());
+      if off == arr.Length || Available() == 0 {
+        assert (min (req, Available())) == 0;
+        return Success(0);


Should probably ensure unchanged for this return path.

For consistency with the other methods, I suppose, or maybe to be more easily adaptable to streams that don't read from memory? Parameter req seems misnamed, since it indicates a desired, not required, number of bytes to be read.

I will rename the parameter and change the return type to remove the possibility of failure.

Ignore my comment, which was intended for the item below.

Instead, I removed the if statement in the code.

MatthewBennington · 2019-10-07T15:58:29Z

src/Util/Streams.dfy

-    // TODO add a version without arrays
-    method ReadSimple(arr: array<uint8>) returns (res: Result<nat>)
+
+    method ReadSeq(req: nat) returns (res: Result<seq<uint8>>)


There doesn't appear to be a way for this method to fail, why is it returning a Result?

For consistency with the other methods, I suppose, or maybe to be more easily adaptable to streams that don't read from memory? Parameter req seems misnamed, since it indicates a desired, not required, number of bytes to be read.

I will rename the parameter and change the return type to remove the possibility of failure.

src/SDK/MessageHeader/Deserialize.dfy

MatthewBennington · 2019-10-07T16:32:27Z

src/SDK/MessageHeader/Deserialize.dfy

+    ensures is.Valid()
+  {
+    var reserved :- Utils.ReadFixedLengthFromStreamOrFail(is, 4);
+    if reserved[0] == reserved[1] == reserved[2] == reserved[3] == 0 {


if reserved == [0, 0, 0, 0]?

MatthewBennington · 2019-10-07T16:36:50Z

src/SDK/MessageHeader/Deserialize.dfy

+    var frameLength :- rd.ReadUInt32();
+
+    // inter-field checks
+    if ivLength != AlgorithmSuite.Suite[algorithmSuiteID].params.ivLen {


Move ValidIVLength() to StandardLibrary, and use it here.

Because this is logic specific to the ESDK data format, this shouldn't belong in the StandardLibrary. However I agree that we should reuse Msg.ValidIVLength here instead of duplicating the logic. That way, if we need to add new conditions to IV Length Validity, those new conditions are also checked here, which will always be the behavior we want.

I changed line 284 to use the IVLength() member function of type AlgorithmSuite.ID.

The web page is not giving me a Reply field for Matt's comment about reserved == [0, 0, 0, 0], so I'll write my reply here. I prefer the existing code, since it will be more efficient at run time. (The expression [0, 0, 0, 0] will allocate a sequence in the underlying compiled code, which seems unnecessary here.)

MatthewBennington · 2019-10-07T16:41:39Z

src/SDK/MessageHeader/Deserialize.dfy

+    return Success(hb);
+  }
+
+  method DeserializeHeaderAuthentication(rd: Streams.StringReader, algorithmSuiteID: AlgorithmSuite.ID) returns (ret: Result<Msg.HeaderAuthentication>)


If we aren't checking authenticity during deserialization, when should we be checking it?

This is done by the client during decryption, and after deserialization of the message.

src/SDK/AlgorithmSuite.dfy

src/SDK/MessageHeader/Deserialize.dfy

lavaleri · 2019-10-07T20:49:35Z

src/SDK/MessageHeader/Deserialize.dfy

-  import Msg = Format
+module Deserialize {
+  export
+    provides DeserializeHeaderBody, DeserializeHeaderAuthentication


I think this module should provide a DeserializeHeader, which uses DeserializeHeaderBody and DeserializeHeaderAuthentication

Good idea. I added such a method and am exporting it instead of the other two.

src/SDK/MessageHeader/Deserialize.dfy

lavaleri · 2019-10-07T21:18:34Z

src/SDK/MessageHeader/Deserialize.dfy

+    var frameLength :- rd.ReadUInt32();
+
+    // inter-field checks
+    if ivLength != AlgorithmSuite.Suite[algorithmSuiteID].params.ivLen {


Because this is logic specific to the ESDK data format, this shouldn't belong in the StandardLibrary. However I agree that we should reuse Msg.ValidIVLength here instead of duplicating the logic. That way, if we need to add new conditions to IV Length Validity, those new conditions are also checked here, which will always be the behavior we want.

lavaleri · 2019-10-07T21:32:56Z

src/SDK/MessageHeader/MessageHeader.dfy

 include "../AlgorithmSuite.dfy"
+
 include "../../Util/Streams.dfy"
 include "../../StandardLibrary/StandardLibrary.dfy"

 module MessageHeader {


I like this restructuring. One final comment is that we should move these files out of the MessageHeader directory.

lavaleri · 2019-10-07T21:42:29Z

src/SDK/MessageHeader/MessageHeader.dfy

+      2 + |kvPairs[hi - 1].1|
+  }
+
+  lemma KVPairsLengthSplit(kvPairs: Materials.EncryptionContext, lo: nat, mid: nat, hi: nat)


It's not obvious to me why the following KVPair lemmas are necessary. What exactly are the prupose of these lemmas? Are they used to prove anything more concrete, or do we need confidence that KVPairsLength actually has these properties?

Lemma KVPairsLengthSplit is needed in `Serialize.ComputeAADLength.

Lemma KVPairsLengthInsert is needed in Deserialize.DeserializeAAD, and makes use of lemmas KVPairsLengthPrefix and KVPairsLengthExtend in its proof.

Lemma KVPairsLengthCorrect is used in the proof of ADDLengthCorrect, whose purpose is to prove that AADToSeq and AADLength are related in the expected way.

src/SDK/MessageHeader/MessageHeader.dfy

lavaleri · 2019-10-07T21:52:49Z

src/SDK/MessageHeader/MessageHeader.dfy

+    && AADLength(kvPairs) < UINT16_LIMIT
+  }
+
+  predicate ValidIVLength(ivLength: uint8, algorithmSuiteID: AlgorithmSuite.ID) {


So this might be exceedingly pedantic, but the question this predicate should be answering is: "does the value of IVLength field in the message header match the IVLength of the AlgorithmSuiteID in the header", not "is this a valid IVLength for this algorithmSuite". If we were answering the latter, then yes, I agree that belongs in AlgorithmSuite.dfy. However, I think this belongs here if we are answering the former. Maybe a more appropriate place for this is actually to move this into the MessageHeader dataType, and use the datatype's IVLength and AlgorithmSuiteID fields. Thoughts?

src/Util/Streams.dfy

lavaleri · 2019-10-07T22:34:13Z

src/SDK/MessageHeader/MessageHeader.dfy

+
+  datatype EncryptedDataKeys = EncryptedDataKeys(entries: seq<Materials.EncryptedDataKey>)
+  {
+    predicate Valid() {


Additionally, MUST be greater than 0. i.e. a message header isn't valid unless it contains at least one edk.

Move files from src/SDK/MessageHeader/ to src/SDK/. Rename constant ValidIDs to VALID_IDS. Simplify return value of StringReader.ReadSeq. Simplify logic of StringReader.Read. Add a TODO to StringWriter.HasRemainingCapacity. Add method Deserialize.DeserializeHeader, and export it in lieu of DeserializeHeaderBody and DeserializeHeaderAuthentication. Moved DeserializeHeaderBody and DeserializeHeaderAuthentication closer to the top of file Deserialize.dfy (no change of those methods). Inline and then remove ValidIVLength predicate. Add `0 < |entries|` to EncryptedDataKeys.Valid().

lavaleri

There are still a couple places where I'm unsure whether reducing duplication of predicate logic is the correct thing or not, but there is enough value in the rest of this PR that I see those issues as non-blocking. LGTM.

RustanLeino added 8 commits September 27, 2019 21:09

Enhance Makefile

31e4e7e

* Remove `noverif` build target, since it duplicates `build`. * Update .PHONY target. * Add SRCS_DONT_VERIFY (which is empty for now).

Use Result type instead of Either

e3595d8

Reformat code according to Dafny style guide

bfca9c7

Mostly indentation changes. Capitalize method names.

Use :- error-handling assignment

8a53935

Make serialization and deserialization verify

5915688

Include AAD Length in AAD Validity. Corrected definition of AAD Length to include the two bytes that record the number of key/value pairs. State and prove some needed lemmas.

Remove special data structure for an empty AAD

a73b6dd

Change MessageHeader to use seq instead of array

8080e8a

This change also eliminated the need for `reads` clauses and many of its supporting `Repr...` functions.

MatthewBennington suggested changes Sep 30, 2019

View reviewed changes

Revise according to @MatthewBennington's comments

3997d30

Remove Client.dfy from Makefile (since Client.dfy isn't part of this PR) Remove the type synonyms `EncCtx` and `T_ADD` in MessageHeader/Definitions.dfy, which stand for `Materials.EncryptionContext`.

lavaleri suggested changes Oct 1, 2019

View reviewed changes

lavaleri reviewed Oct 1, 2019

View reviewed changes

RustanLeino added 2 commits October 1, 2019 16:18

Specify validity of authentication header

737ff25

Fix deserialization of header authentication (first IV, then authTag). Change HeaderAuthentication datatype to use seq instead of array.

lavaleri suggested changes Oct 1, 2019

View reviewed changes

RustanLeino added 8 commits October 1, 2019 21:24

Fail deserialization on duplicate keys, not on unsorted input

4ab103d

Eliminate import opened

68580be

Don't `import opened` for `MessageHeader.Definitions` and `MessageHeaderValidity` (instead, I used the local names `Msg` and `V`, respectively). This caused the need for some other imports that previously had been available via these opened imports.

Name magic constants

781ca5c

Add VERSION_1 and TYPE_CUSTOMER_AED. Change base type of Version and Type to uint8. Add conversion functions ContentTypeToUInt8 and UInt8ToContentType, and an associated correctness lemma.

Rename variables that hold String{Reader,Writer} to rd, wr

a7d33ea

This commit only does this renaming, but it touches many lines. Old names were `is` and `os`. Not only are these overloaded in computer-science speak, but `rd` and `wr` are more straightforward in the first place.

MatthewBennington mentioned this pull request Oct 3, 2019

Refactoring AES crypto code #56

Merged

MatthewBennington previously approved these changes Oct 3, 2019

View reviewed changes

RustanLeino dismissed MatthewBennington’s stale review via 7c2036b October 3, 2019 19:09

lavaleri suggested changes Oct 4, 2019

View reviewed changes

RustanLeino added 2 commits October 4, 2019 17:30

Refactor as per PR comments

d218053

First of two steps: Remove existing MessageHeader.dfy file.

MatthewBennington reviewed Oct 7, 2019

View reviewed changes

lavaleri suggested changes Oct 7, 2019

View reviewed changes

lavaleri reviewed Oct 7, 2019

View reviewed changes

lavaleri approved these changes Oct 8, 2019

View reviewed changes

RustanLeino merged commit 9c7924f into aws:develop Oct 8, 2019

RustanLeino deleted the verifying-message-header branch October 8, 2019 21:47

lavaleri mentioned this pull request Oct 11, 2019

Review Intern SDK work #19

Closed

josecorella pushed a commit to josecorella/aws-encryption-sdk-dafny that referenced this pull request Oct 11, 2023

feat: add roundtrip ensures clause to Encode (aws#47)

d7cc56e

josecorella pushed a commit that referenced this pull request Oct 11, 2023

feat: add roundtrip ensures clause to Encode (#47)

f1ec5c3

josecorella pushed a commit that referenced this pull request Oct 11, 2023

feat: add roundtrip ensures clause to Encode (#47)

9996350

josecorella pushed a commit that referenced this pull request Oct 11, 2023

feat: add roundtrip ensures clause to Encode (#47)

373caca

		@@ -10,11 +10,25 @@ module Materials {

		type EncryptionContext = seq<(seq<uint8>, seq<uint8>)>


		function method EncryptionContextKeys(encryptionContext: EncryptionContext): set<seq<uint8>> {


		// ----- Specification -----

		function SerializeAAD(kvPairs: Materials.EncryptionContext): seq<uint8>

Verify message-header serialization and deserialization #47

Verify message-header serialization and deserialization #47

Conversation

RustanLeino commented Sep 28, 2019

MatthewBennington left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lavaleri left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lavaleri left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lavaleri left a comment

Choose a reason for hiding this comment