SeL4 – a formally verified, capability-based microkernel(sel4.systems)
sel4.systems
SeL4 – a formally verified, capability-based microkernel
https://sel4.systems/
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 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.
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...
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...
The swings and roundabouts of the Australian Utopia don't always favour capability based learnings.