[seL4] Re: Potential vulnerabilities

Hi Hugo, Sorry I misread you first email. Looking at the sel4webserver setup, it does not seem to use SMP, so this application is not affected by the SMP/VCPU problem. The documentation is only for AArch32, but the application does work for AArch64 and is tested for AArch64. To answer whether the application can be affected by the cache operation vulnerability, the main question is what is considered to be trusted and under what threat model. A reasonable threat model would be to treat the outside network as malicious, and the VM(s) and VMM as known, initially

There are two configurations of the app, one with a single VM that serves

Because the VMM is not formally verified, we usually treat the VMM and

Even if all of this happened, the only consequence would be a system halt. Indan’s threat model was that if the VM is compromised, the main purpose of the application (serving web pages) is already compromised, so the additional vulnerability does not really matter. It would only lead to an additional opportunity for a system halt. The whole thing comes down to that this web server demo is more a demo on how to run a useful VM on top of seL4 than on how to do a secure web server on top of seL4. A more secure design would be the one that currently serves

Cheers, Gerwin

On 7 Nov 2024, at 09:09, Hugo V.C. wrote: 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

Nice Gerwin. Thanks. Just to make a more spicy debate, "A reasonable threat model" well, "reasonable" is what defender wants to achieve. In example, you talk about "it must first subvert Linux with full root-level code execution"... ok, this is too easy. I don't trust Linux since Grsecurity patches went closed source... Vanilla Linux security is a toy. So, to me, Linux is just a "big boy" application. There are lot of kernel and user space apps 0days for getting root. So once clarified this, I assume Linux is already compromised or, a more "real world" use case: I want to give Linux root access to users. An seL4 must stop them from reaching the host. I know is not that easy... All VMM code there... so, if I give you a root shell in a seL4 webserver example ("Testing the web server (qemu-arm-virt)", https://github.com/seL4/sel4webserver) with a compilation evironment (to build an exploit): you can only crash seL4? Or you think you (with your deep know how of seL4) would be able to do more nasty things against the underlying host? Be careful, you are a step away to write the first ever exploit for (demo) seL4 system... ;-) On Thursday, November 7, 2024, Gerwin Klein wrote: trusted code, where the VM(s) may be compromised by attack, because they run Linux. directly to the network and one with a separate VM for network interaction. For this vulnerability I think both can be treated the same (although the one with separate network VM has a smaller attack surface): for a network attack to be able to actually perform the vulnerable syscall, it must first subvert Linux with full root-level code execution, then the VM must subvert the VMM with full code execution, then find an untyped capability or existing frame capability that the VMM possesses (it does possess some), from which to then create a non-writeable mapping, and then make the syscall. the VM as being in the same security domain for analysis, but in this case it makes sense to look more closely. Without formal verification there is no guarantee that the full code execution step from VM to VMM cannot happen, but I can’t see any scenario or currently known kind of attack where that would actually be possible. So I would rate the risk as very low. the se4L website (https://sel4.systems/Info/Website/), but it is still a bit early for general production use. 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,

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