Skip to content

VeriGu/sosp-paper211-ae

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

22 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Verifying a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware

This artifact includes the mechanized Coq proofs for the security of SeKVM, our verified multiprocessor hypervisor, on Arm relaxed memory hardware. It also provides instructions on running the performance evaluations of SeKVM.

Table of Contents

1. Coq Proofs

The Coq proofs of this work have three components. First, we prove the theorems in Section 4 of the paper. These theorems guarantee that if a system satisfies a set of synchronization and memory access conditions that we call the wDRF conditions, then any observable behavior on the Arm relaxed memory hardware is also observable on the sequential consistent (SC) hardware model. Second, we prove that SeKVM satisfies the wDRF conditions. Third, we prove the security of SeKVM on the SC model. Together, these three components guarantee the security of SeKVM on Arm relaxed memory hardware. To check the proof in Coq, please see instruction in this link.

1.1 Proofs of main theorems in the paper

Here we include the mechanized proofs of Theorem 2 and Theorem 4 in Section 4. Note that Theorem 1 and Theorem 3 are both weakened versions of Theorem 4. There correctness automatically hold after Theorem 4 is proved.

1.1.1 Theorem 2 : when the kernel runs in isolation

file description
Base_Isolated Basic definitions
SC_Isolated The sequential consistent hardware model
Promising_Isolated The Promising-Arm relaxed memory model
DRF_Isolated DRF and no-barrier-misuse conditions
Proof_Isolated Proof of the theorem

1.1.2 Theorem 4 : when the kernel runs with user codes

In the proof of Theorem 4, we use data oracles to model user behavior. Details can be seen from the following files.

file description
Base_Full Basic definitions (with user behavior)
SC_Full The sequential consistent hardware model (with user behavior)
Promising_Full The Promising-Arm relaxed memory model (with user behavior)
DRF_Full DRF and no-barrier-misuse conditions (with user behavior)
PageTable_Full Page table behavior model and proof (with user behavior)
Proof_Full Proof of the theorem (with user behavior)

1.2 Proofs that SeKVM satisfies the wDRF conditions

condition proof
DRF-Kernel DRF_and_Barrier
No-Barrier-Misuse DRF_and_Barrier
Weak-Memory-Isolation MemoryIsolation
Transactional-Page-Table Transactional
Write-Once-Kernel-Mapping WriteOnceKernelMapping

1.3 Proofs of SeKVM on SC hardware

1.3.1 34 Security-preserving layers

