Message: 1 Date: Tue, 21 Mar 2023 10:52:40 -0500 From: June Tate-Gans (ジューン) jtgans@google.com Subject: [seL4] Bitfield generator EBNF grammar To: devel devel@sel4.systems Message-ID: CAOPTAH0q0UABvFhffnmJ6ygDuPmpf8fMjxBawmYbhCjjJT8MTA@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.
The plan is to ultimately verify these changes longer term, along with the Rust work we're doing in the userland, but as you said, verification is a monumental task and this is a small research project with two people staffing it at the moment, so it may take us a while to get there.
We'd appreciate a second look on it and any constructive comments you might have, or any patches to help us out -- it's one of the reasons we pushed to get it all out in the open, in fact. If you know of a better way of doing things, we'd absolutely love to hear it, but bear in mind this is most definitely a research project and not something we expect to be used in production without additional work.
All in all, most of the changes we have in the kernel repository are focused on the boot process, devicetree and PLIC/timer drivers for our specific platform. We've made one change to provide a way to reclaim rootserver resources, and if you look at the archives of this mailing list, you'll find requests from us about how to go about this problem appropriately. Before we made this change, we worked with core developers both on and off this list to make sure we could thread the needle here.
On Tue, Mar 21, 2023 at 9:33 PM Isaac Beckett isaactbeckett@gmail.com wrote:
Message: 1
Date: Tue, 21 Mar 2023 10:52:40 -0500 From: June Tate-Gans (ジューン) jtgans@google.com Subject: [seL4] Bitfield generator EBNF grammar To: devel devel@sel4.systems Message-ID: CAOPTAH0q0UABvFhffnmJ6ygDuPmpf8fMjxBawmYbhCjjJT8MTA@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.
On Mar 22, 2023, at 11:56 AM, June Tate-Gans jtgans@google.com wrote:
The plan is to ultimately verify these changes longer term, along with the Rust work we're doing in the userland, but as you said, verification is a monumental task and this is a small research project with two people staffing it at the moment, so it may take us a while to get there.
We'd appreciate a second look on it and any constructive comments you might have, or any patches to help us out -- it's one of the reasons we pushed to get it all out in the open, in fact. If you know of a better way of doing things, we'd absolutely love to hear it, but bear in mind this is most definitely a research project and not something we expect to be used in production without additional work.
All in all, most of the changes we have in the kernel repository are focused on the boot process, devicetree and PLIC/timer drivers for our specific platform. We've made one change to provide a way to reclaim rootserver resources, and if you look at the archives of this mailing list, you'll find requests from us about how to go about this problem appropriately. Before we made this change, we worked with core developers both on and off this list to make sure we could thread the needle here.
Nice! I’m glad this has been thought about. While I don’t doubt you or your colleagues’ competence as individuals, I had worried the profit incentive from Google (especially the desire for a return on investment) could lead to hasty decisions that would lead to fatal flaws that would be expensive to fix. Hopefully more eyes on this will be helpful too!
Also, KataOS seems like it would provide a useful starting point for tinkering with embedded devices running seL4, which is something I’ve thought about but been hesitant about because of my lack of experience in this field. I’ll definitely be looking closer at it.
Thanks, Isaac Beckett
-
Isaac Beckett -
June Tate-Gans (ジューン)