4 ms·
The federal government sucks, but this particular decision is not the government's fault. CSIRO had more than enough money to keep the seL4 team: to a large ext
by saithound 5y ago
The federal government sucks, but this particular decision is not the government's fault. CSIRO had more than enough money to keep the seL4 team: to a large extent, they paid for themselves by bringing in their own industry contracts. But even if they didn't, CSIRO just got a lot of funding for AI and cybersecurity.
Dismantling the seL4 team is the result of two things: simple lack of vision from CSIRO leadership (who seem to think that cybersecurity and formal verification don't have much overlap), and the long-standing one-upmanship and antagonism between the fields of AI and formal methods.
- roenxi 5y agoThe formal method community made a huge mistake using 'proof' as a part of their branding. The SeL4 FAQ has this gem [0]: > Is seL4 proved secure? > This depends on what you mean by secure. [answer continues...] The leadership team would need to be truly inspired to take that sort of thing seriously. It sounds like madness. [0] https://docs.sel4.systems/projects/sel4/frequently-asked-questions.html https://docs.sel4.systems/projects/sel4/frequently-asked-que...
- saithound 5y ago[answer continues] as you noted, so let's continue that answer: "In the interpretation of classic operating system security, the answer is yes. In particular, seL4 has been proved to enforce specific security properties, namely integrity and confidentiality, under certain assumptions."
- CalChris 5y agoSecurity claims will always depend on a threat model. The question doesn't provide a threat model. So the answer's proviso is appropriate.
- GregarianChild 5y agoThe SeL4 FAQ has this gem I'm struggling to say what's wrong with that claim from a scientific POV. As others also point out, security is conditional on various things, including, in this case, what you consider a valid flow of information and what you don't. For example if an OS allows user-mode to read AES-encrypted kernel-mode data then that would be insecure if you had an unrestricted attacker (who can brute-force AES) but secure assuming polynomial attackers (under standard hardness assumptions for AES). To add insult to injury, we don't in fact know if the standard hardness assumptions actually hold for AES.
- roenxi 5y agoIt is obviously correct from a scientific perspective. Scientific experts probably wrote it.
- GregarianChild 5y agoWhat else would you have used as branding?
- roenxi 5y ago"Guarantee certain properties about the software".