# Layer Specification Code Verification Source Code Refinement
Hypercall/Exception
34 TrapHandler TrapHandlerSpec TrapHandlerProofCode TrapHandlerCode TrapHandlerRefine
33 TrapHandlerRaw TrapHandlerRawSpec TrapHandlerRawProofCode TrapHandlerRawCode TrapHandlerRawRefine
32 TrapDispatcher TrapDispatcherSpec TrapDispatcherProofCode TrapDispatcherCode TrapDispatcherRefine
31 FaultHandler FaultHandlerSpec FaultHandlerProofCode FaultHandlerCode FaultHandlerRefine
30 MemHandler MemHandlerSpec MemHandlerProofCode MemHandlerCode MemHandlerRefine
VCPU Context
29 CtxtSwitch CtxtSwitchSpec CtxtSwitchProofCode CtxtSwitchCode CtxtSwitchRefine
28 VCPUOps VCPUOpsSpec VCPUOpsProofCode VCPUOpsCode VCPUOpsRefine
27 VCPUOpsAux VCPUOpsAuxSpec VCPUOpsAuxProofCode VCPUOpsAuxCode VCPUOpsAuxRefine
SMMU
26 MmioOps MmioOpsSpec MmioOpsProofCode MmioOpsCode MmioOpsRefine
25 MmioOpsAux MmioOpsAuxSpec MmioOpsAuxProofCode MmioOpsAuxCode MmioOpsAuxRefine
24 MmioCore MmioCoreSpec MmioCoreProofCode MmioCoreCode MmioCoreRefine
23 MmioCoreAux MmioCoreAuxSpec MmioCoreAuxProofCode MmioCoreAuxCode MmioCoreAuxRefine
22 MmioRaw MmioRawSpec MmioRawProofCode MmioRawCode MmioRawRefine
VMBoot/Management
21 BootOps BootOpsSpec BootOpsProofCode BootOpsCode BootOpsRefine
20 BootAux BootAuxSpec BootAuxProofCode BootAuxCode BootAuxRefine
19 BootCore BootCoreSpec BootCoreProofCode BootCoreCode BootCoreRefine
18 VMPower VMPowerSpec VMPowerProofCode VMPowerCode VMPowerRefine
S2Page
17 MemoryOps MemoryOpsSpec MemoryOpsProofCode MemoryOpsCode MemoryOpsRefine
16 MemManager MemManagerSpec MemManagerProofCode MemManagerCode MemManagerRefine
15 PageManager PageManagerSpec PageManagerProofCode PageManagerCode PageManagerRefine
14 PageIndex PageIndexSpec PageIndexProofCode PageIndexCode PageIndexRefine
13 MemRegion MemRegionSpec MemRegionProofCode MemRegionCode MemRegionRefine
SMMU Page Table
12 MmioSPTOps MmioSPTOpsSpec MmioSPTOpsProofCode MmioSPTOpsCode MmioSPTOpsRefine
11 MmioSPTWalk MmioSPTWalkSpec MmioSPTWalkProofCode MmioSPTWalkCode MmioSPTWalkRefine
10 MmioPTWalk MmioPTWalkSpec MmioPTWalkProofCode MmioPTWalkCode MmioPTWalkRefine
9 MmioPTAlloc MmioPTAllocSpec MmioPTAllocProofCode MmioPTAllocCode MmioPTAllocRefine
Page Table
8 NPTOps NPTOpsSpec NPTOpsProofCode NPTOpsCode NPTOpsRefine
7 NPTWalk NPTWalkSpec NPTWalkProofCode NPTWalkCode NPTWalkRefine
6 PTWalk PTWalkSpec PTWalkProofCode PTWalkCode PTWalkRefine
5 PTAlloc PTAllocSpec PTAllocProofCode PTAllocCode PTAllocRefine
Spinlock
4 Locks LocksSpec LocksProofCode LocksCode LocksRefine
3 LockOpsH LockOpsHSpec LockOpsHProofCode LockOpsHCode LockOpsHRefine
2 LockOpsQ LockOpsQSpec LockOpsQProofCode LockOpsQCode LockOpsQRefine
1 LockOps LockOpsSpec LockOpsProofCode LockOpsCode LockOpsRefine
  • Note: The Source Code column lists the Clight source code that we verified. Our verification is based on the C semantics (i.e., Clight) of CompCert, a certified C compiler. The Clight source code written in Coq are extracted from the output of CompCert's clightgen tool. To obtain the clight code, we slightly retrofit the original C source code before parsing them by clightgen, since KVM uses some features that are not supported by CompCert. For example, all function definitions of SeKVM have compilation flag _hyp_text that controls compiler to store all the code into a specific section of the binary, which is not supported by CompCert. After generating Coq code using clightgen, we also deleted unnecessary definitions from the generated output to make them computable using Coq 8.4 and unified the identifier definitions globally, i.e. we made each function have the same identifier in all generated Coq files. In the future, we can add these features into CompCert’s parser and Clight and link the C code and the proofs automatically.

1.3.2 Bottom layer machine definition

These following definitions comprise the base layer of SeKVM's refinement proofs. Note that AbstractMachineState defines the machine state, and is used throughout the layer refinement proofs.

1.3.3 Top-layer Security

2. Performance Evaluation

We provide the instructions to run and test SeKVM as follows.

2.1 Prerequisites

  • We leverage Cloudlab.us which provides machines and preconfigured profiles. Machines will be available upon request for artifact evaluation. See Instructions for Cloudlab. For our profile, we include two physical Arm machines (server/client) connected by private network.

2.2 Instructions for Cloudlab

2.2.1 Joining Cloudlab

Please sign up in cloud.us: https://www.cloudlab.us/signup.php to be able to access machines. Join the existing project: VirtualCloudTech, and we will receive a notification automatically and we will let you in. To ensure anonymity, please use "SOSP21 AE #nonce" for full name, a one-time email address and random information in other fields.

2.2.2 Cloudlab profiles

Use the e6998-vct-m400 profile for running experiments. In Cluster, please select Cloudlab Utah. Please be patient and wait for the machines to setup and boot.

Once your machines are ready, you can login either via ssh or the UI interface. You have root access without password. You need to switch to root by:

# sudo su

2.3 Overview

On both the server and client machines, you need to do the basic preparation for running various scripts and compiling source code.

On both machines, Linux v4.18 is pre-installed, which includes KVM. You will need to first install QEMU to run the VM. If you want to install SeKVM, you first need to use a proper QEMU version, and then update the Linux on the server that includes the SeKVM. Once the installation is complete, you can start running a virtual machine.

On the client, you have the v4.18 kerenl installed. Once the server is running a virtual machine (or none for bare-metal measurements), run application benchmarks and collect results. The script to run the application benchmarks will output performance results.

2.4 Basic preparation

Clone this repository on both machines as a root user in the \root directory. Note that all the commands other than this git clone command need to be executed in the directory this repo is cloned.

# sudo su;

2.4.1 Clone the Artifact Repo

