> Message: 1 > Date: Tue, 21 Mar 2023 10:52:40 -0500 > From: June Tate-Gans (ジューン) <[email protected]> > Subject: [seL4] Bitfield generator EBNF grammar > To: devel <[email protected]> > Message-ID: > <caoptah0q0uabvfhffnmj6ygdupmpf8fmjxbawmybhcjjjt8...@mail.gmail.com> > 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. _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
