Statically check parts of the RTS code with Frama-C

default.nix

@@ -111,6 +111,19 @@ rec {
     '';
   };
 
+  rts-frama-c = stdenv.mkDerivation {
+    name = "asc-rts-frama-c";
+    src = subpath ./rts;
+    buildInputs = [ nixpkgs.framac ];
+    buildPhase = ''
+      patchShebangs .
+      ./run-frama.sh
+    '';
+    installPhase = ''
+      touch $out
+    '';
+  };
+
   asc-bin = stdenv.mkDerivation {
     name = "asc-bin";
 
@@ -394,6 +407,7 @@ rec {
       unit-tests
       samples
       rts
+      rts-frama-c
       stdlib
       stdlib-doc
       stdlib-doc-live

rts/.gitignore

@@ -1,3 +1,6 @@
 as-rts.wasm
 test_rts
+
 _build
+
+.frama-c

rts/Makefile

@@ -91,7 +91,7 @@ RTS_WASM_O=$(RTSFILES:%=_build/wasm/%.o)
 RTS_NATIVE_O=$(RTSFILES:%=_build/native/%.o)
 
 #
-# The actual RTS, a we ship it with the compiler
+# The actual RTS, as shipped with the compiler
 #
 
 as-rts.wasm: $(RTS_WASM_O) $(TOMMATH_WASM_O)

rts/README.md

@@ -56,3 +56,49 @@ with the code provided by `rts.c` from `test_rts.c`. With
 
 this is executed. This is compiled natively, so may not hide bugs that are tied to
 WebAssembly.
+
+Static analysis with Frama-C
+----------------------------
+
+Some of the RTS code is pretty security-critical, as it deals with untrusted
+data (in particular, the IDL parser). So we are experimenting with throwing
+formal verification at it. The most promising tool in terms of power and
+usabilty seems to be Frama-C, which should be installed if you if you
+`nix-shell`; alternatively `opam install frama-c` works nicely.
+
+We currently check that the IDL parser does not access any memory outside the
+array given to it. The way to set this up in Frama-C is:
+
+ * Write a “main” function that embodies a typical incarnation of the idl code.
+   This is in `frama-main.c`.
+
+ * Invoke the EVA (value analysis) plugin of Frama-C with suitable flags. See
+   `run-frama.sh`.
+
+   In particular, since we use pointer comparisons in ways that are not fully
+   specified (or defiend, depending who you ask) we use
+   `-eva-warn-undefined-pointer-comparison`. to allow that.
+
+ * If there is a read from invalid memory, the script will error out
+   (due to `-eva-stop-at-nth-alarm 0`).
+
+   Else, a nice
+   ```
+   [inout] Inputs for function main:
+       test[0..99]
+   ```
+   tells us that everything is right.
+
+Frama-C doesn’t handle dynamic arrays very well, so we have to `split` the
+execution for various array lengths in `frama-main.c`, as advised in
+https://stackoverflow.com/a/57178643/946226.
+
+Frama-C can also do more sophisticated verification, including complex
+assertions, that we will need to explore.
+
+So far this is an experiment, if it gets in the way, we can ditch it. Or if we
+find a way to implement the RTS in Rust, we may also no longer need this.
+
+
+
+

rts/frama-main.c

@@ -0,0 +1,25 @@
+#include <stddef.h>
+#include <stdlib.h>
+#include <stdint.h>
+#include "__fc_builtin.h"
+
+// See README.md, Static analysis with Frama-C
+
+extern char *skip_idl_header(char *, char *);
+
+int main() {
+  int n = Frama_C_interval(0, 11);
+  if (n > 10) (n = 100);
+  //@ split n;
+  uint8_t *test = malloc(n);
+  if (test != NULL) {
+    //@ loop unroll n;
+    for (int i=0; i<n; i++) test[i]=Frama_C_interval(0, 255);
+
+    char* beg, *end;
+    beg = &test[0];
+    end = &test[0] + n;
+    skip_idl_header(beg, end);
+  }
+}
+

rts/idl.c

@@ -45,6 +45,7 @@ int32_t read_sleb128(char **ptr, char *end) {
 }
 
 export char *skip_idl_header(char *ptr, char *end) {
+  if (ptr + 3 >= end) (idl_trap());
   // Magic bytes
   if (*ptr++ != 'D') idl_trap();
   if (*ptr++ != 'I') idl_trap();

rts/run-frama.sh

@@ -0,0 +1,22 @@
+#!/usr/bin/env bash
+
+# See README.md, Static analysis with Frama-C
+
+set -e
+
+frama-c \
+  -eva \
+  -lib-entry \
+  -out-external \
+  -input frama-main.c,idl.c \
+  -no-warn-signed-overflow \
+  -eva-stop-at-nth-alarm 0 \
+  -eva-split-return 0 \
+  -eva-precision 6 \
+  -eva-split-limit 256 \
+  -eva-builtin malloc:Frama_C_malloc_fresh \
+  -eva-warn-undefined-pointer-comparison none
+
+# -no-warn-signed-overflow seems to otherwise give false warnings?
+# or else I do not understand why there is a signed overflow in a left-shift
+# with all arguments unsigned.