Verify message-header serialization and deserialization

Makefile

@@ -19,14 +19,19 @@ SRCS = \
 	   src/SDK/AlgorithmSuite.dfy \
 	   src/SDK/CMM/DefaultCMM.dfy \
 	   src/SDK/CMM/Defs.dfy \
+	   src/SDK/Deserialize.dfy \
 	   src/SDK/Keyring/AESKeyring.dfy \
 	   src/SDK/Keyring/Defs.dfy \
 	   src/SDK/Keyring/RSAKeyring.dfy \
 	   src/SDK/Materials.dfy \
+	   src/SDK/MessageHeader.dfy \
+	   src/SDK/Serialize.dfy \
 	   src/SDK/ToyClient.dfy \
 	   src/StandardLibrary/Base64.dfy \
 	   src/StandardLibrary/StandardLibrary.dfy \
 	   src/StandardLibrary/UInt.dfy \
+	   src/Util/Streams.dfy \
+	   src/Util/UTF8.dfy \
 
 SRCV = $(patsubst src/%.dfy, build/%.dfy.verified, $(SRCS))
 
@@ -37,7 +42,9 @@ SRCDIRS = $(dir $(SRCS))
 DEPS = $(foreach dir, $(SRCDIRS), $(wildcard $(dir)/*.cs)) \
 	$(BCDLL)
 
-.PHONY: all hkdf test noverif clean-build clean
+DEPS_CS = $(foreach dir, src/Crypto/ src/ src/SDK/ src/SDK/CMM src/SDK/Keyring src/StandardLibrary src/Util, $(wildcard $(dir)/*.cs))
+
+.PHONY: all release build verify buildcs hkdf test clean-build clean
 
 all: verify build test
 
@@ -53,6 +60,9 @@ build/%.dfy.verified: src/%.dfy
 build/Main.exe: $(SRCS) $(DEPS)
 	$(DAFNY) /out:build/Main $(SRCS) $(DEPS) /compile:2 /noVerify /noIncludes && cp $(BCDLL) build/
 
+buildcs: build/Main.cs
+	csc /r:System.Numerics.dll /r:$(BCDLL) /target:exe /debug /nowarn:0164 /nowarn:0219 /nowarn:1717 /nowarn:0162 /nowarn:0168 build/Main.cs $(DEPS_CS) /out:build/Main.exe
+
 # TODO: HKDF.dfy hasn't been reviewed yet.
 # Once it is, re-add:
 #
@@ -68,9 +78,6 @@ lib/%.dll:
 test: $(DEPS)
 	lit test -q -v
 
-noverif: $(DEPS)
-	$(DAFNY) /out:build/Main $(SRCS) $(DEPS) /compile:2 /noVerify /noIncludes && cp $(BCDLL) build/
-
 clean-build:
 	$(RM) -r build/*
 

src/SDK/AlgorithmSuite.dfy

@@ -10,14 +10,22 @@ module AlgorithmSuite {
   import C = Cipher
   import Digests
 
-  const validIDs: set<uint16> := {0x0378, 0x0346, 0x0214, 0x0178, 0x0146, 0x0114, 0x0078, 0x0046, 0x0014};
+  const VALID_IDS: set<uint16> := {0x0378, 0x0346, 0x0214, 0x0178, 0x0146, 0x0114, 0x0078, 0x0046, 0x0014};
 
-  newtype ID = x | x in validIDs witness 0x0014
+  newtype ID = x | x in VALID_IDS witness 0x0014
   {
     function method KeyLength(): nat {
       Suite[this].params.keyLen as nat
     }
 
+    function method IVLength(): nat {
+      Suite[this].params.ivLen as nat
+    }
+
+    function method TagLength(): nat {
+      Suite[this].params.tagLen as nat
+    }
+
     function method SignatureType(): Option<S.ECDSAParams> {
       Suite[this].sign
     }
@@ -46,4 +54,26 @@ module AlgorithmSuite {
     AES_192_GCM_IV12_TAG16_KDFNONE_SIGNONE        := AlgSuite(C.AES_GCM_192, Digests.HmacNOSHA,  None),
     AES_128_GCM_IV12_TAG16_KDFNONE_SIGNONE        := AlgSuite(C.AES_GCM_128, Digests.HmacNOSHA,  None)
   ]
+
+  /* Suite is intended to have an entry for each possible value of ID. This is stated and checked in three ways.
+   *   - lemma SuiteIsCompletes states and proves the connection between type ID and Suite.Keys
+   *   - lemma ValidIDsAreSuiteKeys states and proves the connected between predicate ValidIDs and Suite.Keys
+   *   - the member functions of ID use the expression `Suite[this]`, whose well-formedness relies on every
+   *     ID being in Suite.Keys
+   */
+
+  lemma SuiteIsComplete(id: ID)
+    ensures id in Suite.Keys
+  {
+  }
+
+  lemma ValidIDsAreSuiteKeys()
+    ensures VALID_IDS == set id | id in Suite.Keys :: id as uint16
+  {
+    forall x | x in VALID_IDS
+      ensures exists id :: id in Suite.Keys && id as uint16 == x
+    {
+      assert x as ID in Suite.Keys;
+    }
+  }
 }

src/SDK/CMM/DefaultCMM.dfy

@@ -70,7 +70,7 @@ module DefaultCMMDef {
       {
         return Failure("Could not retrieve materials required for encryption");
       }
-      res := Success(em);
+      return Success(em);
     }
 
     method DecryptMaterials(alg_id: AlgorithmSuite.ID, edks: seq<Materials.EncryptedDataKey>, enc_ctx: Materials.EncryptionContext) returns (res: Result<Materials.DecryptionMaterials>)
@@ -104,7 +104,7 @@ module DefaultCMMDef {
         return Failure("Could not get materials required for decryption.");
       }
 
-      res := Success(dm);
+      return Success(dm);
     }
   }
 }