merging with main

Signed-off-by: Wojciech Ozga <woz@zurich.ibm.com>

Author: wojciechozga

.github/workflows/build.yml

@@ -18,7 +18,7 @@ jobs:
     - name: install OpenSBI dependencies
       run: sudo apt -qq -y install clang
     - name: install Qemu dependencies
-      run: sudo apt -qq -y install git libglib2.0-dev libfdt-dev libpixman-1-dev zlib1g-dev ninja-build python3-venv libslirp-dev
+      run: sudo apt -qq -y install git libglib2.0-dev libfdt-dev libpixman-1-dev zlib1g-dev ninja-build python3-venv libslirp-dev xz-utils
     - 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: install utilities

.github/workflows/verify.yml

@@ -47,7 +47,7 @@ jobs:
     - name: Exclude RefinedRust from dune build
       run: echo "(dirs :standard \ generated_code.bak refinedrust)" > verification/dune
     - 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
+      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 xz-utils
     - name: install OpenSBI dependencies
       run: sudo apt -qq -y install clang
     - name: install Buildroot dependencies

.gitignore

@@ -5,6 +5,7 @@ build/*
 target/*
 
 tools/cove_tap_tool/target
+qemu/
 security-monitor/target
 
 configurations/overlay/root/harness/baremetal

.gitmodules

@@ -1,9 +1,6 @@
 [submodule "hypervisor/buildroot"]
 	path = hypervisor/buildroot
 	url = https://github.com/buildroot/buildroot.git
-[submodule "qemu"]
-	path = qemu
-	url = https://github.com/qemu/qemu.git
 [submodule "security-monitor/opensbi"]
 	path = security-monitor/opensbi
 	url = https://github.com/riscv-software-src/opensbi.git

Makefile

@@ -24,7 +24,7 @@ export LINUX_IMAGE						?= $(HYPERVISOR_WORK_DIR)/buildroot/images/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_ABI				= lp64d
@@ -72,7 +72,13 @@ firmware: setup devtools hypervisor
 emulator: setup devtools
 	if [ ! -f "${QEMU_WORK_DIR}/bin/qemu-system-riscv64" ]; then \
 		mkdir -p $(QEMU_WORK_DIR); \
-		cd $(QEMU_SOURCE_DIR); ./configure --prefix=$(QEMU_WORK_DIR) --enable-slirp --enable-kvm --target-list=riscv64-softmmu,riscv64-linux-user; \
+		rm -rf $(QEMU_SOURCE_DIR); \
+		mkdir -p $(QEMU_SOURCE_DIR); \
+		cd $(QEMU_SOURCE_DIR); \
+		wget https://download.qemu.org/qemu-8.2.1.tar.xz; \
+		tar xJf qemu-8.2.1.tar.xz; \
+		mv qemu-8.2.1/* $(QEMU_SOURCE_DIR)/; \
+		./configure --prefix=$(QEMU_WORK_DIR) --enable-slirp --enable-kvm --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

README.md

@@ -1,22 +1,20 @@
-# Assured Confidential Execution (ACE) for RISC-V 
+# Assured Confidential Execution (ACE) for RISC-V
 ![Build Status](https://github.com/IBM/ACE-RISCV/actions/workflows/build.yml/badge.svg?branch=main)
 
-<img src=".github/ace.png" align="right" width="100" height="100"> 
- 
-ACE-RISCV is an open-source project, whose goal is to deliver a confidential computing framework with a formally proven security monitor. It is based on the [canonical architecture](https://dl.acm.org/doi/pdf/10.1145/3623652.3623668) and targets RISC-V with the goal of being portable to other architectures. The formal verification efforts focus on the [security monitor implementation](security-monitor/). We invite collaborators to work with us to push the boundaries of provable confidential computing technology. 
+<img src=".github/ace.png" align="right" width="100" height="100">
 
-This project implements the RISC-V CoVE spec's deployment model 3 referenced in [Appendix D](https://github.com/riscv-non-isa/riscv-ap-tee/blob/main/). 
+ACE-RISCV is an open-source project, whose goal is to deliver a confidential computing framework with a formally proven security monitor. It is based on the [canonical architecture](https://dl.acm.org/doi/pdf/10.1145/3623652.3623668) and targets RISC-V with the goal of being portable to other architectures. The formal verification efforts focus on the [security monitor implementation](security-monitor/). We invite collaborators to work with us to push the boundaries of provable confidential computing technology.
 
-**This is an active research project, without warranties of any kind.** Please read our [paper](https://dl.acm.org/doi/pdf/10.1145/3623652.3623668) to learn about the approach and goals.
+This project implements the RISC-V CoVE spec's deployment model 3 referenced in [Appendix D](https://github.com/riscv-non-isa/riscv-ap-tee/blob/main/). The formal specification is embedded in the security monitor's source code and the proofs are in [verification/ folder](verification/). Please read our [paper](https://dl.acm.org/doi/pdf/10.1145/3623652.3623668) to learn about the approach and goals.
 
 ## Hardware requirements
-We are currently building on RISC-V 64-bit with integer (I), atomic (A) and hypervisor extentions (H), physical memory protection (PMP), memory management unit (MMU), IOPMP, core-local interrupt controller (CLINT), and supervisor timecmp extension (Sstc). 
+We are currently building on RISC-V 64-bit with integer (I), atomic (A) and hypervisor extentions (H), physical memory protection (PMP), memory management unit (MMU), IOPMP, core-local interrupt controller (CLINT), and supervisor timecmp extension (Sstc).
 
 ## Quick Start
-Follow instructions to run one of the sample [confidential workloads](confidential-vms) under an [untrusted Linux KVM hypervisor](hypervisor/) in an [emulated RISC-V environment](qemu/).
+Follow instructions to run one of the sample [confidential workloads](confidential-vms) under an [untrusted Linux KVM hypervisor](hypervisor/) in an emulated RISC-V environment.
 
 ### Requirements
-Full compilation of the framework takes a long time because many tools are built from sources. Our toolchain currently includes: a RISC-V emulator (`qemu`), hypervisor kernel (`Linux kernel`), and firmware (`security monitor` with `OpenSBI firmware`). Make sure to build this project on a machine with at least 4 cores, 4GB RAM, and 50GB disk space for reasonable (~30min) build time.
+Full compilation of the framework takes a long time because many tools are built from sources. Our toolchain currently includes: hypervisor kernel (`Linux kernel`), confidential guest kernel (`Linux kernel`) and firmware (`security monitor` with `OpenSBI firmware`). Make sure to build this project on a machine with at least 4 cores, 4GB RAM, and 50GB disk space for reasonable (~30min) build time.
 
 ### Dependencies
 You must install build dependencies specific to the operating system you use AND install the Rust toolchain. You can also look at the [reproducible build configuration](.github/workflows/build.yml) of the continous integration (CI) system.
@@ -26,7 +24,7 @@ Dependencies for Ubuntu 22.04
 sudo apt update
 
 # riscv-gnu-toolchain dependencies:
-sudo apt -qq -y install 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
+sudo apt -qq -y install 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 xz-utils
 
 # OpenSBI
 sudo apt -qq -y install clang
@@ -81,7 +79,7 @@ MAKEFLAGS="--silent -j4" make
 ```
 
 #### Build individual components
-Alternativly, you can build individual components to avoid long builds that can lead to 'ssh disconnections', 'hangups', and similar issues. 
+Alternativly, you can build individual components to avoid long builds that can lead to 'ssh disconnections', 'hangups', and similar issues.
 
 Install all develoment tools required to compile code for the RISC-V architecture:
 ```
@@ -124,20 +122,16 @@ You should see the output from the boot process and a promt to login to the hype
 # login: root, password: passwd
 ```
 
-To run the sample Linux OS as a confidential VM execute:
+To run the sample Linux OS as a confidential VM (login: root, password: passwd) execute:
 ```
 ./run_linux_vm.sh
 ```
 
-To run the sample `baremetal` as a confidential VM execute:
-```
-./run_baremetal.sh
-```
-
-
 # License
 This repository is distributed under the terms of the Apache 2.0 License, see [LICENSE](LICENSE).
 
+**This is an active research project, without warranties of any kind.**
+
 # Citation
 ```
 @inproceedings{ozga2023riscvtee,

hypervisor/Makefile

@@ -60,7 +60,7 @@ dev:
 
 rootfs: overlay
 	echo "Generating hypervisor's root filesystem" ;\
-	$(MAKE) -s -C $(BUILDROOT_SOURCE_DIR) RISCV=$(RISCV_GNU_TOOLCHAIN_WORK_DIR) PATH=$(PATH) O=$(BUILDROOT_WORK_DIR) rootfs-ext2 
+	$(MAKE) -s -C $(BUILDROOT_SOURCE_DIR) RISCV=$(RISCV_GNU_TOOLCHAIN_WORK_DIR) PATH=$(PATH) O=$(BUILDROOT_WORK_DIR) rootfs-ext2
 
 clean:
 	rm -rf $(HYPERVISOR_WORK_DIR)

hypervisor/README.md

@@ -1,2 +1,2 @@
 # Hypervisor
-This code builds a Linux-based hypervisor (KVM+Qemu). The hypervisor is untrusted in our architecture.
+This code builds a Linux KVM hypervisor. The hypervisor is untrusted in our architecture.

hypervisor/configurations/qemu_riscv64_virt_defconfig

@@ -73,7 +73,6 @@ BR2_PACKAGE_QEMU_BLOBS=y
 # below not needed?
 BR2_TARGET_OPENSBI=y
 BR2_TARGET_OPENSBI_PLAT="generic"
-
 #BR2_PACKAGE_DEVMEM2=y
 
 ###