WingNews logo WingNews GitHub [2]

jesse_m's comments

jesse_m | 5 years ago | on: Verified seL4 on secure RISC-V processors

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.

jesse_m | 5 years ago | on: Verified seL4 on secure RISC-V processors

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

jesse_m | 5 years ago | on: Verified seL4 on secure RISC-V processors

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.

jesse_m | 5 years ago | on: Technical reasons to choose FreeBSD over GNU/Linux

Is the ports system similar to Gentoo's portage/ebuild system? I can get sources, configure the build, or get binaries (for some things) pretty easy through it.

The QA with the build farm would be nice though.

jesse_m | 6 years ago | on: SeL4 Design Principles

I think one of the big things here is that the refinement proofs from the models for isolation, IPC fast path, capability access control, and scheduling to C source to binary are strongest when the kernel is built with a particular configuration on particular hardware. When all of these are satisfied and you are on a trusted platform, you have very very strong guarantees that what is modeled is what you get. But it's not like this is hidden. They have make it pretty clear what the verified platforms and configurations are[1].

You should take a look at the verification chain though[1]. It is fairly extensive. It's not like they proved just a small part of a system in a general way.

1: https://docs.sel4.systems/Hardware/

2: https://github.com/seL4/l4v

page 1
more