Infrastructure for running MPS under pKVM

.cargo/config.toml

@@ -0,0 +1,3 @@
+[target.aarch64-unknown-linux-gnu]
+linker = "aarch64-linux-gnu-gcc"
+

.github/workflows/main.yml

@@ -12,24 +12,8 @@ on:
 
 # A workflow run is made up of one or more jobs that can run sequentially or in parallel
 jobs:
-    mps-build:
-        runs-on: ubuntu-latest
-        steps:
-          - name: Checkout repository and submodules
-            uses: actions/checkout@v4
-          - name: Build MPS
-            uses: addnab/docker-run-action@v3
-            with:
-              image: galoisinc/hardens:latest
-              options: -v ${{ github.workspace }}:/HARDENS
-              run: |
-                cd components/mission_protection_system/src
-                SENSORS=NotSimulated SELF_TEST=Enabled make rts
-                make clean
-                SENSORS=NotSimulated SELF_TEST=Enabled make rts_bottom
-
-    mps-test:
-      runs-on: ubuntu-latest
+  mps-build:
+      runs-on: ubuntu-22.04
       steps:
         - name: Checkout repository and submodules
           uses: actions/checkout@v4
@@ -40,12 +24,54 @@ jobs:
             options: -v ${{ github.workspace }}:/HARDENS
             run: |
               cd components/mission_protection_system/src
+              SENSORS=NotSimulated SELF_TEST=Enabled make rts_bottom
               make clean
               SENSORS=NotSimulated SELF_TEST=Disabled make rts
               mv rts rts.no_self_test
               make clean
               SENSORS=NotSimulated SELF_TEST=Enabled make rts
               mv rts rts.self_test
-              cd ../tests
-              pip3 install -r requirements.txt
-              RTS_DEBUG=1 QUICK=1 python3 ./run_all.py
+        - name: Upload MPS binaries
+          uses: actions/upload-artifact@v4
+          with:
+            name: mps-binaries
+            path: components/mission_protection_system/src/rts.*
+
+  mps-test:
+    runs-on: ubuntu-22.04
+    needs: mps-build
+    steps:
+      - name: Checkout repository and submodules
+        uses: actions/checkout@v4
+      - name: Download MPS binaries
+        uses: actions/download-artifact@v4
+        with:
+          name: mps-binaries
+      - name: Display structure of downloaded files
+        run: |
+          chmod +x rts.*
+          mv rts.* components/mission_protection_system/src/.
+      - name: Test MPS
+        uses: addnab/docker-run-action@v3
+        with:
+          image: galoisinc/hardens:latest
+          options: -v ${{ github.workspace }}:/HARDENS
+          run: |
+            cd components/mission_protection_system/tests
+            pip3 install -r requirements.txt
+            RTS_DEBUG=1 QUICK=1 python3 ./run_all.py
+
+  vmrunner:
+    runs-on: ubuntu-22.04
+    steps:
+    - name: Install aarch64 toolchain
+      run: sudo apt-get install -y gcc-aarch64-linux-gnu
+    - uses: hecrj/setup-rust-action@v2
+      with:
+        rust-version: 1.74
+        targets: aarch64-unknown-linux-gnu
+    - uses: actions/checkout@master
+    - name: Build VM runner
+      run: |
+        cd src/vm_runner
+        cargo build --release --target aarch64-unknown-linux-gnu

.github/workflows/proofs.yml

@@ -14,7 +14,7 @@ on:
 jobs:
 
   mps-verify-cn:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-22.04
     steps:
       - name: Checkout repository and submodules
         uses: actions/checkout@v4
@@ -32,7 +32,7 @@ jobs:
             make -f cn.mk proofs
 
   mps-verify-frama-c:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-22.04
     steps:
       - name: Checkout repository and submodules
         uses: actions/checkout@v4

components/mission_protection_system/build_aarch64.sh

@@ -0,0 +1,10 @@
+#!/bin/bash
+set -euo pipefail
+
+cd "$(dirname "$0")/src"
+make clean
+make CC=aarch64-linux-gnu-g++ CXX=aarch64-linux-gnu-g++ SENSORS=NotSimulated SELF_TEST=Disabled
+cp -v rts rts.no_self_test.aarch64
+make clean
+make CC=aarch64-linux-gnu-g++ CXX=aarch64-linux-gnu-g++ SENSORS=NotSimulated SELF_TEST=Enabled
+cp -v rts rts.self_test.aarch64

components/mission_protection_system/src/posix_main.c

@@ -83,6 +83,10 @@ void update_display() {
   }
 }
 
