Skip to content Skip to footer

The SeL4 Microkernel: An Introduction [pdf] by snvzz

5 Comments

  • Post Author
    coldblues
    Posted March 23, 2025 at 2:40 pm

    https://genode.org/index

    An operating system with seL4 support

  • Post Author
    hackpelican
    Posted March 23, 2025 at 2:47 pm

    Does the OS that lies on top of this kernel need to be formally verified as well for the security guarantees to hold?

  • Post Author
    nimish
    Posted March 23, 2025 at 3:32 pm

    SeL4 is proof that microkernels are safe, efficient and scalable yet we are stuck with big honking Linux kernels in 2025. That said more and more drivers moving usermode anyway so it's a wash in the end.

  • Post Author
    mmooss
    Posted March 23, 2025 at 3:51 pm

    SeL4 is old news – not a criticism, but has anyone added another formally proven layer or component? (Edit: I mean new components beyond the microkernel, not improvements to the microkernel.)

    Also, I suspect some people – maybe some on HN :) – get emotional overload when they see the word 'proof' and their intellectual functions stop. It's not a panacea for the infinite problem of secure IT; it isn't a way to create or discover a perfect and flawless diamond of software. IIUC it means it's proven to meet specific requirements in specific conditions, and those requirements and conditions can be quite narrow; and it says nothing about other functions and conditions that are out of spec. Is that roughly correct?

    What does it mean in practical terms? What does a security professional see when they see 'formally proven software'?

    What are the specs that SeL4 meet (no, I haven't looked at the OP in a long time)? Isn't that the essential information here?

  • Post Author
    hannob
    Posted March 23, 2025 at 4:15 pm

    L4 was popular at my university (Karlsruhe). While I never really looked into it in any detail, it always appeared to me like a project that is primarily interested in testing some theoretical ideas, but not in building anything that would be practically useful.

    That was 20 years ago. As far as I can tell, this has not changed. (Quick googling tells me there appear to be some efforts to build an OS on it, but they all look more like proof of concepts, not like something with real-world use.)

Leave a comment

In the Shadows of Innovation”

© 2025 HackTech.info. All Rights Reserved.

Sign Up to Our Newsletter

Be the first to know the latest updates

Whoops, you're not connected to Mailchimp. You need to enter a valid Mailchimp API key.