Gernot Heiser

The recordings of all presentations from this month's #seL4 Summit are up: sel4.systems/news/2025.ht...

Schedule | LF Events Please note: This schedule is automatically displayed in Central European Summer Time (CEST / UTC+2). To see the schedule in your preferred timezone, please select from the drop-down menu to the right...

Regrettably I didn’t take a picture, but one of the coolest talks at the #seL4 Summit was Alexander Böttcher: “Sculpt OS – a dynamic, general-purpose OS powered by Genode on seL4”. It was presented on a laptop running Sculpt OS!
events.linuxfoundation.org/sel4-summit/...

#seL4 for secure voice communication for aircraft: Peter de Ridder from MEP at the seL4 Summit

Again Kaegi at the #seL4 Summit reports on progress on verifying an IPv6 attack with a bunch of undergraduate students

Side Agrawal from UBC discusses evaluating isolation mechanisms at the #seL4 Summit

#seL4 Foundation CEO June Andronick's update reveals that we'll be moving to a new structure, based in Switzerland! Members will no longer have to pay for Linux Foundation membership

Day 2 of the seL4 Summit kicks off with an industry panel discussing making a business case for a verified kernel

Yayan Shen from NIO talks at the #seL4 Summit about fault tolerant designs. Also, after launching their seL4-based OS in their new entry- level brand, it now runs in NIO-branded premium EVs

Gerwin at the #seL4 Summit talking about making the verification generic, so on new platforms the kernel can be verified quickly

Recordings will be published within a week or so

The #seL4 Summit is underway in Prague!
John Hatcliff from Kansas State kicks off with a keynote on model- based system development on seL4, as used in various DARPA projects

And this is how it looks inside, running seL4, Microkit, LionsOS, native device drivers and reusing an unmodified Linux display driver

The humble TS Kitty has just returned from its third overseas trip, having now had gigs in four continents

TS celebrating seL4 Day

Today is the 16th anniversary of the completion of se4’s proof of implementation correctness, and the 11th anniversary of seL4 being open-sourced.
Happy #seL4 Day from all at Trustworthy Systems!

The recording of my CASA/MPI-SP Distinguished Lecture is now available – thanks for hosting me!

casa.rub.de/veranstaltun...

Very pleased that UNSW is sponsoring this year’s #seL4 Summit again: sel4.systems/news/#sponso...

Got an invite for “Blockchain-Powered Machine Learning”. Certainly highly buzzword compliant, although I’m disappointed they couldn’t fit in quantum computing…

CASA Distinguished Lecture mit Gernot Heiser (USNW Sydney) Das Thema ist "It´s time for truly secure operating systems".

Looking forward to giving this CASA Distinguished Lecture this Tuesday: "It´s time for truly secure operating systems”.

hgi.rub.de/news/newsarc...

My first paper at a systems conference was at ATC'99.
My first paper award was at ATC'05...

RIP Usenix ATC – I’ve got many fond memories of you

www.usenix.org/blog/usenix-...

Great to see Collins Aerospace sponsoring the #seL4 Summit again: sel4.systems/news/#summit...

Benchmarking Crimes Meet Formal Verification

There are multiple instances of authors comparing verification efforts of systems projects by looking at the ratio of proof to code size. I demonstrate why this is nonsense and constitutes a benchmarking crime.

so, remind me again: why would I want to use these “AI” tools?

Why can’t my Mac share a wifi connection as a wifi hotspot, when my Samsung phone has no problem doing this?

I hope to find some time to look at this in detail...

Giving a joint keynote at ASPLOS+EuroSys was an honour but also 😁
After all, I was talking about LionsOS

Release 0.3.0 · au-ts/lionsos Release notes are available here.

LionsOS v0.3.0 is released! github.com/au-ts/lionso...
This is on the back of sDDF (#seL4 driver framework) 0.6.0 and Microkit 2.0.1

The seL4 whitepaper is trending on HN: news.ycombinator.com/item?id=4345...

Time for the Coalition to end the nuclear (con)fusion. (3/3)

Mr O’Brien further walked back from nuclear in parliament: “No-one on the side of the House, including me, is suggesting that nuclear technology—even small nuclear reactors—is an absolute certainty for this country” (Hansard) tedobrien.com.au/nuclear-ener... (2/3)