+// A copy of the `argv` that was passed to main.  This is used to implement the
+// reset (`R`) command inside `read_rts_command`.
+static char** main_argv = NULL;
+
 int read_rts_command(struct rts_command *cmd) {
   int ok = 0;
   uint8_t device, on, div, ch, mode, sensor;
@@ -166,8 +170,13 @@ int read_rts_command(struct rts_command *cmd) {
           sensor,ch,val));
 #endif
   } else if (line[0] == 'Q') {
-    // printf("<main.c> read_rts_command QUIT\n");
+    printf("<main.c> read_rts_command QUIT\n");
     exit(0);
+  } else if (line[0] == 'R') {
+    printf("<main.c> read_rts_command RESET\n");
+    // Re-exec the RTS binary with the same arguments and environment.  This
+    // has the effect of resetting the entire RTS to its initial state.
+    execv("/proc/self/exe", main_argv);
   } else if (line[0] == 'D') {
     DEBUG_PRINTF(("<main.c> read_rts_command UPDATE DISPLAY\n"));
     update_display();
@@ -363,6 +372,7 @@ uint32_t time_in_s()
 }
 
 int main(int argc, char **argv) {
+  main_argv = argv;
   struct rts_command *cmd = (struct rts_command *)malloc(sizeof(*cmd));
 
   core_init(&core);

components/mission_protection_system/src/self_test_data/test.csv

@@ -1,10 +1,190 @@
-0x1	[[0xb56b, 0x9b67], [0x116d, 0x305e], [0x1e6a, 0x6d2b], [0x4278, 0x3cac]]	[[0xbea4, 0x8cff, 0x8276], [0x73c1, 0x3306, 0x4b66], [0x1306, 0x8017, 0x061b], [0x0681, 0xe654, 0x563f]]	0x1	0x2
-0x1	[[0xb4bf, 0xf2a5], [0xb729, 0x0592], [0xc445, 0x3267], [0xdb63, 0x98d5]]	[[0x0af4, 0xb1ce, 0xa1c2], [0x3042, 0x23f3, 0x50b6], [0x578e, 0xc16a, 0xad24], [0xebd5, 0xc4b4, 0x6ea9]]	0x2	0x3
-0x1	[[0x9e64, 0x646e], [0xec38, 0xa171], [0x8b17, 0x26fa], [0x6e11, 0x13e9]]	[[0x4301, 0xeed8, 0x407c], [0xbdd9, 0x5e64, 0x978f], [0x337e, 0xb6b8, 0xc261], [0xf272, 0xbec3, 0xe020]]	0x3	0x3
-0x1	[[0xc707, 0x909b], [0x5950, 0x5023], [0x2174, 0x7fbc], [0x9c8e, 0xb1c5]]	[[0x450a, 0x5387, 0x4251], [0x54f7, 0x7331, 0x610c], [0x2246, 0xc23c, 0xe353], [0xd742, 0x11f0, 0x5c9b]]	0x2	0x2
-0x1	[[0x64a7, 0xfc58], [0x73c5, 0x0dca], [0x76be, 0x322f], [0xf275, 0x856e]]	[[0x71fb, 0xe1fc, 0xc226], [0xdca3, 0x47de, 0x2a2c], [0x365b, 0xe8d8, 0x5e63], [0x7d75, 0xf509, 0x0d46]]	0x0	0x0
-0x1	[[0x3379, 0x097d], [0x8d0a, 0xf187], [0xb18d, 0x6bde], [0x31b3, 0x1656]]	[[0x2a5f, 0xa347, 0xfd69], [0x99a0, 0xb82f, 0x9554], [0x2106, 0x7623, 0x08dd], [0xabf1, 0xc54c, 0x1237]]	0x0	0x2
-0x1	[[0xe71e, 0x506e], [0x84a3, 0xf7d7], [0x3c66, 0xfdb7], [0x354c, 0xa3bb]]	[[0x79e7, 0xec8c, 0x73c2], [0x9d4c, 0x395b, 0x4a52], [0x783c, 0xf1cc, 0xd0ee], [0x8171, 0xc116, 0x08bd]]	0x0	0x0
-0x1	[[0x33fe, 0x41d3], [0x1842, 0xce9e], [0xa731, 0x6312], [0xbabb, 0xaa2e]]	[[0xd683, 0x8077, 0x2d0d], [0x0c50, 0xa354, 0xb23e], [0xc806, 0xa680, 0x25d1], [0x965f, 0xba1f, 0x7f91]]	0x1	0x3
-0x3	[[0x8f55, 0xa308], [0x8910, 0xc8f3], [0xed53, 0xa96e], [0x6b72, 0xb094]]	[[0x8024, 0x2af2, 0x8a77], [0xd392, 0x6b95, 0xc5e4], [0xd167, 0x78eb, 0xae62], [0xd786, 0x2183, 0xeda3]]	0x3	0x3
-0x1	[[0x03a4, 0x7579], [0xfef5, 0x193e], [0x8381, 0xbdd3], [0x649d, 0xae79]]	[[0xc42c, 0xd33a, 0x2cc9], [0xa687, 0x657b, 0xbf3b], [0x48d2, 0xc9b1, 0x2b48], [0xb123, 0x8814, 0x497c]]	0x2	0x3
+0x1	[[0x753c,
+0x8567],
+[0x9941,
+0x9047],
+[0x010f,
+0x619e],
+[0x6c16,
+0xa5e2]]	[[0xbe86,
+0x2ac0,
+0x508e],
+[0xf929,
+0x7f97,
+0x2e07],
+[0x92f3,
+0xdec1,
+0xe896],
+[0xca3a,
+0x4532,
+0x67ac]]	0x1	0x3
+0x1	[[0xe2bc,
+0x48ad],
+[0x20ab,
+0x6b44],
+[0x5074,
+0x8063],
+[0x74b5,
+0xfadb]]	[[0xe5ce,
+0x151f,
+0x69fc],
+[0x933a,
+0xe0e5,
+0x372d],
+[0x52d0,
+0x5320,
+0x6273],
+[0x6d2a,
+0xc90a,
+0x6c50]]	0x3	0x1
+0x3	[[0xaf29,
+0xfb7f],
+[0xd293,
+0xcaa6],
+[0x101d,
+0xb852],
+[0x10da,
+0xfa5c]]	[[0x1f9b,
+0xf7d2,
+0x64c2],
+[0xfa38,
+0x35e3,
+0xd88e],
+[0x0660,
+0xe4b8,
+0xb256],
+[0x5071,
+0x5b45,
+0xa947]]	0x3	0x1
+0x3	[[0xfd39,
+0x21d4],
+[0xdb77,
+0xff43],
+[0x899b,
+0xd07b],
+[0x576c,
+0xe806]]	[[0xf591,
+0x3092,
+0xdeab],
+[0x53b7,
+0xcdd8,
+0x3125],
+[0x71c2,
+0x375c,
+0x4d54],
+[0xf62f,
+0xe4f1,
+0x7d1a]]	0x0	0x3
+0x1	[[0x2111,
+0x72a4],
+[0x5ef8,
+0xc6af],
+[0x702d,
+0x1f3f],
+[0x7030,
+0x1828]]	[[0x70bd,
+0xa499,
+0xb6a4],
+[0x3749,
+0x0bc8,
+0x0170],
+[0x90ef,
+0x1291,
+0xf908],
+[0x66b2,
+0xc0a7,
+0x4c86]]	0x0	0x2
+0x1	[[0x205c,
+0x813b],
+[0xdfcc,
+0xb70d],
+[0x877f,
+0x930a],
+[0x4300,
+0x3a90]]	[[0x1966,
+0xf30a,
+0x1237],
+[0xcbb6,
+0xdf45,
+0xb3a7],
+[0xb5d1,
+0x9b11,
+0x1e04],
+[0x4ca2,
+0xa2c5,
+0xe2b2]]	0x2	0x1
+0x1	[[0x64f6,
+0x2140],
+[0x839a,
+0x55a7],
+[0x6255,
+0x27ed],
+[0x9baa,
+0xb966]]	[[0xc51d,
+0x1552,
+0xc126],
+[0x86c1,
+0x66ae,
+0x8294],
+[0xb374,
+0x4385,
+0x5ffb],
+[0x3ff4,
+0x9a3c,
+0xb897]]	0x2	0x0
+0x1	[[0x77b9,
+0x9969],
+[0x648b,
+0x1459],
+[0x1c41,
+0x5f5e],
+[0x30a9,
+0x9941]]	[[0xa6c2,
+0xc89c,
+0x854d],
+[0xbff7,
+0xd30a,
+0xae30],
+[0x733a,
+0xacbc,
+0x5680],
+[0xde27,
+0x0ba9,
+0xcc1c]]	0x1	0x2
+0x3	[[0x95a8,
+0xecfd],
+[0x617d,
+0xeb9b],
+[0x74c8,
+0xfb58],
+[0x73e2,
+0x378c]]	[[0x1674,
+0x53e5,
+0xabbd],
+[0x6ee4,
+0xe0c2,
+0xdd77],
+[0x26ab,
+0x9e64,
+0x6e96],
+[0x0c21,
+0x13a3,
+0x9d27]]	0x3	0x1
+0x3	[[0xd477,
+0x4235],
+[0xa5b1,
+0xf5e3],
+[0x30ec,
+0xf265],
+[0x014e,
+0x8fd2]]	[[0x31b9,
+0x7d86,
+0x15e4],
+[0xea39,
+0xf888,
+0x9fbe],
+[0x8247,
+0x7fbd,
+0x5b29],
+[0xdb42,
+0x301d,
+0x7ed8]]	0x2	0x0

components/mission_protection_system/src/self_test_data/test_to_c.py

@@ -27,8 +27,16 @@ def render(test):
         return f"{test}"
 
 with open(sys.argv[1]) as csv_file:
-    reader = csv.reader(csv_file,delimiter='\t')
-    foos = [render(tc) for testcase in reader for tc in expand(testcase)]
+    line_buf = ''
+    foos = []
+    for line in csv_file:
+        line = line.rstrip()
+        line_buf += line
+        if not line_buf.endswith(','):
+            testcase = line_buf.split('\t')
+            foos.extend(render(tc) for tc in expand(testcase))
+            line_buf = ''
+
     tests = ",\n".join(foos)
     print(f"// Tests generated from {sys.argv[1]}")
     print(tests)