The SeL4 Microkernel: An Introduction [pdf]

https://sel4.systems/About/seL4-whitepaper.pdf

On Apple Exclaves. Enhancing kernel isolation, one step at… | by Random Augustine | Feb, 2025 | Medium

Link

Ein Meilenstein für IT-Sicherheit: Die @Cyberagentur hat am 20.01.2025 fünf Verträge für das Forschungsprogramm „Ökosystem vertrauenswürdige IT“ (ÖvIT) unterzeichnet. Ziele: Beweisbare IT-Sicherheit und ein internationales Netzwerk von Experten.
Mehr Informationen: https://t1p.de/8mb4c
#ÖvIT #Cybersicherheit #FormaleVerifikation #Forschung #seL4

Running the manual: an approach to high-assurance microkernel development
> the kernel is obviously a state
transformer, and hence, conveniently represented as a monad. This
choice is reaffirmed by the need for recoverable exceptions, which
are detailed in the next subsection. In fact, we will see that we want
to distinguish between code that may raise recoverable exceptions
and code that does not have that liberty. Hence, it is worthwhile
to use monad transformers as provided by the MTL in the Haskell
Hierarchical Libraries
> seL4 API includes several system calls that
attempt to manipulate a capability address space, which is a data
structure containing a sparse mapping from addresses to capabili-
ties. If one of these system calls fails to locate a specified capability,
it will generate a system call error that is returned to the caller. On
the other hand, a similar failure while searching for a capability that
is being directly invoked will generate a fault message that is sent
to the current thread’s fault handler; a failure while trying to trans-
mit a capability through a one-way communication channel will be
silently ignored when the receiver is unable or unwilling to receive
the capability.
> HOL is a logic of total functions and is as such not suitable to ex-
press the semantics of Haskell directly. It is however suitable to
describe the semantics of Haskell functions that always terminate
and that do not make essential use of laziness. The seL4 implemen-
tation consists of such functions.

#haskell #isabelle #sel4
http://portal.acm.org/citation.cfm?id=1159842.1159850&coll=portal&dl=ACM&type=series&idx=1159842&part=Proceedings&WantType=Proceedings&title=Haskell&CFID=18785943&CFTOKEN=93152956

if you port #seL4 to a new architecture, you’ll end up with a portion of code that has undergone formal verification in a different context, and a portion that is new and has not undergone formal verification yet. If the new architecture is similar to existing architectures, that new code is probably following patterns similar to the ones used in verified code.

None of that constitutes a new proof or gives any guarantees, but compared to an implementation that is entirely new code and has only undergone normal testing, there are still some benefits. The verified generic code can still fail in a new context, when it is used in ways that doesn’t satisfy its preconditions
https://sel4.discourse.group/t/is-there-any-value-to-porting-sel4-to-a-platform-without-also-verifying-the-port/77/4

Each of #seL4 ’s verified configurations target a single hardware/platform configuration. This specificity drasticially simplifies the proofs and also allows them to refer to a more accurate model of the platform/hardware.

The tradeoff is that changes to the hardware/platform configuration also require changes to the proofs and, because of correspondence requirements, also to the C source implementation of the kernel. As the kernel ABI is described by the C implementation of the kernel, the ABI can only target a single hardware/platform configuration at a time. There is tooling to make it easier to switch hardware/platform configurations across different kernel configurations, but this must all happen before the kernel is compiled; this is why there are lots of C preprocessor macros used in all the definitions.

This isn’t something that is impossible to change, but would require a very large investment into the verification to support it.
https://sel4.discourse.group/t/pre-rfc-specify-a-fixed-kernel-abi-for-each-architecture/145/19

Oh wow, I wasn't aware that #seL4 Foundation has uploaded the lectures of #UNSW's famous Advanced Operating Systems course to youtube.

https://www.youtube.com/watch?v=IvqM2pmApSY&list=PLtoQeavghzr3nlXyJEXaTLU9Ca0DXWMnt
#os #microkernel #operatingsystems

@riskybusiness RE your discussion about viewing iPhone on macOS - I’m 99% sure this is a direct device to device connection, iCloud isn’t involved other than the devices being on the same account and having shared secrets/keys.

It’s not that different from the current implementation that lets you use an iPad as a second screen over wifi - it’s designed for the “my phone is in my pocket/over there charging and I don’t want to get it” use case, not the “my phone is at home and I want to stream its screen over the internet” case - unless I’ve missed something? I’d be shocked if it weren’t encrypted using keys in each device’s Secure Enclave.

Somewhat unrelated, but this also reminds me of some tech DST Group showed me years ago when we were teaching them. It allowed a user to use an untrusted web browser/computer to connect to a Remote Desktop-esque page, but the image was encrypted They had a device which sat between the computer and monitor which decrypted the image signal, and encrypted keyboard/mouse data back to the page. (All built on #seL4 of course).

In the first of our #EverythingOpen schedule highlights, we're delighted to present #UNSW Scientia Professor @gernot who will present on efforts to take #sel4 from a #MicroKernel to fully-fledged #OS
with #LionsOS, named for open source luminary, John Lions.

Schedule will be posted soon, we promise!

Heavily discounted #EarlyBird #EB tickets still available, for a short time only:
https://2024.everythingopen.au/news/registrations-open/

Interestingly, #seL4 would be a worse choice that #Xen for #QubesOS, due to its worse support for x86 speculative execution mitigations. Xen typically provides patches the day the embargo breaks, and Qubes OS users rely on that. There are various ways to make speculative execution less of a concern, but they don’t work for Qubes OS. This is because Qubes OS heavily overcommits CPU and allows execution of arbitrary untrusted code in VMs.

I don’t fault the seL4 developers for not focusing on a use-case that is practically the worst-case scenario for it. It just means that Qubes OS is very much more like a server than an embedded system, and so it needs a hypervisor that is designed for the kinds of workloads it runs.

Last year when the #seL4 Team won the ACM Software System Award, most of the awardees agreed to pool the price money for a PhD scholarship. This is now open for applications: https://trustworthy.systems/students/schol-swsa

Anyone here using #seL4 and #Rust on Cortex-M? Cortex-A?

Or more broadly, anyone here using seL4 at all? Can I pick your brain a bit?

systems beyond #posix: #sel4

https://www.youtube.com/watch?v=ekV7wWQf7_g
#microkernel #os

Just catching up on YouTube videos for the evening, when I found this #seL4 presentation for #CorePlatfrom and I could not help but notice the parallelism of the concept I talked about this week for #microkernel and #stacks. I do feel a sense of elegance in the Stack approach I propose. Thoughts? https://github.com/jemo07/MicroKernelIdeas/blob/main/IPC_Stack_Design.md