On the server, you will need to clone the repo to a dedicated SSD mounted to /mydata.

# cd /mydata
# git clone https://github.com/VeriGu/sosp-paper211-ae.git
# cd sosp-paper211-ae 

On the client, you can just clone it to the home directory.

# cd /root
# git clone https://github.com/VeriGu/sosp-paper211-ae.git
# cd sosp-paper211-ae 

2.4.2 Download the VM Image

We prepare different virtual disk images for different application workloads.

Benchmarks Image
Apache cloud-apache.img
Hackbench cloud-hack.img
Kernbench cloud-kern.img
MongoDB cloud-mongo.img
Redis cloud-redis.img

To download the images, on the server, run

cd scripts/tools/
./download-images.sh

Images will be downloaded under /mydata.

2.4.3 Create Multiple VMs Images

To run multiple VMs configuration, you will need to create an image for each VM for each benchmark:

# cd /mydata/sosp-paper211-ae/scripts/tools
# ./copy-image.sh

This may take around 10 minutes. You should see images been created under /mydata. For example, images for apache is named as cloud-hack-i.img.

The next sections explain how to compile and install QEMU and Linux kernel.

2.5 QEMU Setup

2.5.1 QEMU compilation for KVM

You will be able to run KVM on the server after the compilation is finished. See here for instructions to run VMs on KVM. Note that KVM can only run before SeKVM is installed.

# cd /srv/vm/qemu
# ./configure --target-list=aarch64-softmmu --disable-werror
# make -j8

To run SeKVM, you will first have to compile QEMU from the source code we modified to support SeKVM.

2.5.2 QEMU compilation for SeKVM

Download QEMU source from the repo below and setup environment.

# cd /mydata/sosp-paper211-ae/
# git submodule update --init qemu

Wait for a moment for the clone to complete, then do the following.

# cd qemu
# ./configure --target-list=aarch64-softmmu --disable-werror
# make -j8

2.6 SeKVM Setup

The setup involves compiling and installing Linux/KVM on the server machine that includes SeKVM and rebooting the machine.

First, sync from remote to fetch the kernel source

# cd /mydata/sosp-paper211-ae/
# git submodule update --init linux

Please wait for a few minutes for the clone to complete. You will then see the source code in the linux/ directory.

2.6.1 SeKVM Configuration & Compilation

# cd linux
# make sekvm_defconfig
# make -j8
# make modules_install
# make install

2.6.2 SeKVM Installation

First switch to the directory of "sosp-paper211-ae". The following will install the newly compiled SeKVM binary to your boot partition, so u-boot can load and boot SeKVM on the hardware.

# cd /mydata/sosp-paper211-ae/scripts/tools/
# ./install-kernel.sh
# reboot

Each time after reboot, run sudo su.

2.7 Running a virtual machine

To run virtual machines, please go to the directory sosp-paper211-ae/scripts.

# cd /mydata/sosp-paper211-ae/scripts/tests/

Run net.sh to create a virtual bridge to a network interface connecting the client machine. You only need to run it once whenever you (re)boot the host machine. You do not need to run it everytime you boot the VM.

# ../tools/net.sh

You can run the VM on SeKVM using the following command. root/root is the id/pwd needed for login. Note that you can only run the benchmark correpsonding to image used by the VM.

# ./run-guest-sekvm.sh -i /mydata/cloud-apache.img

You can replace run-guest-sekvm.sh with run-guest-kvm.sh to run the VM in KVM, if SeKVM has not been installed and booted. You can replace apache with hack, kern, mongo or redis to run their corresponding benchmark.

2.8 Terminating a virtual machine

After the experiment, you need to terminate a virtual machine. Run halt -p command iteratively inside virtual machines running on the server until you get the server shell.

[VM ~] # halt -p

2.9 Client Setup

The experiments measure various application performance on one machine, the server machine (i.e. bare-metal machine and virtual machines), while the other machine, which is the client machine, sends workloads to the server machine over the network.

Run this command on the client machine. It will automatically install all the applications for the performance evaluation on the server and the client machines.

Note: all scripts under scripts/client should only be run on the client machine.

When the client is ready, run the following to install the environment:

# cd /root/sosp-paper211-ae/scripts/client
# ./install.sh

2.10 Running Application Benchmarks and Collect Results

After all required packages are install on the client, you can then run the benchmark from the client machine using the respective script.

2.10.1 Apache/MongoDB/Redis

For instance, to run apache/MongoDB/Redis, do the following:

# cd /root/sosp-paper211-ae/scripts/client
# ./prep-apache.sh 10.10.1.100
# ./apache.sh 10.10.1.100

You can replace apache with mongo or redis to run mongodb or redis.

The results will be stored at scripts/client/apache.txt.

