Fall 2024 progress report

The year concludes with the addition of 300 commits to Miralis and successful deployment of Debian running securely on ACE with a policy that isolates the linux kernel from the OpenSBI firmware (see image below). We can run the classical commands There have been some changes in the composition of the Miralis team, Frédéric and I are replacing Sofia and Noé. Additionally, we have open-sourced a second tool, Virt-Sail, a transpiler currently under development that converts Sail code into Rust.

3 new security policies

Building on the strong momentum established by Sofia and Noé, Charly, Frédéric, and I have developed three security policies. Additionally, Miralis can now boot various Linux distributions, including Ubuntu, Fedora, OpenSUSE, and Debian. Charly focused on virtualizing interrupts, Frédéric took responsibility for integrating the Keystone security monitor, and I focused on integrating the ACE security monitor, isolating the Linux kernel from the firmware, and resuming development on Virt-Sail.

ACE - secure the confidential virtual machines!

ACE is a security monitor for confidential virtual machines, built on the CoVE specification presented at a workshop by IBM Research. Currently, ACE operates alongside OpenSBI and requires the firmware to be part of the root of trust.

I developed a demonstration showcasing how the ACE security monitor can be collocated with Miralis. The process began with emulating the hypervisor extension in Miralis, which ACE requires. The most challenging and interesting aspect was merging the two security monitors.

The architecture is based on the following principle:

• When the firmware is running, Miralis serves as the security monitor responsible for handling security operations.
• When the payload or confidential virtual machines are active, ACE becomes the active security monitor.

A "monitor context switch" is performed during transitions between the firmware and payload, transferring control of the system from one security monitor to the other. After a few intense debugging sessions with GDB, ACE is now able to launch a confidential virtual machine with a virtual firmware monitor. Success! 🎉

Keystone - secure the confidential enclave!

The second policy, simply named the "Keystone Policy," is a rust reimplementation of the open-source Keystone framework. The Keystone security monitor provides a Trusted Execution Environment (TEE) framework for RISC-V platforms and its primary goal is to enable the secure and isolated execution of user applications (enclaves) while protecting them from malicious software, untrusted operating systems, or even hypervisors

Frédéric reimplemented Keystone in Rust and adapted it into a policy that works seamlessly with Miralis. He is currently fixing the last few issues.

Strict protect payload - secure the linux kernel!

Last but not least, in a more general case, we aim to isolate the Linux kernel from untrusted firmware. The final policy we present here is the Protect Payload policy.

This policy is the smallest of the three and is responsible for isolating the firmware from the operating system. The firmware can no longer access the payload’s memory, thanks to PMP entries, and registers are cleared between each world switch, except for registers a0-a7, which are preserved for ecalls. Additionally, we implemented an attestation mechanism to verify that the firmware properly loads the payload before jumping to it.

On the hardware side, we also had to implement emulation for misaligned loads and stores since we can no longer rely on OpenSBI for this functionality. Currently, we can boot Linux kernels for Fedora, openSUSE, and Ubuntu (in recovery mode), with the OS memory isolated from the firmware.

Virt-sail - verify the hypervisor!

In the KISV paper, we presented an initial draft for formally verifying the MRET instruction. We have since revisited this project and are now developing a transpiler capable of translating the instructions that virt.rs aims to emulate. An example is shown below, and the source code (currently under development) is available here.

#![allow(unused, non_snake_case, non_upper_case_globals, non_camel_case_types, bindings_with_variant_name)]

use sail_prelude::*;

const xlen: usize = 64;
const xlen_bytes: usize = 8;

type xlenbits = BitVector<xlen>;
type priv_level = BitVector<2>;
type regidx = BitVector<5>;
type cregidx = BitVector<3>;
type csreg = BitVector<12>;
type Mstatus = BitVector<64>;

struct SailVirtCtx {
    PC: xlenbits,
    nextPC: xlenbits,
    mepc: xlenbits,
    sepc: xlenbits,
    uepc: xlenbits,
    mstatus: Mstatus,
    cur_privilege: Privilege,
    Xs: [xlenbits;32],
}

#[derive(Eq, PartialEq, Clone, Copy, Debug)]
enum Privilege {
    User,
    Supervisor,
    Machine,
}

fn haveUsrMode(sail_ctx: &mut SailVirtCtx) -> bool {
    true
}

fn privLevel_to_bits(sail_ctx: &mut SailVirtCtx, p: Privilege) -> BitVector<2> {
    match p {
        Privilege::User => {BitVector::new(0b00)}
        Privilege::Supervisor => {BitVector::new(0b01)}
        Privilege::Machine => {BitVector::new(0b11)}
    }
}

