[seL4] KataOS modifications to seL4

Message: 1 Date: Tue, 21 Mar 2023 10:52:40 -0500 From: June Tate-Gans (ジューン) Subject: [seL4] Bitfield generator EBNF grammar To: devel Message-ID: Content-Type: text/plain; charset="UTF-8"

Hey guys,

I've been attempting to put together some rust bindings for the seL4 fault handling mechanisms, and I'm afraid the bitfield generator is driving me a bit up a wall at this point. I'd like to find a concise grammar for the language so I can better understand how bitfield_gen.py works, but there doesn't seem to be any explicit BNF for it anywhere.

Is there a paper I should be reading or a reference guide somewhere that would help?

Thanks!

-- June Tate-Gans Software Engineer Techlead, Kata OS / AmbiML, Google

Hello June, I have a question about something I read on the announcement post for KataOS:

The current GitHub release includes most of the KataOS core pieces, including the frameworks we use for Rust (such as the sel4-sys crate, which provides seL4 syscall APIs), an alternate rootserver written in Rust (needed for dynamic system-wide memory management), and the kernel modifications to seL4 that can reclaim the memory used by the rootserver. And we've collaborated with Antmicro to enable GDB debugging and simulation for our target hardware with Renode.

Are these changes being formally verified? I understand it involves a not insignificant amount of labor to do so, but I worry about bugs being introduced that undermine the security properties of seL4 if care isn’t taken here. Thanks, Isaac Beckett PS: I decided to post this to the mailing list because I thought it may be of interest to some folks here.