[seL4] Re: Potential vulnerabilities

HI Hugo, The CHANGES.md file lists the vulnerable versions of seL4 for each of

Hi Gerwin, thanks for the fast response! Yes, this.I already know. But I'm interested in this specific case: https://docs.sel4.systems/projects/sel4webserver/ as I guess it may not vulnerable as this example (by default) does not run SMP seL4. For "for cache maintenance ops" I'm not sure as this qemu environment. Any hints? On Tuesday, November 5, 2024, Gerwin Klein wrote: these (https://github.com/seL4/seL4/blob/master/CHANGES.md)

- for VCPU/SMP: seL4 versions 12.0.0 and 12.1.0. - for cache maintenance ops on AArch64: all versions before 13.0.0 from 5.0.0 Cheers, Gerwin

On 5 Nov 2024, at 10:02, Hugo V.C. wrote: I'm forwarding this question here (tried on Mattermost Trustworthy Systems group first) hoping someone can put some light on this?

---

Hi, I'm having a look to the vulns (in areas of the kernel that have not been formally verified) patched in seL4 13.0.0.

We have:

1) "NULL pointer dereference when injecting an IRQ for a non-associated VCPU on SMP configurations." 2) "On AArch64, when seL4 runs in EL1 the kernel would fault with a data abort in seL4_ARM_Page_Invalidate_Data and seL4_ARM_VSpace_Invalidate_Data when the user requested a dc ivac cache maintenance operation on a page that is not mapped writeable."

Extremely simple question: running version < 13.0.0 on top of Qemu (in example like https://docs.sel4.systems/projects/sel4webserver/) would it be vulnerable to any of those?

---

Best, _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems