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 <kle...@unsw.edu.au> 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. <skydive...@gmail.com> 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
