[seL4] Re: Potential vulnerabilities

15 Nov 2024

      Sorry if this is unwelcome, but this discussion is a bit alarming. If there
is a conceivable exploit anywhere, it is a vulnerability that should be
contained. I wrote a post about Murphy's Law because the entry on it in
Wikipedia is woefully incorrect and it appears that somehow the zeitgeist
now has Murphy's Law as just a humorous observation and nothing more. It's
a real thing that systems people should understand and respect.

https://blog.bobtrower.com/2024/06/murphys-law-is-not-simply-adage.html

Note that you can comfortably say that a given random selection from, say,
2^1024 is improbable to the point of impossibility, but you *cannot* be
certain that the selection is random.

Cheers!

On Thu, Nov 7, 2024 at 3:31 PM Hugo V.C.  wrote:
...
"But it's still very unlikely, as all they can write is 1
to limited memory targets."
Interesting. Moreover as we are talking about a system with static memory
definitions (no need to bypass any KASLR...) so, if the attacker is very,
very lucky and the overwrited memory region is profitable, we would have an
ultrareliable exploit. But as per your explanations, look very difficult.
BTW: writing "1" in the right place can be fatal. Would be nice to test
what ca be achieved.
"Usually customers understand their own system enough to know whether
...
a bug affects their system or not."
Unfortunately here I strongly disagree. My experience is many times even
the software developers don't get the full impact of a bug (that's why we
have those patches for vulns in well known OSs that don't really patch and
things get exploited again).
When it comes to memory bugs, things can become very weird in terms of
knowing the impact. Fortunately in seL4 environment bugs impact are
"easier" to be defined as things in the kernel are "static". The bad news
is this also helps attackers.
If I were you guys I would create an exploitable environment and would try
to exploit it. Just for fun. Just to learn. Maybe you get a surprise.
On page 210 of this document (https://www.pentest.es/checkpoint_hack.pdf)
there's (at that time, year 2007, a 0day) for a memory vulnerability that
was supposed to be "almost impossible to exploit" as there were many
protections in place. At the end an exploit was possible. It took me few
months, but I did it. At that time ROP technique still didn't existed (in
fact this document is the genesys) so exploitation was painful. Nowadays
everything is automated.
If there's a way to exploit the bug you described, I bet it will be
exploited.
Attackers like to learn.
Probably someone is reading this and considering seL4 targets military
environments, yes, looks interesting.
And almost never you will have 100% verified code, so to me looks very
interesting to research what is the impact of bugs in unverified code when
they interact with verified code.
Maybe we learn something. And for sure we will have fun.
On Thursday, November 7, 2024, Indan Zupancic  wrote:
...
Hello Hugo,
On 2024-11-07 08:09, Hugo V.C. wrote:
...
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.
The bugs are normally limited to halting the kernel in both cases for all
user space setups:
- The cache invalidate causes a halt because there is no write access.
  This is a user space app calling cache maintenance syscalls on a page
  cap that is mapped read-only. Here seL4 was more permissive than the
  actual hardware. The only problem is the kernel halt, there are no
other
  side effects.
- The VCPU bug only affects ARM SMP configurations (otherwise it would
have
  been found by verification). Normally the kernel has no memory mapped
at
  address 0, you can check the memory map to verify if this is the case
for
  your platform. If there is no mapping for address 0, the kernel will
halt
  and there are no other side effects.
The rest of the analysis is for the highly unlikely case that you do run
an unverified kernel build on SMP ARM with HYP enabled, where an
untrusted
or compromised task has a cap to a disassociated VCPU, with a kernel that
has memory mapped starting at address 0:
If for some reason it has, the NULL access itself is limited to a read of
the NULL TCB's affinity, which will be used to decide whether to send an
IPI
and to which core (offset depends on the size of arch_tcb_t, but will be
less than 4kb). If you have device memory at that address, that read may
have some side effect (although I think ARM hardware usually doesn't).
Otherwise that invalid read itself will have no side-effects and is
harmless.
If it reads a valid core affinity, then things end up harmless:
handleVCPUInjectInterruptIPI() will handle the IPI and do what was
requested,
it doesn't use or touch the NULL TCB in any way, it just does some
internal
bookkeeping.
If it reads an invalid core affinity, things get more interesting. It
will
try to send an IPI to core >= NUM_CORES. This results in an out-of-bound
write
past big_kernel_lock.node_owners[] in generic_ipi_send_mask(). The write
is
limited to writing the value '1' to the third word in one 64 or 32 bytes
aligned
chunk past the big kernel lock, limited in range to about 64 or 32 * 64
bytes,
for 64-bit and 32-bit platforms respectively (less if L1 cache lines are
32 bytes).
You can check your kernel.elf binary to see what could be affected this
way if
you're interested. If you're unlucky it's within range of the kernel
stack and
the attacker can modify one stack word to the value of 1.
Assuming the attacker has no control over memory content at address
0-4kb, this
is most likely useless, as they can't choose the address, nor the value
written.
This one write is all they get, because after that the kernel will hang
forever
in ipi_wait(), without releasing the big kernel lock, so any write they
did to
kernel memory can't affect other cores either.
If the attacker has control over address range 0-4kb and all other
requirements
are met, and the attacker gets very lucky, then the VCPU bug might be
enough to
take over the system. But it's still very unlikely, as all they can write
is 1
to limited memory targets. That one write has to both escalate privileges
and
avoid the hang in ipi_wait() to be useful. They can't unlock the kernel
lock
because that requires a write of 0 to the wrong offset.
...
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.
Usually customers understand their own system enough to know whether
a bug affects their system or not. An analysis like I did above is
required for your specific system before you can be assured that
known bugs don't affect your systems.
Greetings,
Indan
...
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
-- 
Bob Trower
--- From Gmail webmail account. ---