It's 2021, when will we finally have formally verified kernels and drivers (or at the very least privileged stuff that isn't written in memory unsafe languages aaaaaa)
Conversation
Me: programming languages need to adopt capability security to pave way for a future where we're better at respecting our users' privacy and security
Me, remembering that we haven't even moved away from unproven memory unsafe languages in privileged applications:
2
1
7
At the very least Fuchsia seems to be moving in that direction and Google has shipped it to one device. There's still hope for the future...
But Fuchsia is written in a memory unsafe language and does not have a formal proof afaik :(
1
3
Replying to
Makes me even more mad that the Australian government cut funding for the team making seL4 - so incredibly short sighted, it breaks my heat. 😭
Quote Tweet
Word is out, and unfortunately true: @CSIRO's @Data61news dismantles Trustworthy Systems (TS), the team that shook the scientific world with the first correctness proof of an OS, #seL4. TS staff to reallocate to AI projects or sacked 1/6
Show this thread