6 ms·

CSIRO's Data61 Dismantles SeL4 Team

130 points by zekrioca 5y ago

stephen_g 5y ago
I assume this must be related to our Government’s continuing starving of CSIRO of funding? It’s really sad to see, they’re doing it to our universities too - in that case, the Universities were massively hit from international students not able to come in due to COVID, but the Government specifically excluded Unis from the main income support program designed to keep business, industry and education solvent for no reason (apart from their political ideology).
- toomanybeersies 5y ago
  CSIRO was allocated an additional $459m over the next 4 years last October.
  - tmn007 5y ago
    Only to make up for lost funding due to economic downturn from covid19 https://www.innovationaus.com/csiro-gets-a-459m-budget-lifeline-for-science/ https://www.innovationaus.com/csiro-gets-a-459m-budget-lifel...
    - stuaxo 5y ago
      Ah, I see the Aus gov plays similar numbers games to the UK gov.
- 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 ago
    The 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 ago
      Security 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 ago
      The 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 ago
        It is obviously correct from a scientific perspective. Scientific experts probably wrote it.
h0l0cube 5y ago
Anyone here had any exposure to SeL4 or it's concepts? Is it being used in the wild, or has it influenced anything else of real import?
- saithound 5y ago
  I don't know if it influenced anything else (probably not, as it dominates its niche, and there aren't many other verified kernel projects), but it's definitely used in the wild. German sensor company Hensoldt ships seL4 in ROM on some of their embedded boards. Other users are Real-Time Innovations (autonomous systems), Cog Systems (connected devices), Raytheon (defense/aerospace), DornerWorks (IoT/medical), Ghost (self-driving cars), Penten (communications security).
- angry_octet 5y ago
  Fortunately it has significant interest in the US. COVID has put a bit of a kink in collaboration but it wouldn't surprise me to see the team working for US R&D labs. https://www.sel4-us.org/summits/2020-summit/ https://www.sel4-us.org/summits/2020-summit/
