Hi guys, maybe a stupid question but I wonder if we can have formal verification of CHERI C (purecap) mode programs that run on a CHERI-enabled seL4?
I mean, we are all on the same boat and as dinosaur 0day exploit writer that have bypassed almost any OS security protections that exist, I can see here two amazing technologies: formal verification and hardware enforcement. I love both. I know that may look like redundant but... can we have both or am I missing something? Best, El mié, 30 jul 2025 a las 14:04, Gernot Heiser via Devel (<devel@sel4.systems>) escribió: > On 30 Jul 2025, at 19:39, Hesham Almatary via Devel <devel@sel4.systems> > 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. > > 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). > > That doesn’t mean that intra-AS safety isn’t a good thing, but please > don’t over-claim. > > 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 -- 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