fn privLevel_of_bits(sail_ctx: &mut SailVirtCtx, p: BitVector<2>) -> Privilege {
    match p {
        b__0 if (b__0 == BitVector::new(0b00)) => {Privilege::User}
        b__1 if (b__1 == BitVector::new(0b01)) => {Privilege::Supervisor}
        b__2 if (b__2 == BitVector::new(0b11)) => {Privilege::Machine}
        _ => {not_implemented(String::from("Invalid privilege level"))}
    }
}

fn pc_alignment_mask(sail_ctx: &mut SailVirtCtx) -> BitVector<64> {
    !(BitVector::<64>::new(BitVector::new(0b10).bits()))
}

fn _get_Mstatus_MPIE(sail_ctx: &mut SailVirtCtx, v: Mstatus) -> BitVector<1> {
    v.subrange::<7, 8, 1>()
}

fn _get_Mstatus_MPP(sail_ctx: &mut SailVirtCtx, v: Mstatus) -> BitVector<2> {
    v.subrange::<11, 13, 2>()
}

fn set_next_pc(sail_ctx: &mut SailVirtCtx, pc: BitVector<64>) {
    sail_ctx.nextPC = pc
}

fn handle_illegal(sail_ctx: &mut SailVirtCtx) {
    
}

fn get_xret_target(sail_ctx: &mut SailVirtCtx, p: Privilege) -> BitVector<64> {
    match p {
        Privilege::Machine => {sail_ctx.mepc}
        Privilege::Supervisor => {sail_ctx.sepc}
        Privilege::User => {sail_ctx.uepc}
    }
}

fn prepare_xret_target(sail_ctx: &mut SailVirtCtx, p: Privilege) -> BitVector<64> {
    get_xret_target(sail_ctx, p)
}

fn exception_handler(sail_ctx: &mut SailVirtCtx, cur_priv: Privilege, pc: BitVector<64>) -> BitVector<64> {
    let prev_priv = sail_ctx.cur_privilege;
    sail_ctx.mstatus = {
        let var_1 = _get_Mstatus_MPIE(sail_ctx, sail_ctx.mstatus);
        sail_ctx.mstatus.set_subrange::<3, 4, 1>(var_1)
    };
    sail_ctx.mstatus = sail_ctx.mstatus.set_subrange::<7, 8, 1>(BitVector::new(0b1));
    sail_ctx.cur_privilege = {
        let var_2 = _get_Mstatus_MPP(sail_ctx, sail_ctx.mstatus);
        privLevel_of_bits(sail_ctx, var_2)
    };
    sail_ctx.mstatus = {
        let var_3 = {
            let var_4 = if haveUsrMode(sail_ctx) {
                Privilege::User
            } else {
                Privilege::Machine
            };
            privLevel_to_bits(sail_ctx, var_4)
        };
        sail_ctx.mstatus.set_subrange::<11, 13, 2>(var_3)
    };
    if (sail_ctx.cur_privilege != Privilege::Machine) {
        sail_ctx.mstatus = sail_ctx.mstatus.set_subrange::<17, 18, 1>(BitVector::new(0b0))
    } else {
        
    };
    (prepare_xret_target(sail_ctx, Privilege::Machine) & pc_alignment_mask(sail_ctx))
}

#[derive(Eq, PartialEq, Clone, Copy, Debug)]
enum Retired {
    RETIRE_SUCCESS,
    RETIRE_FAIL,
}

#[derive(Eq, PartialEq, Clone, Copy, Debug)]
enum ast {
    MRET(),
}

fn ext_check_xret_priv(sail_ctx: &mut SailVirtCtx, p: Privilege) -> bool {
    true
}

fn ext_fail_xret_priv(sail_ctx: &mut SailVirtCtx) {
    
}

fn execute_MRET(sail_ctx: &mut SailVirtCtx, TodoArgsApp: TodoUnsupportedUnionSignature) {
    if (sail_ctx.cur_privilege != Privilege::Machine) {
        handle_illegal(sail_ctx);
        Retired::RETIRE_FAIL
    } else if !(ext_check_xret_priv(sail_ctx, Privilege::Machine)) {
        ext_fail_xret_priv(sail_ctx);
        Retired::RETIRE_FAIL
    } else {
        {
            let var_5 = exception_handler(sail_ctx, sail_ctx.cur_privilege, sail_ctx.PC);
            set_next_pc(sail_ctx, var_5)
        };
        Retired::RETIRE_SUCCESS
    }
}

Next steps

We are currently facing some issues with the graphical interface that we plan to fix. We'll start by resolving this issue, followed by running benchmarks on the board to accurately measure the overhead under real-world conditions. Afterward, we will complete Virt-sail and add formal verification to the CI/CD tests to formally validate virt.rs, the part of the implementation responsible for emulating the virtual firmware.

Meanwhile, Charly is working on formalizing the definition of the firmware monitor using a theorem prover to extend the criteria set by Popek and Goldberg. On his end, Frédéric is focused on completing the integration of Keystone on the board.