Ok, I understand, but think about it. Qemu 9.x intruduces control-flow integrity, IOMMU,... nobody runs 6.2...
Maybe a subset of the full patch (just RISC-V not MIPS, just a specific CPU... On Thursday, July 31, 2025, Hesham Almatary < heshamalmat...@capabilitieslimited.co.uk> wrote: > Hello Hugo, > > On Thu, 31 Jul 2025 at 08:32, Hugo V.C. <skydive...@gmail.com> wrote: >> >> Looking this: >> >> https://github.com/CHERI-Alliance/qemu/tree/codasip-cheri-riscv_v3 >> >> I realize your patched Qemu is based on version 6.2, which is very old (2021). Do you have the patches so we try to apply them to a recent version of Qemu like 9.X or 10.X? >> > Unfortunately there is no set of patches to apply to recent QEMU > versions, rebasing/merging to a recent version is a lot of work and is > on the TODO list though, but it's not a priority at the moment. > > Regards, > Hesham >> Best, >> >> >> >> >> El mié, 30 jul 2025 a las 11:39, Hesham Almatary (< heshamalmat...@capabilitieslimited.co.uk>) escribió: >>> >>> 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