zibzab 5y ago
I think this is good for everyone. This team and associated groups around the world (a famous researcher once called it "the German army") have been receiving a lot of grants, been too dominant in conferences and to be honest have not done much practical work for some time. (If you think sel4 is extremely useful in practical applications, go ahead and try it yourself. Port an existing project to use sel4 and see how well it works)
- johndoe0815 5y ago
  L4 shows that not only US-based researchers can do great systems research - and this is a very good think IMHO. Billions of iOS devices use L4 (though net seL4 AFAIK) as the OS for their security processor and there are numerous other embedded use cases. The 30 years of efforts by Jochen Liedtke at GMD/Karlsruhe, Hermann Härtig at TU Dresden and Gernot Heiser at UNSW (and the countless students and postdocs) have significantly advanced the field of microkernel research and OS research in general. Microkernels were a dead field of research after Mach etc. didn't live up to their expectations, only to be revived by Liedtke's work. It is extremely confusing that you think a successful team publishing great papers and receiving significant research founding is "too dominant" (and the anti-German tone of the "army" comment is certainly inappropriate).
  - zibzab 5y ago
    Let me explain my comment: For a while it was really hard to do something in the OS, security or embedded system field of it didn't align with the L4 way of doing things. This harmed progress, and in particular young researchers with new controversial ideas.
    - saithound 5y ago
      Can you be specific? Who are these young researchers with new controversial ideas who are harmed by L4?
    - johndoe0815 5y ago
      I know the German OS research landscape pretty well and I can assure you that there were a large number of successful systems projects and good PhD theses which were not in any way related to L4. Of course, the groups for which L4 was fundamental (such as Hermann Härtig's TU Dresden group) had a natural focus on L4. But there is a lot of internationally renowned research in OS going on in Germany, I will only mention two examples, Wolfgang Schröder-Preikschat's group at FAU Erlangen and Frank Bellosa's group at KIT. But I would certainly love to discuss your view of the research landscape further - for me, it is always interesting to get to know different views and insights. So if you are interested to talk about this, feel free to contact me directly.
Smerity 5y ago
The state of Australia's national science initiatives and the projects they support have always been of concern to me. There are bright spots but they seem overwhelmingly destined to be extinguished or flee. That the team members can only decide between AI projects or being sacked is insane. And that's coming from someone in the damn field of AI. If Australia decided to hard core focus and "go all in" on AI then _maybe_ you could (very poorly) justify bleeding dry all other fields of innovation - but the recent Australian budget threw $124 million AUD vaguely at "AI" and called it a day. That's only $96 million USD and represents 3-4 large AI startup raises of capital but over more years and with usage limited by red tape and bureaucracy. The saddest thing re: "AI or sack" is that I could list many promising AI projects from the CSIRO's NICTA (precursor to Data61) about a decade or so ago that had their support slowly strangled just like seL4. Some of those projects survived regardless and many went on to be central figures in the now hyped AI field - except they had to move overseas ... Australia's national science initiatives seem to have neither the capital outlay / flexibility to compete with startup / commercial R&D for chasing hype nor the attention to fund and champion the projects that might build the promising scientific advances of tomorrow. If you only swim at the wave when you see it appear you'll always be behind ... (echoing content from my tweet: https://twitter.com/Smerity/status/1395694815291985921 https://twitter.com/Smerity/status/1395694815291985921)
- deleted 5y ago
  [deleted]
- toomanybeersies 5y ago
  > The state of Australia's national science initiatives and the projects they support have always been of concern to me That's because technology companies generally don't make political donations or engage in lobbying, unlike the banking, gambling, and mining industries, and trade unions.
  - mrslave 5y ago
    >technology companies generally don't make political donations or engage in lobbying I'm pretty sure they do, but their primary concerns are getting their piece of the foreign worker visa pie, resisting further industry regulation, and corporate tax. It is definitely not supporting local universities in either the quality of their undergraduate programs or post-grad research.
zekrioca 5y ago
The news snippet: https://www.innovationaus.com/data61-dumps-world-class-sel4-security-team/ https://www.innovationaus.com/data61-dumps-world-class-sel4-...
stuaxo 5y ago
Some big tech firms really should use some of their stacks of cash to fund the sel4foundation.
fmajid 5y ago
Seems short-sighted. Diverting that funding to overhyped AI is insult on top of injury.
legostormtroopr 5y ago
Does Data61 have a track record of successful projects? Have they been able to successfully fund a single project that returned a positive return on investment? Not say all research must be commercialisable, but at least some of it should be.
- senbarryobama 5y ago
  Audinate made audio over ethernet Apple-like.
- EarthMephit 5y ago
  Yes, they developed the first WLAN chip. Their Wifi patent alone brought in $430 million dollars: https://www.ipaustralia.gov.au/tools-resources/case-studies/csiro-wlan-patent https://www.ipaustralia.gov.au/tools-resources/case-studies/...
  - legostormtroopr 5y ago
    That was the CSIRO (and boy don’t they love to tell people they invented wifi). I asked about Data61, given that they are meant to bridge research and industry through commercialisation, I’ve yet to hear of an actual profitable success story from them.
    - saithound 5y ago
      Hivery (AI for retailing) came from Data61 and has raised a massive amount of money, and Propeller Aero (drone surveying) is profitable. Not sure if seL4 and Audinate count (they started out as NICTA projects, before Data61), but they are both commercially viable.
kragen 5y ago
https://nitter.dark.fail/GernotHeiser/status/1395517697689931780 https://nitter.dark.fail/GernotHeiser/status/139551769768993... > 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 TS was exemplary in @CSIRO's @Data61news: from world-leading fundamental research to real-world deployment. It had a strong culture of excellence that aimed high and shunned incremental work, #seL4 a prime example. @sel4Foundation 2/6 Claims by @CSIRO's @Data61news of research excellence sound hollow. I challenge you to identify work in Data61 eclipsing the TS team and #seL4. Yet it's easy to identify highly incremental work in Data61 that seems safe 3/6 And it's not that TS rested on its laurels: Time Protection, systematic prevention of information leakage through timing channels - in the too-hard basket for most. This has just won its third Best Paper Award, at @DateConference'21 4/6 This would be a desaster for #seL4, had we not set up the seL4 Foundation to minimise dependency on @CSIRO's @Data61news. Please help us strengthening @seL4Foundation, to bring real #security to the world's computing systems 5/6 TS's work will continue @UNSW, in close collaboration with @lsf37 and colleagues at #ProofCraft and our ecosystem partners in @seL4Foundation. Together we will continue to define the state of the art in OS #security 6/6
- danerd 5y ago
  Honestly, this is a disgrace for Australia! Given what I heard about Data61, this decision must've been coming from the government. No sane research leader would dismantle such an outstanding team, or force them to change direction.
  - saithound 5y ago
    I don't know what you heard about Data61, but as bad as the federal government is, they don't go around micro-managing ~10-person research groups of CSIRO business units. This is entirely on the current Data61 leadership. There's nothing more to it.
    - danerd 5y ago
snvzz 5y ago
For anybody wondering what seL4 is, here's the whitepaper[0]. [0]: https://sel4.systems/About/seL4-whitepaper.pdf https://sel4.systems/About/seL4-whitepaper.pdf
deleted 5y ago
[deleted]

130 points by zekrioca 5y ago

I assume this must be related to our Government’s continuing starving of CSIRO of funding? It’s really sad to see, they’re doing it to our universities too - in that case, the Universities were massively hit from international students not able to come in due to COVID, but the Government specifically excluded Unis from the main income support program designed to keep business, industry and education solvent for no reason (apart from their political ideology).

toomanybeersies 5y ago
CSIRO was allocated an additional $459m over the next 4 years last October.
- tmn007 5y ago
  Only to make up for lost funding due to economic downturn from covid19 https://www.innovationaus.com/csiro-gets-a-459m-budget-lifeline-for-science/ https://www.innovationaus.com/csiro-gets-a-459m-budget-lifel...
  - stuaxo 5y ago
    Ah, I see the Aus gov plays similar numbers games to the UK gov.
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 ago
  The 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 ago
    Security 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 ago
    The 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 ago
      It is obviously correct from a scientific perspective. Scientific experts probably wrote it.

h0l0cube 5y ago

Anyone here had any exposure to SeL4 or it's concepts? Is it being used in the wild, or has it influenced anything else of real import?

saithound 5y ago
I don't know if it influenced anything else (probably not, as it dominates its niche, and there aren't many other verified kernel projects), but it's definitely used in the wild. German sensor company Hensoldt ships seL4 in ROM on some of their embedded boards. Other users are Real-Time Innovations (autonomous systems), Cog Systems (connected devices), Raytheon (defense/aerospace), DornerWorks (IoT/medical), Ghost (self-driving cars), Penten (communications security).
angry_octet 5y ago
Fortunately it has significant interest in the US. COVID has put a bit of a kink in collaboration but it wouldn't surprise me to see the team working for US R&D labs. https://www.sel4-us.org/summits/2020-summit/ https://www.sel4-us.org/summits/2020-summit/

zibzab 5y ago

I think this is good for everyone. This team and associated groups around the world (a famous researcher once called it "the German army") have been receiving a lot of grants, been too dominant in conferences and to be honest have not done much practical work for some time. (If you think sel4 is extremely useful in practical applications, go ahead and try it yourself. Port an existing project to use sel4 and see how well it works)

johndoe0815 5y ago
L4 shows that not only US-based researchers can do great systems research - and this is a very good think IMHO. Billions of iOS devices use L4 (though net seL4 AFAIK) as the OS for their security processor and there are numerous other embedded use cases. The 30 years of efforts by Jochen Liedtke at GMD/Karlsruhe, Hermann Härtig at TU Dresden and Gernot Heiser at UNSW (and the countless students and postdocs) have significantly advanced the field of microkernel research and OS research in general. Microkernels were a dead field of research after Mach etc. didn't live up to their expectations, only to be revived by Liedtke's work. It is extremely confusing that you think a successful team publishing great papers and receiving significant research founding is "too dominant" (and the anti-German tone of the "army" comment is certainly inappropriate).
- zibzab 5y ago
  Let me explain my comment: For a while it was really hard to do something in the OS, security or embedded system field of it didn't align with the L4 way of doing things. This harmed progress, and in particular young researchers with new controversial ideas.
  - saithound 5y ago
    Can you be specific? Who are these young researchers with new controversial ideas who are harmed by L4?
  - johndoe0815 5y ago
    I know the German OS research landscape pretty well and I can assure you that there were a large number of successful systems projects and good PhD theses which were not in any way related to L4. Of course, the groups for which L4 was fundamental (such as Hermann Härtig's TU Dresden group) had a natural focus on L4. But there is a lot of internationally renowned research in OS going on in Germany, I will only mention two examples, Wolfgang Schröder-Preikschat's group at FAU Erlangen and Frank Bellosa's group at KIT. But I would certainly love to discuss your view of the research landscape further - for me, it is always interesting to get to know different views and insights. So if you are interested to talk about this, feel free to contact me directly.

Smerity 5y ago

The state of Australia's national science initiatives and the projects they support have always been of concern to me. There are bright spots but they seem overwhelmingly destined to be extinguished or flee. That the team members can only decide between AI projects or being sacked is insane. And that's coming from someone in the damn field of AI. If Australia decided to hard core focus and "go all in" on AI then _maybe_ you could (very poorly) justify bleeding dry all other fields of innovation - but the recent Australian budget threw $124 million AUD vaguely at "AI" and called it a day. That's only $96 million USD and represents 3-4 large AI startup raises of capital but over more years and with usage limited by red tape and bureaucracy. The saddest thing re: "AI or sack" is that I could list many promising AI projects from the CSIRO's NICTA (precursor to Data61) about a decade or so ago that had their support slowly strangled just like seL4. Some of those projects survived regardless and many went on to be central figures in the now hyped AI field - except they had to move overseas ... Australia's national science initiatives seem to have neither the capital outlay / flexibility to compete with startup / commercial R&D for chasing hype nor the attention to fund and champion the projects that might build the promising scientific advances of tomorrow. If you only swim at the wave when you see it appear you'll always be behind ... (echoing content from my tweet: https://twitter.com/Smerity/status/1395694815291985921 https://twitter.com/Smerity/status/1395694815291985921)

deleted 5y ago
[deleted]
toomanybeersies 5y ago
> The state of Australia's national science initiatives and the projects they support have always been of concern to me That's because technology companies generally don't make political donations or engage in lobbying, unlike the banking, gambling, and mining industries, and trade unions.
- mrslave 5y ago
  >technology companies generally don't make political donations or engage in lobbying I'm pretty sure they do, but their primary concerns are getting their piece of the foreign worker visa pie, resisting further industry regulation, and corporate tax. It is definitely not supporting local universities in either the quality of their undergraduate programs or post-grad research.

zekrioca 5y ago

The news snippet: https://www.innovationaus.com/data61-dumps-world-class-sel4-security-team/ https://www.innovationaus.com/data61-dumps-world-class-sel4-...

stuaxo 5y ago

Some big tech firms really should use some of their stacks of cash to fund the sel4foundation.

fmajid 5y ago

Seems short-sighted. Diverting that funding to overhyped AI is insult on top of injury.

legostormtroopr 5y ago

Does Data61 have a track record of successful projects? Have they been able to successfully fund a single project that returned a positive return on investment? Not say all research must be commercialisable, but at least some of it should be.

senbarryobama 5y ago
Audinate made audio over ethernet Apple-like.
EarthMephit 5y ago
Yes, they developed the first WLAN chip. Their Wifi patent alone brought in $430 million dollars: https://www.ipaustralia.gov.au/tools-resources/case-studies/csiro-wlan-patent https://www.ipaustralia.gov.au/tools-resources/case-studies/...
- legostormtroopr 5y ago
  That was the CSIRO (and boy don’t they love to tell people they invented wifi). I asked about Data61, given that they are meant to bridge research and industry through commercialisation, I’ve yet to hear of an actual profitable success story from them.
  - saithound 5y ago
    Hivery (AI for retailing) came from Data61 and has raised a massive amount of money, and Propeller Aero (drone surveying) is profitable. Not sure if seL4 and Audinate count (they started out as NICTA projects, before Data61), but they are both commercially viable.

kragen 5y ago

https://nitter.dark.fail/GernotHeiser/status/1395517697689931780 https://nitter.dark.fail/GernotHeiser/status/139551769768993... > 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 TS was exemplary in @CSIRO's @Data61news: from world-leading fundamental research to real-world deployment. It had a strong culture of excellence that aimed high and shunned incremental work, #seL4 a prime example. @sel4Foundation 2/6 Claims by @CSIRO's @Data61news of research excellence sound hollow. I challenge you to identify work in Data61 eclipsing the TS team and #seL4. Yet it's easy to identify highly incremental work in Data61 that seems safe 3/6 And it's not that TS rested on its laurels: Time Protection, systematic prevention of information leakage through timing channels - in the too-hard basket for most. This has just won its third Best Paper Award, at @DateConference'21 4/6 This would be a desaster for #seL4, had we not set up the seL4 Foundation to minimise dependency on @CSIRO's @Data61news. Please help us strengthening @seL4Foundation, to bring real #security to the world's computing systems 5/6 TS's work will continue @UNSW, in close collaboration with @lsf37 and colleagues at #ProofCraft and our ecosystem partners in @seL4Foundation. Together we will continue to define the state of the art in OS #security 6/6

danerd 5y ago
Honestly, this is a disgrace for Australia! Given what I heard about Data61, this decision must've been coming from the government. No sane research leader would dismantle such an outstanding team, or force them to change direction.
- saithound 5y ago
  I don't know what you heard about Data61, but as bad as the federal government is, they don't go around micro-managing ~10-person research groups of CSIRO business units. This is entirely on the current Data61 leadership. There's nothing more to it.
  - danerd 5y ago

snvzz 5y ago

For anybody wondering what seL4 is, here's the whitepaper[0]. [0]: https://sel4.systems/About/seL4-whitepaper.pdf https://sel4.systems/About/seL4-whitepaper.pdf

deleted 5y ago

[deleted]