2.10.2 Hackbench/Kernbench

To run hackbench:

# cd /root/sosp-paper211-ae/scripts/client
# ./hack.sh 10.10.1.100

After hackbench is done, you can download the result from the server:

# ./grab-hack.sh 10.10.1.100

The result will be stored at scripts/client/hackbench.txt.

You can replace hack with kern to run kernbench.

2.11 Running Multi-VMs

We provide scripts for multiple VMs setup. Before you run benchmarks, make sure images for VMs and benchmark are craeted.

We provide scripts to run multiple VMs benchmarks on the client. Due to hardware constraints, here we use 8 VMs.

2.11.1 Launch VMs

You can launch VMs by:

# cd /mydata/sosp-paper211-ae/scripts/multi
# ./multi-sekvm.py apache

This script does not signal when it terminates. You should press Enter when there is no more output in the console. Same with multi-run.sh below.

Note that you can only run benchmarks correpsonding to image used by the VM. Due to IP address configuration, you cannot boot VMs for different benchmarks at the same time. To run different benchmarks, you should first shutdown current VMs.

There are 56 available VMIDs in SeKVM. When they are exhausted, you will see an error "ioctl(KVM_CREATE_VM) failed: 22 Invalid argument qemu-system-aarch64: failed to initialize KVM: Invalid argument qemu-system-aarch64: kvm_init_vcpu failed: Input/output error". Then you need to reboot the server and relaunch VMs.

Note: all scripts below under scripts/client should only be run on the client machine.

To test the connection to the VM, run:

# ./multi-connection.sh

If some connection fails, reboot the server and relaunch VMs.

2.11.2 Apache/MongoDB/Redis

You can run these benchmarks by:

# ./multi-prep.sh apache
# ./multi-run.sh apache

You can replace apache with mongo or redis to run mongodb or redis. mongo may trigger some intermediate errors which you can safely ignore.

The throughput numbers (ops/sec) of each VM/run will be appended at scripts/client/apache.txt.

2.11.3 Hackbench/Kernbench

To run hackbench:

# ./multi-run.sh hack

After hackbench is done, you can download the result from the server:

# ./multi-grab.sh hack

The runtime numbers (sec) of each VM/run will be appended at scripts/client/hackbench.txt.

You can replace hack with kern to run kernbench. These two benchmarks take longer to run. For hack, wait for at least one minute before you determine there is no more output and then press Enter. For kern, wait for 5 minutes.

2.11.4 Shutdown VMs

To shutdown VMs from the client, run:

# cd /root/sosp-paper211-ae/scripts/client
# ./multi-shutdown.sh

We use kvm-unit-test for microbenchmarks. kvm-unit-test creates a new VM for each measurement (please see arm-run in the source folder after untar). You can get the source of the benchmarks from here:

2.12 Running Microbenchmarks

We measure the workloads using Arm’s cycle counters. By default, KVM does not allow VMs to access the counters. Thus, we would have to patch KVM to enable VM access. You can the patch for KVM from here:

And the patch for SeKVM from here:

Before running the tests, you will have to recompile and reinstall KVM/SeKVM. For KVM, you should first cd sosp-paper211-ae/linux and do git checkout HEAD~1 to checkout to the mainline Linux 4.18. For SeKVM you do not have to git checkout.

You can compile the source by make -j8 && make modules_install && make install, and install the new binaries by cd /mydata/sosp-paper211-ae/scripts/tools/; ./install-kernel.sh.

You also need to install perf in your system for testing microbenchmarks. You can compile perf by:

cd /mydata/sosp-paper211-ae/linux/tools/perf; make; cp perf /usr/bin/

Then download the 3 QMP scripts that we created to pin vCPUs to physical CPUs: isolate_vcpus.sh, pin_vcpus.sh, qmp-cpus. You can download them by replacing $FILENAME in the following command:

Then, copy the above three scripts to QEMU for SeKVM: /mydata/sosp-paper211-ae/qemu/scripts/qmp/ QEMU for KVM: /srv/vm/qemu/scripts/qmp

Then you can untar kvm-unit-test first, and compile the source by: ./configure and make.

You can now run the tests by running the respective script for KVM and SeKVM in kvm-uni-test/:

KVM: ./perf-kvm.sh

SeKVM: ./perf-sekvm.sh

You need to open a different terminal, ssh to the cloudlab server running KVM/SeKVM, then cd into the corresponding qemu/scripts/qmp and run ./isolate_cpu.sh. The raw data will be written to the file result (Note that the old results will be removed). You can also use ./get-results.sh to pull the numbers from result.

About

Mirror of Artifact for SOSP 21 Paper: Verifying a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware

Resources

License

Stars

Watchers

Forks

Contributors 4

  •  
  •  
  •  
  •