SeL4 – a formally verified, capability-based microkernel

sel4.systems

6 points·wh313··4 comments

It is my belief one of the classic footgun moments for the Australian science/industry body the CSIRO was defunding and deprioritising work on SEL in favour of formal methods applied to block chain. Yes, an analysis of etherium contracts was interesting and topical but not at the cost of remaining a committed partner securing operating systems.

The swings and roundabouts of the Australian Utopia don't always favour capability based learnings.

The silly thing is that your "blockchain" could be the smartest thing in the world, have super incredible cryptography or whatever. You can have the smartest developers in the world writing the software without bugs.

But you run that software on a mainstream operating system (Linux/Windows), your funds are not safu - they're just one confused deputy away from being stolen.

Having a secure by design operating system is a fundamental requirement for "blockchain" to ever become more than an online casino.

Online payments through centralized entities don't have this problem. If you get hacked, someone can revert the payment. If you get hacked and the private keys for your smart contract are stolen, there's nobody who can just roll it back for you.

The OS is the weakest link - a side-channel that will bypass any and all clever cryptocurrency designs.

The full-story is insane[0].

It is good that seL4 is now its own organization, fully independent. A tragedy that it was hampered by CSIRO for so many years.

0. https://microkerneldude.org/2022/02/17/a-story-of-betrayal-c...

Reply on news.ycombinator.com