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? 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". 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. 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
