Verified seL4 on secure RISC-V processors | Hacker News Reader

Verified seL4 on secure RISC-V processors

ts.data61.csiro.au

155 pointstodsacerdoti14 comments

From the abstract:

> We have been working for a number of years on time protection, the temporal equivalent of memory protection, as a systematic timing-channel prevention. Our experience on x86 and ARM processors is that they lack the mechanisms to do this completely. RISC-V presents an opportunity to get this right, and I will report on my experience working with the RISC-V Foundation's Security Standing Committee to get the required mechanisms into the processor specification.

Last I read, for ARM and x86 they were exploring page and cache coloring techniques for memory allocation. I'm curious if the mechanisms they'll recommend for RISC-V are in this vein (i.e. cache partitioning), or something else entirely.

Their implementation of time protection is presented here: "Prevention of Microarchitectural Covert Channels on an Open-Source 64-bit RISC-V Core". https://arxiv.org/abs/2005.02193

They use cache partitioning, but that's not the whole story. Temporal fence instruction, fence.t, is introduced.

In their first try, they cleared L1, TLB, branch history, and flushed pipeline. They discovered this is not enough, and covert timing channel persisted.

In their second try, in addition to first try, they cleared cache replacement state, cache arbitration state, and TLB replacement state. This eliminated the channel, achieving Shannon channel capacity of zero.

Given that hypervisors are essentially 4th generation microkernels plus some hardware emulation slow-path code to handle the cases where the OS kernel isn't paravirtualized to use upcalls, it would be interesting to see RISC-V boards that shipped that boot directly to seL4 from ROM as their firmware. All OS kernels for the platform would be paravirtualized.

L4 provides a pretty minimal and stable interface as a paravirtualization target. If a software ecosystem arose where a hypervisor was always present, you could get away with never implementing all of that attack surface/potentially buggy code in the hardware emulation portions of the hypervisor. The Alpha AXP showed that this sort of arrangement can be very high performance. Hopefully the RISC-V virtualization extensions would provide features (like shadow registers / separate register bank) for very light-weight transitions into and out of hypervisor mode.

In a sense, the Alpha AXP's firmware (PALCode) was a minimalist hypervisor that only supported a single guest OS. The PALCode always handled the lowest-level details, such as lowest-level interrupt handling, exception handling, and TLB / cache management. All OS kernels for Alphas (VMS, Windows NT, Tru64, Linux, etc.) were in a sense paravirtualized for the PALCode, although there were different versions of the PALCode for running VMS and Tru64 / other POSIX-y kernels. My guess is that Windows NT for Alpha AXP ran on the VMS PALCode, given Dave Cutler's role in both the NT and VMS kernels.

RISC-V booting directly to seL4 would look something like UNSW's L4/Alpha project. L4/Aplha was a port of L4 at least partially ran as Alpha AXP PALCode, replacing the normal firmware. Of course, you couldn't run VMS, Tru64, etc. on top of L4/Alpha, but L4Linux is a port of Linux to run on top of L4.

I'm not sure what I ever knew about the low level on our whizzy Alphas, but I do remember a 1970s design which had (arguably?) a microkernel in hardware/firmware, was fast, and supported an A1/B3-level OS: https://en.wikipedia.org/wiki/GEC_4000_series#Nucleus

For what it's worth, the current draft of the hypervisor extensions is available here: https://github.com/riscv/riscv-isa-manual/releases/download/... and is Chapter 5

It does say this: The hypervisor extension has been designed to be efficiently emulable on platforms that donot implement the extension, by running the hypervisor in S-mode and trapping into M-modefor hypervisor CSR accesses and to maintain shadow page tables. The majority of CSR accessesfor type-2 hypervisors are valid S-mode accesses so need not be trapped. Hypervisors can supportnested virtualization analogously.

This would be also great secure OS for chipset microcontraller (like Intel ME running Minix OS).

Except that it would still be delivered as an opaque binary blob. The GP's suggestion isn't much different from Intel's proposal for abstracting drivers into EFI Runtime Services, and many people see those as a security risk (in a "you don't control your hardware" sense, not necessarily in a "it has bugs" sense).

Outside CPU, you have microprosessors inside the chipsets (like Intel ME), network cards, mass memory devices, etc. They all have binary blobs. Better that they don't have bugs.

One thing that seL4 requires is an mmu in order to support the isolation claims. The intel me type cpu would need to have some of these features that micorcontrollers don't usually have.

>boot directly to seL4 from ROM as their firmware.

That's not a bad idea, but it just means you'd need to exploit dom0 or equivalent.

That's not necessarily true. There are VMM or hypervisor projects that utilize seL4 for x86 and ARM [1][2][3]. In this situation there isn't really one that is in "control". You could also have other threads or components that have higher privileges that can maybe do other monitoring or control activities.

1: https://github.com/seL4/camkes-vm 2: https://github.com/seL4/camkes-vm-examples 3: https://github.com/SEL4PROJ/camkes-arm-vm-manifest

This was presented in 2020-01, where proof was “due Q1’20”. FYI, Proof got finished in 2020-06: https://microkerneldude.wordpress.com/2020/06/09/sel4-is-ver...

Earlier post about SeL4 verification:

https://news.ycombinator.com/item?id=23464187

Also, my previous comment linking to how SeL4 performed the verification:

https://news.ycombinator.com/item?id=23475748

> seL4 hey used Haskell to create an model which was then their specification to help with the formal verification process [1][2].

> [1] https://dl.acm.org/doi/pdf/10.1145/1159842.1159850

> [2] https://www.sigops.org/s/conferences/sosp/2009/papers/klein-....

This seems really ideal for ECs and TPMs. I think it would be lovely to see at least one device this decade with no 0day hardware rootkits during the product life.

Reply on news.ycombinator.com