KRover is a Symbolic Execution Engine for Dynamic Kernel Analysis. A kernel analyst can develop a kernel analysis program on top of KRover and invoke the latter as a library. The program benefits from the following KRover features.

1. KRover takes a live kernel thread as input and functions without(necessarily) relying on the kernel source code. KRover neither instruments the kernel binary nor applies Dynamic Binary Translation (DBT).
2. The analysis program (including KRover) uses the same address space as the target kernel’s, with its binary instructions running on the CPU and referencing kernel memory using kernel virtual addresses e.g., mov %rax 0xffffffff12345678.
3. The analysis program, like conventional dynamic analysis tools, has access to hardware features to control the target thread, such as using debug registers or INT3 probes.
4. The analysis program is empowered by KRover to direct how the target thread runs: to “slide down" from one program point to another with native execution or to single-step with symbolic execution for close monitoring and analysis. The analysis program orchestrates the interleaving of these two modes.

These features make KRover amicable for those kernel analysis tasks which demand a binary level understanding of an execution flow. For more information, refer to "KRover: A Symbolic Execution Engine for Dynamic Kernel Analysis (ACM CCS23)", "KRoverFullPaper.pdf". This document will guide you through the setup of the necessary infrastructure and dependent systems needed for the execution of KRover.

Happy KRoving !!!

This includes the following software packages.

1. KRover: Symbolic execution engine.

KRover is executed on OASIS infrastructure. OASIS consists of the following components.

2. kernel: A Linux kernel with modified KVM.
3. k-loader: A LKM that acts as a kernel loader.
4. u-loader: Modified libc to satisfy specific loading/address space requirements.
5. oasis-lib: A collection of binaries enabling specific OASIS features such as EFI: execution flow instrumentation.
6. launcher: System launcher, launches oasis and KRover.

KRover executes on OASIS infrastructure. Thus, the first step is to set up the OASIS infrastructure. If you need more information about OASIS design and features, refer to our OASIS paper: "A novel dynamic analysis infrastructure to instrument untrusted execution flow across user-kernel spaces (IEEE SP21)".

OASIS needs to run on a bare-metal machine with the customized kernel specified above. The target kernel which will be analyzed using KRover would be executed in a VM. We recommend a host machine with Ubuntu. If your current Ubuntu does not match the following requirements or you do not want to disturb your current working environment, you can consider creating a new partition and installing a separate Ubuntu OS. Then your machine becomes a dual-boot Ubuntu system, do the following things in the new Ubuntu.

1. Host OS: Ubuntu 18.04; Kernel version: Linux 5.4.X.
2. binutils: 2.30
3. gcc:7.5.0
4. Install KVM and its related virt-manager toolchain

3.1. Install a VM with Linux 5.4.X using virt-manager

3.2. Configure the guest VM: disable ASLR permanently reference Add a file /etc/sysctl.d/01-disable-aslr.conf containing:

kernel.randomize_va_space = 0

3.3. Configure the guest VM: disable pti through the boot option add 'nopti' after 'quite splash' in /etc/default/grub, then

sudo update-grub2

git clone https://github.com/KRoverSystems/KRover.git

sudo apt-get install build-essential libncurses-dev bison flex libssl-dev libelf-dev

Go to oasis/kernel/linux-hwe-5.3.18/virt/kvm/imee.h Update the constant, KROVER_OASIS_LIB_PATH accordingly. In this repo, the oasis-lib is available in oasis/oasis-lib/KRover-OASIS-Lib( See step 8 for more info.)

confirm CONFIG_X86_SMAP is not set in the .config file. if CONFIG_X86_SMAP = y, change it to CONFIG_X86_SMAP = n.

cd oasis/kernel/Linux-hwe-5.3.18
grep CONFIG_X86_SMAP .config

load and save the .config file, then exit.

make menuconfig 

make -j`nproc` deb-pkg
cd ../ && ls -la

There would be four *.deb packages generated.

sudo dpkg -i Linux-image-5.3.18_5.3.18-1_amd64.deb 
sudo dpkg -i Linux-image-5.3.18-dbg_5.3.18-1_amd64.deb
sudo dpkg -i Linux-libc-dev_5.3.18-1_amd64.deb   
sudo dpkg -i Linux-headers-5.3.18_5.3.18-1_amd64.deb 

During the boot procedure, remember to select Advanced options for ..., then select 5.3.18 kernel, which is the modified oasis kernel we just installed. you may choose to update /etc/default/grub or /boot/grub/grub.cfg to make the newly installed 5.3.18 kernel the default kernel whenever rebooting, to avoid the above troublesome selectings.

reference Add a file /etc/sysctl.d/01-disable-aslr.conf containing:

kernel.randomize_va_space = 0

add 'nopti' after 'quite splash' in /etc/default/grub, then

sudo update-grub2

Go to oasis/k-loader/configure.sh and update the path to kernel's imee.h accordingly. Execute configure.sh to create a symbolic link to imee.h .

make && sudo insmod ld.ko

