Hello Gernot,
On Wed, 30 Jul 2025 at 12:57, Gernot Heiser via Devel <[email protected]> wrote: > > On 30 Jul 2025, at 19:39, Hesham Almatary via Devel <[email protected]> > wrote: > > > >> 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 > > That’s a somewhat courageous statement. > > For one, just because an OS is “dynamic” doesn't mean it’s “rapidly changing” > – high assurance OSes certainly don’t, verification or not. > Understood. By dynamic OS, I didn't necessarily mean high assurance, I mean something like L4Re, Linux or FreeBSD, with many commits, drivers, PRs, changes, features added everyday. Linux and FreeBSD can currently build and run memory-safe on CHERI platforms, and can in the future run on CHERI-seL4 as VMs with hypervisor enabled, when supported. > Secondly, there’s a lot of work on making verification more of a repeatable > engineering process, there’s at least a whole DARPA program committed to > this. At UNSW, we’re working on exactly this (and it surely doesn’t mean > re-writing everything in Rust). > Really looking forward to the outcome of that. Hopefully it'll make the lengthy reviewing and verification process/checks smoother and accessible to system developers with no verification expertise. > That doesn’t mean that intra-AS safety isn’t a good thing, but please don’t > over-claim. > It's intra-AS memory-safety to be specific that CHERI mainly offers to existing C/C++ projects (besides software compartmentalisation). As things stand, IMO, I don't think formal verification will be able to keep up with rapidly-changing OSes like Linux or FreeBSD, but I'd be happy to be proven wrong in the future when such tools/solutions exist. Regards, Hesham > Gernot > > Confidential communication - This email and any files transmitted with it are > confidential and are intended solely for the addressee. If you are not the > intended recipient, please be advised that you have received this email in > error and that any use, dissemination, forwarding, printing, or copying of > this email and any file attachments is strictly prohibited. If you have > received this email in error, please notify me immediately by return email > and destroy this email. > > _______________________________________________ > Devel mailing list -- [email protected] > To unsubscribe send an email to [email protected] _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
