[seL4] Re: Potential vulnerabilities

Hi Indan, thanks for the explanation. Anyway, still not clear to me 🙏. Let me clarify my risk model. 1) I don't care abour user space (Linux/web server) crashes 2) Suppose I have a webserver example with a "vulnerable" seL4 kernel version I'm a bit concerned about "But those operations, if done in good faith". So to be even more precise: In a "webserver example" of year... 2022? (which will be running an old seL4 version), as is, with no modifications from what was published at that time: Can or can not the kernel be crashed in a exploitable way? An seL4 system halt is not a problem to me. An execution manipulation at kernel level it would be. A halt is a halt. No problem. But seL4 is formally verified, so, my concern is if an attacker can do more than halting the seL4. This kind of questions are not just for fun guys, this is what customers will ask you every single time a non verified code bug arises. And the infosec community needs that kind of analysis to increase trust. Thank you in advance 🙏 On Tuesday, November 5, 2024, Indan Zupancic wrote:

Hello Hugo,

The bugs you listed are only a problem for untrusted code. That is, it gives threads with vcpu control or vspace caps the ability to cause a system halt, effectively giving them more rights than they should have, hence it being a vulnerability. But those operations, if done in good faith, would be user space bugs.

In the case of the webserver example, if you can trigger either of the two bugs in any way, with a current kernel it will avoid the kernel crashing, but it will still mean your user space will most likely be broken, resulting in the same end user experience of a non-working system. Because as far as I know, the webserver example has no fault detection, recovery or restart mechanism implemented.

Greetings,

Indan

On 2024-11-05 10:34, Hugo V.C. wrote:

...

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:

...

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

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,