cd oasis/u-loader/
mkdir build-glibc
mkdir install
cd build-glibc
../KRover-u-loader/configure --prefix=/<PATH-TO>/oasis/u-loader/install
make -j`nproc` CFLAGS="-O2 -U_FORTIFY_SOURCE -fno-stack-protector"
make install

oasis-lib includes a collection of prebuilt binaries in the form of .so files. These are a collection of gates that facilitate EFI-execution flow switches(Eg: switch between a target kernel thread and KRover). Use the .so files as-is. Re-compiling may change the offsets between certain functions( or the start offset of a certain function) within a given .so file causing oasis to malfunction.

add x permission for the data_page file in springboard.

sudo chmod +x /<PATH-TO>/oasis/oasis-lib/KRover-OASIS-Lib/springboard/data_page

Go to oasis/launcher/oasis-launcher.c and update the constant, KROVER_PATH accordingly. Once KRover is built later, an executable KRover binary named "testtest" will be available in KRover/loader/ directory. Go to oasis/launcher/ and run compile.sh to generate the launcher binary named, oasis-launcher.

KRover uses Dyninst for binary instruction disassembly and Z3 for constraint evaluation.

sudo apt install libiberty-dev

Install cmake version > 3.13

sudo apt install texlive-full

 git clone https://github.com/dyninst/dyninst.git
 cd dyninst
 git checkout -b V12 v12.0.0
 cd ..
 mkdir dyninst_build && cd dyninst_build
 cmake ../dyninst -DCMAKE_INSTALL_PREFIX=`pwd`/../install -DSTERILE_BUILD=OFF
 make -j`nproc`
 make install

Download and install Microsoft Z3 version 4.8.14 Follow the instructions provided by the Z3 team. (https://github.com/Z3Prover/z3/tree/z3-4.8.14)

Update all incomplete paths in the two Makefiles in KRover (DYNINST_PATH, Z3_PATH, etc.)

Update run-Krover.sh with the path to oasis-launcher

cd KRover
./build-KRover.sh

KRover executable binary named, testtest will be generated in KRover/loader/ directory.

This is a POC of how you can use KRover to symbolically execute a Linux syscall handler.

We have included a POC target user space program, poc.c in the "poc" directory. Copy this into the target guest VM and build the poc.c

gcc -fno-stack-protector poc.c -o target

Execute the following command in the target VM to obtain the list of syscall handler addresses from the target kernel.

sudo cat /proc/kallsyms >> ksyms.txt

Then, copy the contents of ksyms.txt into KRover/stc-files/kern_syms.txt .

The following details are specific to the execution of the selected POC where we are trying to symbolically execute the getpriority syscall of the target kernel.

The user can leverage KRover as a library to write their own simple user analyzer. A POC analyzer to support the symbolic execution of getpriority is included in Analyze.cpp.

The sample user analyzer included in Analyze.cpp, supports the symbolic execution of a selected system call. The user can select the syscall handler name in "CAnalyze::setupScallAnalysis()". To support the POC, we have set the syscall handler name for getpriority by selecting the corresponding kernel symbol name "__x64_sys_getpriority" in "Analyze::setupScallAnalysis()". The corresponding VA of the syscall handler is available in KRover/stc-files/kern_syms.txt .

The POC user analyzer installs an int3 breakpoint at the start of the getpriority syscall handler in "CAnalyze::beginAnalysis()". The API, "InstallINT3Probe()" is used for this purpose.

The POC user analyzer uses the "defineSymbolsForScalls()" API to symbolize some syscall arguments passed to the syscall handler of getpriority. KRover supports both register and memory symbols.

The analysis sequence enabled by the POC user analyzer is as follows.

1. main.cpp : Once the target thread is captured, control is passed to the user analyzer in Analyze.cpp to find the address of the getpriority syscall and install an int3 breakpoint at its start.
2. main.cpp > to_native(): Captured target VM thread is dispatched for naive execution. i.e. the target thread is executed in the onsite environment directly on the hardware(out of KRover).
3. Once the target's native execution reaches the installed int3 breakpoint( at the syscall handler of getpriority), the int3 exception handler(main.cpp > int3_store_context() > int3_handler() ) receives control.
4. The int3 exception handler, int3_handler() passes control back to the user analyzer. "execState->processAt()".
5. The POC analysis program("CAnalyze::beginAnalysis()" ) dispatches the target thread to thin controller("m_Thin->processFunction(addr)" ) for symbolic execution.
6. Thin controller single steps the syscall handler and conducts symbolic execution.
7. The POC analyzer terminates the analysis once the execution reaches the end of the syscall handler( See CAnalyze::onEndOfInsExec() ), and path constraints are provided for the user.
8. A sample symbolic execution trace for the symbolic execution of the syscall handler of getpriority is available in poc/poc_getpriority.trace .

Make sure to have the k-loader installed in advance (If not done already). The execution includes two sequential steps as follows.

1. On the target VM, Execute the poc target program. Go to the directory of the poc.c,

./target

2. Next, on the host, launch the onsite environment and execute KRover as follows. Go to KRover's directory,

./run-KRover.sh