Update verification setup (#24)

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

.github/workflows/verify.yml

@@ -20,6 +20,7 @@ jobs:
       uses: actions/checkout@v4
       with:
         persist-credentials: false
+        submodules: 'true'
     - name: Fix permissions
       run: chown -R 1000 .
     - name: ls
@@ -32,13 +33,25 @@ jobs:
       run: su coq -c 'curl --proto "=https" --tlsv1.2 -sSf https://sh.rustup.rs | bash /dev/stdin "-y"'
     - name: Setup Rust toolchain
       run: su coq -c 'source "$HOME/.cargo/env" && REFINEDRUST_ROOT=$PWD/verification/refinedrust ./verification/refinedrust/scripts/setup-rust.sh'
+    - name: Install the RiscV target for RefinedRust's toolchain
+      run: su coq -c 'source "$HOME/.cargo/env" && cd ./verification/refinedrust/rr_frontend && rustup target add riscv64gc-unknown-none-elf'
     - name: Install frontend
       run: su coq -c 'source "$HOME/.cargo/env" && REFINEDRUST_ROOT=$PWD/verification/refinedrust ./verification/refinedrust/scripts/install-frontend.sh'
     - name: Install Opam dependencies
       run: su coq -c 'eval $(opam env) && REFINEDRUST_ROOT=$PWD/verification/refinedrust ./verification/refinedrust/scripts/setup-coq.sh'
     - name: Install RefinedRust type system
       run: su coq -c 'eval $(opam env) && REFINEDRUST_ROOT=$PWD/verification/refinedrust ./verification/refinedrust/scripts/install-typesystem.sh'
+    - name: install build dependencies
+      run: sudo apt -qq -y install wget autoconf automake autotools-dev curl python3 libmpc-dev libmpfr-dev libgmp-dev gawk build-essential bison flex texinfo gperf libtool patchutils bc zlib1g-dev libexpat-dev
+    - name: install OpenSBI dependencies
+      run: sudo apt -qq -y install clang
+    - name: install Buildroot dependencies
+      run: sudo apt -qq -y install unzip sed binutils diffutils build-essential bash patch gzip bzip2 perl tar cpio unzip rsync file bc findutils
+    - name: make setup
+      run: su coq -c 'source "$HOME/.cargo/env" && eval $(opam env) && make setup'
+    - name: make devtools
+      run: su coq -c 'source "$HOME/.cargo/env" && eval $(opam env) && make devtools'
     - name: Translate specified files using RefinedRust
-      run: su coq -c 'source "$HOME/.cargo/env" && eval $(opam env) && REFINEDRUST="refinedrust_translate" make verify'
+      run: su coq -c 'source "$HOME/.cargo/env" && eval $(opam env) && make verify'
     - name: Check proofs
       run: su coq -c 'eval $(opam env) && cd verification && dune build'

Makefile

@@ -16,10 +16,10 @@ export OVERLAY_ROOT_DIR					?= $(ACE_DIR)/overlay/root
 export LINUX_IMAGE						?= $(ACE_DIR)/linux/arch/riscv/boot/Image
 export TOOLS_SOURCE_DIR					?= $(MAKEFILE_SOURCE_DIR)/tools
 export TOOLS_WORK_DIR					?= $(ACE_DIR)/tools
+export CROSS_COMPILE					?= riscv64-unknown-linux-gnu-
 
-export CROSS_COMPILE					= riscv64-unknown-linux-gnu-
-export PLATFORM_RISCV_XLEN				= 64 
-export PLATFORM_RISCV_ISA				= rv64gc 
+export PLATFORM_RISCV_XLEN				= 64
+export PLATFORM_RISCV_ISA				= rv64gc
 export PLATFORM_RISCV_ABI				= lp64d
 export PATH 							:= $(RISCV_GNU_TOOLCHAIN_WORK_DIR)/bin:$(PATH)
 
@@ -55,14 +55,14 @@ emulator: setup devtools
 		cd $(QEMU_SOURCE_DIR); ./configure --prefix=$(QEMU_WORK_DIR) --target-list=riscv64-softmmu,riscv64-linux-user; \
 		PATH="$(RISCV_GNU_TOOLCHAIN_WORK_DIR)/bin:$(PATH)" $(MAKE) -C $(QEMU_SOURCE_DIR) >/dev/null; \
 		PATH="$(RISCV_GNU_TOOLCHAIN_WORK_DIR)/bin:$(PATH)" $(MAKE) -C $(QEMU_SOURCE_DIR) install; \
-	fi 
+	fi
 
 tools: setup
 	mkdir -p $(TOOLS_WORK_DIR)
 	cp -rf $(TOOLS_SOURCE_DIR)/* $(TOOLS_WORK_DIR)
 
 verify:
-	ACE_DIR=$(ACE_DIR) $(MAKE) -C verification
+	PATH="$(RISCV_GNU_TOOLCHAIN_WORK_DIR)/bin:$(PATH)" ACE_DIR=$(ACE_DIR) LINUX_IMAGE=$(LINUX_IMAGE) CROSS_COMPILE=$(CROSS_COMPILE) PLATFORM_RISCV_XLEN=$(PLATFORM_RISCV_XLEN) PLATFORM_RISCV_ISA=$(PLATFORM_RISCV_ISA) PLATFORM_RISCV_ABI=$(PLATFORM_RISCV_ABI) $(MAKE) -C verification verify
 
 clean:
 	rm -rf $(ACE_DIR)

security-monitor/Makefile

@@ -31,6 +31,9 @@ build: hack fmt
 	cp $(SM_WORK_DIR)/$(CHAIN)/release/$(EXEC_NAME) $(SM_WORK_DIR)/ ; \
 	rm -rf $(OPENSBI_WORK_DIR)
 
+refinedrust: build
+	RUSTFLAGS='$(RUSTFLAGS)' CARGO_TARGET_DIR=$(SM_WORK_DIR) INSTALL_DIR=$(ACE_DIR) $(CARGO) refinedrust $(RELEASE) $(TARGET) --features verbose
+
 debug: hack
 	mkdir -p $(SM_WORK_DIR) ; \
 	RUSTFLAGS='$(RUSTFLAGS)' CARGO_TARGET_DIR=$(SM_WORK_DIR) INSTALL_DIR=$(ACE_DIR) $(CARGO) build $(TARGET) --features verbose ; \

security-monitor/src/lib.rs

@@ -16,6 +16,10 @@
 // used for convenience for calculating offsets between *usize pointers as bytes
 #![feature(pointer_byte_offsets)]
 #![feature(pointer_is_aligned)]
+// used for RefinedRust annotations
+#![feature(register_tool)]
+#![register_tool(rr)]
+#![feature(custom_inner_attributes)]
 
 // extern creates
 extern crate alloc;

verification/.gitignore

@@ -4,3 +4,4 @@ log
 rustc-ice-*
 refinedrust
 generated_code
+generated_code.bak

verification/Makefile

@@ -5,31 +5,27 @@
 MAKEFILE_PATH 							:= $(abspath $(lastword $(MAKEFILE_LIST)))
 MAKEFILE_SOURCE_DIR 					:= $(dir $(realpath $(lastword $(MAKEFILE_LIST))))
 
-REFINEDRUST ?= refinedrust_translate
+REFINEDRUST_CARGO ?= cargo-refinedrust
+REFINEDRUST_RUSTC ?= refinedrust-rustc
 
 # TODO: currently, this builds in-tree.
 # It would be good if we could build in the ACE_DIR
 # Main Problem: generating the RefinedRust files there.
 
 ## Verification-related make targets
-# a list of Rust source files to verify
-VERIFICATION_TARGETS =
-# ../security-monitor/src/core/memory_tracker/test.rs
 
-# generate the Coq code for a particular Rust file
-# TODO: configure output directory for Refinedrust
-%.rs.gen: %.rs
-	@$(REFINEDRUST) $<
-.PHONY: phony
+echo_toolchain:
+	@echo "Using RefinedRust toolchain located at $(REFINEDRUST_CARGO)"
 
-# generate Coq code for all verification targets
-generate_all: $(addsuffix .gen, $(VERIFICATION_TARGETS))
-.PHONY: generate_all
+backup_build_artifacts:
+	rm -rf generated_code.bak
+	@[ ! -d generated_code ] || (echo "Backing up generated files to generated_code.bak" && mv generated_code generated_code.bak)
+	rm -rf generated_code
 
-echo_toolchain:
-	@echo "Using RefinedRust toolchain located at $(REFINEDRUST)"
+generate: echo_toolchain backup_build_artifacts
+	RR_OUTPUT_DIR=$(MAKEFILE_SOURCE_DIR)/generated_code PATH="$(RISCV_GNU_TOOLCHAIN_WORK_DIR)/bin:$(PATH)" ACE_DIR=$(ACE_DIR) CROSS_COMPILE=$(CROSS_COMPILE) PLATFORM_RISCV_XLEN=$(PLATFORM_RISCV_XLEN) PLATFORM_RISCV_ISA=$(PLATFORM_RISCV_ISA) PLATFORM_RISCV_ABI=$(PLATFORM_RISCV_ABI) $(MAKE) -C ../security-monitor refinedrust
 
-verify: echo_toolchain generate_all
+verify: generate
 	@dune build --display short
 
 clean:

verification/dune

@@ -1,2 +1,2 @@
 ; Add project-wide flags here.
-(dirs :standard \ refinedrust)
+(dirs :standard \ refinedrust generated_code.bak)

verification/readme.md

@@ -0,0 +1,8 @@
+# Verification of the Security Monitor
+
+This directory contains work-in-progress on verifying the security monitor.
+Currently, the verification is in early stages.
+
+This document will be updated with details on the verified components and assurances as the verification effort progresses.
+
+For now, the [setup](setup.md) document describes how to setup the verification toolchain on your system.

verification/setup.md

@@ -46,15 +46,17 @@ If you do not have rustup installed yet, follow the instructions at https://rust
 Now, run the following commands in the shell opened previously:
 ```
 REFINEDRUST_ROOT=$PWD/refinedrust ./refinedrust/scripts/setup-rust.sh
+cd $PWD/refinedrust/rr_frontend && rustup target add riscv64gc-unknown-none-elf
 REFINEDRUST_ROOT=$PWD/refinedrust ./refinedrust/scripts/install-frontend.sh
 ```
 
-This will install a binary `refinedrust_translate` in the rustup toolchain for RefinedRust, which is available afterwards.
+This will install binaries `refinedrust-rustc` and `cargo-refinedrust` in your cargo path.
+This allows us to run `cargo refinedrust` in Rust projects.
 
 ## Verifying the code
 
 Now, we are ready to run the verification.
 To that end, run
 ```
-REFINEDRUST=refinedrust_translate make verify
+make verify
 ```

verification/theories/memory_tracker/page/page_extra.v

@@ -0,0 +1,33 @@
+From refinedrust Require Import typing.
+
+(* This reflects the page sizes in [core/mmu/page_size.rs] *)
+Inductive page_size : Set :=
+  | Size4KiB
+  | Size2MiB
+  | Size1GiB
+  | Size512GiB
+  | Size128TiB.
+
+Definition page_size_to_nat (sz : page_size) : nat :=
+  match sz with
+  | Size4KiB => 8 * 512
+  | Size2MiB => 8 * 512 * 512
+  | Size1GiB => 8 * 512 * 512 * 512
+  | Size512GiB => 8 * 512 * 512 * 512
+  | Size128TiB => 8 * 512 * 512 * 512 * 512 * 256
+  end.
+Definition page_size_to_Z (sz : page_size) : Z :=
+  page_size_to_nat sz.
+
+(* Pages should be aligned to the size of the page *)
+Definition page_size_align_log (sz : page_size) : nat :=
+  match sz with
+  | Size4KiB => 12
+  | Size2MiB => 21
+  | Size1GiB => 30
+  | Size512GiB => 39
+  | Size128TiB => 47
+  end.
+
+Definition mk_page_layout (sz : page_size) : layout :=
+  Layout (page_size_to_nat sz) (page_size_align_log sz).