trusted boot: firmware.c specifications pass (#123)

GaloisInc · Oct 29, 2024 · d255dc0 · d255dc0
1 parent 0a113bf
commit d255dc0
Show file tree

Hide file tree

Showing 9 changed files with 308 additions and 43 deletions.
diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml
@@ -48,23 +48,21 @@ jobs:
             mkdir -p /tmp/wp-session/cache
             make -f frama_c.mk proofs
 
-  # secure-boot-verify-cn:
-  #   runs-on: ubuntu-22.04
-  #   steps:
-  #     - name: Checkout repository and submodules
-  #       uses: actions/checkout@v4
-  #     - name: Prove secure boot
-  #       uses: addnab/docker-run-action@v3
-  #       with:
-  #         image: ghcr.io/galoisinc/verse-opensut/cerberus:release
-  #         registry: ghcr.io
-  #         username: ${{ github.actor }}
-  #         password: ${{ secrets.VERSE_OPENSUT_ACCESS_TOKEN }}
-  #         options: -v ${{ github.workspace }}:/data
-  #         # This action seems to override the docker image entrypoint, as a result
-  #         # we need to run "eval `opam env`" first
-  #         # Use `>` so newlines will be replaced with spaces
-  #         run: >
-  #           eval `opam env` &&
-  #           cd components/platform_crypto/shave_trusted_boot &&
-  #           make cn_proof
+  secure-boot-verify-cn:
+    runs-on: ubuntu-22.04
+    steps:
+      - name: Checkout repository and submodules
+        uses: actions/checkout@v4
+      - name: Prove secure boot
+        uses: addnab/docker-run-action@v3
+        with:
+          image: ghcr.io/rems-project/cerberus/cn@sha256:7f999b2d3126458f364bfd177edeef3a161f0b4fd306e942e07d81311f24b325
+          registry: ghcr.io
+          options: -v ${{ github.workspace }}:/data
+          # This action seems to override the docker image entrypoint, as a result
+          # we need to run "eval `opam env`" first
+          # Use `>` so newlines will be replaced with spaces
+          run: >
+            eval `opam env` &&
+            cd components/platform_crypto/shave_trusted_boot &&
+            make cn_proof
diff --git a/components/include/wars.h b/components/include/wars.h
@@ -10,13 +10,22 @@
 // CN issue https://github.com/rems-project/cerberus/issues/284
 // GCC atributes not supported
 #define WAR_CN_284 1
+#ifdef WAR_CN_284
+#if WAR_CN_284
+#define __attribute__(...)
+#endif
+#endif
 
 // CN issue https://github.com/rems-project/cerberus/issues/285
 // Function pointers not supported
 #define WAR_CN_285 1
 
+// CN issue https://github.com/rems-project/cerberus/issues/309
+// String literals are created in the global context but the function doesn't have a resource for them
+#define WAR_CN_309
+
 // CN issue https://github.com/GaloisInc/VERSE-Toolchain/issues/103
 // memcmp not supported
 #define WAR_VERSE_TOOLCHAIN_103 1
 
-#endif // __CN_WARS_H__
+#endif // __CN_WARS_H__
diff --git a/components/platform_crypto/shave_trusted_boot/Makefile b/components/platform_crypto/shave_trusted_boot/Makefile
@@ -24,7 +24,7 @@ OBJ = $(SRC:$(ROOT_DIR)/%.c=$(BUILD_DIR)/%.o)
 CFLAGS = -I$(ROOT_DIR)
 
 CN_FLAGS=-I$(ROOT_DIR) --include=$(ROOT_DIR)/../../include/wars.h --magic-comment-char-dollar
-CN=cn $(CN_FLAGS)
+CN=cn verify $(CN_FLAGS)
 
 $(TRUSTED_BOOT_BIN): $(OBJ)
 	@mkdir -pv $(dir $@)
@@ -34,9 +34,17 @@ $(BUILD_DIR)/%.o: $(ROOT_DIR)/%.c
 	@mkdir -pv $(dir $@)
 	$(CC) $(CFLAGS) -c $< -o $@
 
+.PHONY: cn_proof clean
 clean:
 	rm -rf build/ build.*/
 	rm -f $(TRUSTED_BOOT_BIN)
 
-cn_proof: $(ROOT_DIR)/trusted_boot.c
+.PHONY: cn_proof_trusted_boot cn_proof_firmware cn_proof_firmware_with_attest
+cn_proof: cn_proof_trusted_boot cn_proof_firmware cn_proof_firmware_with_attest
+
+cn_proof_trusted_boot: $(ROOT_DIR)/trusted_boot.c
+	#$(CN) $<
+cn_proof_firmware: $(ROOT_DIR)/firmware.c
 	$(CN) $<
+cn_proof_firmware_with_attest: $(ROOT_DIR)/firmware.c
+	$(CN) -DWITH_ATTEST $<
diff --git a/components/platform_crypto/shave_trusted_boot/cn_array_utils.h b/components/platform_crypto/shave_trusted_boot/cn_array_utils.h
@@ -0,0 +1,120 @@
+#ifndef CN_ARRAY_UTILS_H_
+#define CN_ARRAY_UTILS_H_
+
+/*$
+predicate (map<u64,u8>) ArrayOrNull_u8 (pointer p, u64 l)
+{
+  if (!is_null(p)) {
+    take pv = each(u64 i; i >= 0u64 && i < l) {Owned<uint8_t>(array_shift<uint8_t>(p,i))};
+    return pv;
+  } else {
+    return default<map<u64,u8> >;
+  }
+}
+
+lemma SplitAt_Block_u8(pointer tmp, u64 len, u64 at, u64 slen)
+  requires
+    take a1 = each(u64 j; 0u64<=j && j<len){Block<uint8_t>(array_shift<uint8_t>(tmp, j))};
+    at >= 0u64;
+    len >= 0u64;
+    slen >= 0u64;
+    at < len;
+    slen <= len;
+    at + slen <= len;
+  ensures
+    take a2 = each(u64 j; 0u64<=j && j<at){Block<uint8_t>(array_shift<uint8_t>(tmp, j))};
+    take a3 = each(u64 j; ((u64)at)<=j && j<(at+slen)){Block<uint8_t>(array_shift<uint8_t>(tmp, j))};
+    take a4 = each(u64 j; ((u64)(at+slen))<=j && j<len){Block<uint8_t>(array_shift<uint8_t>(tmp, j))};
+
+lemma SplitAt_Owned_u8(pointer tmp, u64 len, u64 at, u64 slen)
+  requires
+    take a1 = each(u64 j; 0u64<=j && j<len){Owned<uint8_t>(array_shift<uint8_t>(tmp, j))};
+    at >= 0u64;
+    len >= 0u64;
+    slen >= 0u64;
+    at < len;
+    slen <= len;
+    at + slen <= len;
+  ensures
+    take a2 = each(u64 j; 0u64<=j && j<at){Owned<uint8_t>(array_shift<uint8_t>(tmp, j))};
+    take a3 = each(u64 j; ((u64)at)<=j && j<(at+slen)){Owned<uint8_t>(array_shift<uint8_t>(tmp, j))};
+    take a4 = each(u64 j; ((u64)(at+slen))<=j && j<len){Owned<uint8_t>(array_shift<uint8_t>(tmp, j))};
+
+lemma UnsplitAt_Block_u8(pointer tmp, u64 len, u64 at, u64 slen)
+  requires
+    take a2 = each(u64 j; 0u64<=j && j<at){Block<uint8_t>(array_shift<uint8_t>(tmp, j))};
+    take a3 = each(u64 j; ((u64)at)<=j && j<(at+slen)){Block<uint8_t>(array_shift<uint8_t>(tmp, j))};
+    take a4 = each(u64 j; ((u64)(at+slen))<=j && j<len){Block<uint8_t>(array_shift<uint8_t>(tmp, j))};
+    at >= 0u64;
+    len >= 0u64;
+    slen >= 0u64;
+    at < len;
+    slen <= len;
+    at + slen <= len;
+  ensures
+    take a1 = each(u64 j; 0u64<=j && j<len){Block<uint8_t>(array_shift<uint8_t>(tmp, j))};
+
+lemma UnSplitAt_Owned_u8(pointer tmp, u64 len, u64 at, u64 slen)
+  requires
+    take a2 = each(u64 j; 0u64<=j && j<at){Owned<uint8_t>(array_shift<uint8_t>(tmp, j))};
+    take a3 = each(u64 j; ((u64)at)<=j && j<(at+slen)){Owned<uint8_t>(array_shift<uint8_t>(tmp, j))};
+    take a4 = each(u64 j; ((u64)(at+slen))<=j && j<len){Owned<uint8_t>(array_shift<uint8_t>(tmp, j))};
+    at >= 0u64;
+    len >= 0u64;
+    slen >= 0u64;
+    at < len;
+    slen <= len;
+    at + slen <= len;
+  ensures
+    take a1 = each(u64 j; 0u64<=j && j<len){Owned<uint8_t>(array_shift<uint8_t>(tmp, j))};
+
+lemma ViewShift_Block_u8(pointer a, pointer b, u64 at, u64 len)
+  requires
+    take a1 = each(u64 j; at <= j && j <(at+len)) {Block<uint8_t>(array_shift<uint8_t>(a,j))};
+    ptr_eq(array_shift<uint8_t>(b,0u64), array_shift<uint8_t>(a,at));
+  ensures
+    take a2 = each(u64 j; 0u64 <= j && j <len) {Block<uint8_t>(array_shift<uint8_t>(b,j))};
+
+lemma ViewShift_Owned_u8(pointer a, pointer b, u64 at, u64 len)
+  requires
+    take a1 = each(u64 j; at <= j && j <(at+len)) {Owned<uint8_t>(array_shift<uint8_t>(a,j))};
+    ptr_eq(array_shift<uint8_t>(b,0u64), array_shift<uint8_t>(a,at));
+  ensures
+    take a2 = each(u64 j; 0u64 <= j && j <len) {Owned<uint8_t>(array_shift<uint8_t>(b,j))};
+
+lemma UnViewShift_Block_u8(pointer a, pointer b, u64 at, u64 len)
+  requires
+    take a2 = each(u64 j; 0u64 <= j && j <len) {Block<uint8_t>(array_shift<uint8_t>(b,j))};
+    ptr_eq(array_shift<uint8_t>(b,0u64), array_shift<uint8_t>(a,at));
+  ensures
+    take a1 = each(u64 j; at <= j && j <(at+len)) {Block<uint8_t>(array_shift<uint8_t>(a,j))};
+
+lemma UnViewShift_Owned_u8(pointer a, pointer b, u64 at, u64 len)
+  requires
+    take a2 = each(u64 j; 0u64 <= j && j <len) {Owned<uint8_t>(array_shift<uint8_t>(b,j))};
+    ptr_eq(array_shift<uint8_t>(b,0u64), array_shift<uint8_t>(a,at));
+  ensures
+    take a1 = each(u64 j; at <= j && j <(at+len)) {Owned<uint8_t>(array_shift<uint8_t>(a,j))};
+
+predicate (map<u64,u8>) CondArraySliceBlock_u8 (pointer p, boolean c, u64 s, u64 e)
+{
+  if (c) {
+    take pv = each(u64 i; i >= s && i < e) {Block<uint8_t>(array_shift<uint8_t>(p,i))};
+    return pv;
+  } else {
+    return default<map<u64,u8> >;
+  }
+}
+
+predicate (map<u64,u8>) CondArraySliceOwned_u8 (pointer p, boolean c, u64 s, u64 e)
+{
+  if (c) {
+    take pv = each(u64 i; i >= s && i < e) {Owned<uint8_t>(array_shift<uint8_t>(p,i))};
+    return pv;
+  } else {
+    return default<map<u64,u8> >;
+  }
+}
+$*/
+
+#endif // CN_ARRAY_UTILS_H_
diff --git a/components/platform_crypto/shave_trusted_boot/cn_memcpy.h b/components/platform_crypto/shave_trusted_boot/cn_memcpy.h
@@ -0,0 +1,33 @@
+#ifndef CN_MEMCPY_H_
+#define CN_MEMCPY_H_
+
+int _memcmp(const unsigned char *dest, const unsigned char *src, size_t n);
+/*$ spec _memcmp(pointer dest, pointer src, u64 n);
+
+requires
+    take Src = each (u64 i; 0u64 <= i && i < n ) { Owned(array_shift(src, i)) };
+    take Dest = each (u64 i; 0u64 <= i && i < n ) { Owned(array_shift(dest, i)) };
+
+ensures
+    take SrcR = each (u64 i; 0u64 <= i && i < n ) { Owned(array_shift(src, i)) };
+    take DestR = each (u64 i; 0u64 <= i && i < n ) { Owned(array_shift(dest, i)) };
+    Src == SrcR; Dest == DestR;
+    (return != 0i32 || Src == Dest) && (return == 0i32 || Src != Dest);
+$*/
+
+void _memcpy(unsigned char *dest,
+                 const unsigned char *src, size_t n);
+/*$
+spec _memcpy(pointer dest, pointer src, u64 n);
+requires
+    take Src = each (u64 i; 0u64 <= i && i < n ) { Owned(array_shift(src, i)) };
+    take Dest = each (u64 i; 0u64 <= i && i < n ) { Block<unsigned char>(array_shift(dest, i)) };
+
+ensures
+    take SrcR = each (u64 i; 0u64 <= i && i < n ) { Owned(array_shift(src, i)) };
+    take DestR = each (u64 i; 0u64 <= i && i < n ) { Owned(array_shift(dest, i)) };
+    Src == SrcR;
+    each (u64 i; 0u64 <= i && i < n ) { SrcR[i] == DestR[i] };
+$*/
+
+#endif // CN_MEMCPY_H_