Hi Hugo, On Wed, 30 Jul 2025 at 10:07, Hugo V.C. <skydive...@gmail.com> wrote: > > I read the pull discussion here: > > https://github.com/seL4/seL4/pull/1469 > > you say: > > "This port has been tested with Microkit on Codasip's QEMU and hardware > platforms (x730)" > > is Codasip's QEMU a custom QEMU to support x730? > Yes, it's a QEMU fork that adds a machine (currently called hobgoblin, but will be Codasip Prime in the next release) with CHERI support that's almost exactly the same as X730 hardware; code that runs on it also runs out of the box on X730. You can find it here https://github.com/CHERI-Alliance/qemu/tree/codasip-cheri-riscv_v3
> also, this question is for seL4 Foundation: are there plans to formal verify > seL4 with this changes? > > I thing you guys have put together two different Worlds that open a powerful > new field: software formally verfied (seL4) + hardware enforced "memory > protection". I a real World where very few orgs have the (intellectual) > capability of formally verify all the software they use (specifically C/C++), > Cheri support on top of seL4 looks very interesting to "CHERI support in > Microkit lets you run legacy C/C++ (non-CHERI), memory-safe C/C++ (using > CHERI capabilities), and Rust programs in distinct protection domains". > Exactly. Formal verification works great on a slowly moving delveoplement project such as the seL4 microkernel itself, but once you start building an actual dynamic OS on top of seL4 that'll need to keep rapidly changing and is an order of magnitude bigger in size, formally verifying this C/C++ codebase is really impractical and won't be scalable, let alone having the scarcity of experts to do so. So your options are to 1) (re)write everything in Rust (which also requires a relatively rare intellectual capability), or 2) use something like CHERI which is arguably just "good practice, clean C/C++ code" from an application developer perspective. > And as we already have LionsOS, so we get a third option (old CamkES. > LionOS/Microkit, Cheri-seL4). It is not competition, it is evolution just > following different valid paths. ANY of those paths is 1000 times better than > current OSs/solutions. I love to have different options, all around seL4. > LionsOS/Microkit, CAmkES, or pretty much any C/C++ userspace framework (e.g., sel4test, sel4bench, Kry10 OS, etc) could be ported and run on CHERI-seL4 (the CHERI-enabled microkernel itself). We hope there will be opportunities in the future (especially once we have commercial CHERI processors people can buy) to formally verify the CHERI extensions in the kernel (e.g., the PR we submitted), and we're happy to collaborate on that. > I wish you guys collaborate to expand seL4 ecosystem. > > Best, > > On Tuesday, July 29, 2025, Hesham Almatary > <heshamalmat...@capabilitieslimited.co.uk> wrote: > > Hello Hugo, > > On Tue, 29 Jul 2025 at 18:26, Hugo V.C. <skydive...@gmail.com> wrote: > >> > >> Hi Hesham, > >> > >> 2 questions: > >> > >> do you run a modified seL4? > > > > Yes definitely, as mentioned in the blog post. The link to the fork [1] is > > in the blog post and we’ve submitted a PR [2] upstream for it (also in the > > blog post). > > [1] https://github.com/CHERI-Alliance/CHERI-seL4 > > [2] https://github.com/seL4/seL4/pull/1469 > >> > >> is there any real world example of a Rust app running on top of you > >> solution? > > > > I’ve built and run Microkit’s Rust hello example on top without any issues. > > You can also reproduce that if you’d like. Happy to give further > > instructions if needed. > > Regards, > > Hesham > >> > >> Best, > >> > >> On Tuesday, July 29, 2025, Hesham Almatary via Devel <devel@sel4.systems> > >> wrote: > >> > Hello, > >> > > >> > The CHERI Alliance has released a prototype of CHERI-seL4, an > >> > experimental version of the seL4 microkernel with CHERI support. This > >> > release includes CHERI-Microkit, a lightweight userspace framework, > >> > and a set of exercises and tutorials designed to help developers > >> > explore CHERI’s potential in a real microkernel environment. > >> > > >> > The release is aimed at developers who want to build and experiment > >> > with memory-safe C/C++ software on seL4. It supports the draft > >> > CHERI-RISC-V architecture and runs on QEMU, Codasip’s X730 processor, > >> > CHERI-Toooba, and CHERI-CVA6 on FPGA. > >> > > >> > For those who are unfamiliar with CHERI, CHERI support in seL4 enables > >> > memory-safe C/C++ user-level projects and applications without having > >> > to (re)write code in languages like Rust. This complement's seL4's > >> > strong isolation between different components, enforced by the MMU and > >> > seL4's software capabilities. > >> > > >> > We welcome any feedback. > >> > > >> > Learn more: > >> > https://cheri-alliance.org/cheri-sel4-and-cheri-microkit-released/ > >> > > >> > Regards, > >> > Hesham > >> > _______________________________________________ > >> > Devel mailing list -- devel@sel4.systems > >> > To unsubscribe send an email to devel-leave@sel4.systems > >> > _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
