SeL4 – a formally verified, capability-based microkernel(sel4.systems)

5 pointsby wh3135 hours ago1 comment

ggm5 hours ago
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.
- sparkie4 hours ago
  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.
- defrost5 hours ago
  The swings and roundabouts of the Australian Utopia don't always favour capability based learnings.