CSIRO's Data61 Dismantles SeL4 Team | Hacker News Reader

CSIRO's Data61 Dismantles SeL4 Team

twitter.com

130 pointszekrioca46 comments

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)

> 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.

>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.

This is not true. [https://www.opensecrets.org/orgs/microsoft-corp/summary?id=D...]

I should've clarified, I was meaning in the context of Australian politics. A lot of Australian tech companies actually ban political donations as part of their anti-bribery and corruption policies.

If you look at donation data from the Australian Electoral Commission, there are no donations from tech companies [1]. The majority of donations are from banks, property developers, and mining companies.

[1] http://democracyforsale.net/search-aec/

Sounds scaringly similar to the ludicrous mass redundancies imposed on the pure mathematics department at the University of Leicester, in order to create funds for AI.

And pray tell on what foundations the field of machine learning and AI is built on? https://www.reddit.com/r/math/comments/nf5r5o/the_pure_math_...

I find the blind show-me-the-money approach to funding research is baffling, in light of evidence about how research in fields/subjects such as neural networks[1] and mRNA[2] that fell out of favour for many years were eventually proven to be valid and of tremendous use.

[1] https://en.wikipedia.org/wiki/AI_winter

[2] https://en.wikipedia.org/wiki/Katalin_Karik%C3%B3#Career

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

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.

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.

It used to be ~30-40 people AFAIK. But you're right, the government would not have said "axe this team". The government would have likely said "focus on AI research, and get rid of any team that does not align with it." Same outcome though, and same source of the decision.

Data61 was mostly gutted over the last few years anyway, the slide downhill started when it changed from NICTA. The politicians hate the idea of long term research funding, so they had the idea it would be self sustaining, but big Australian corporations spend nothing on external research, lowest in the OECD, and foreign corps don't reinvest in research overseas.

Also, I remember Hugh Durrant-Whyte (robotics/SLAM pioneer, ACFR, former NICTA CEO) telling us that CSIRO culture would overwhelm Data61. So no surprise.

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).

CSIRO was allocated an additional $459m over the next 4 years last October.

Only to make up for lost funding due to economic downturn from covid19 https://www.innovationaus.com/csiro-gets-a-459m-budget-lifel...

Ah, I see the Aus gov plays similar numbers games to the UK gov.

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.

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-que...

[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."

Security claims will always depend on a threat model. The question doesn't provide a threat model. So the answer's proviso is appropriate.

    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.

It is obviously correct from a scientific perspective. Scientific experts probably wrote it.

What else would you have used as branding?

"Guarantee certain properties about the software".

For anybody wondering what seL4 is, here's the whitepaper[0].

[0]: https://sel4.systems/About/seL4-whitepaper.pdf

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

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

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?

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).

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/

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

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.

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/...

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.

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.

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)

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).

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.

Can you be specific? Who are these young researchers with new controversial ideas who are harmed by L4?

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.

It's hard to know how common this is. But I have personally witnessed the L4 top folks talking down someones novel contributions as "this is nothing knew, you should have used L4, we did this stuff 10 years ago" and making a young researcher feel miserable.

(IIRC the very same people also published a paper introducing the same novel idea in L4 some months later, but that's another discussion)

Cell phone baseband and virtualization supervisor hosts are the only niches where L4 gained any traction. Considering the lack of publicly available information about baseband operating environments, those could actually be the same niche (ie, L4 is acting as a hypervisor for the baseband).

Hurd-on-L4 was a flop. Fuscha went a completely different direction with dissimilar communication primitives.

From the outside, L4 looks like a perfect example of a line of academic research that has no industrial relevance.

I think some people from industry would disagree. Certainly L4 has found use cases mostly in the field of embedded systems, but I wouldn't call this a niche (or at least it's a pretty big one).

Companies like Hensoldt Cyber (https://hensoldt-cyber.com - Gernot Heiser is involved in this) but also SYSGO with PikeOS (an independently developed L4-family microkernel - https://www.sysgo.com), Kernkonzept (https://www.kernkonzept.com) or Genode Labs (https://genode.org) have successfully used and deployed L4-based systems with many customers from industry. Yes, this is again very much focused on Germany, but that's also where a lot of the research was done.

Fuchsia at Google is probably a result of the "not-invented-here" syndrome that seems to be popular at Google. I haven't taken a closer look at the system but would certainly be interested in reading about the differences to an L4-based microkernel.

And Hurd-on-L4 is certainly coming next year ;-) (or a bit later, due to Corona or so...).

Other active seL4 users include Real-Time Innovations (autonomous systems), Cog Systems (connected devices), Raytheon (defense/aerospace), DornerWorks (IoT/medical), Ghost (self-driving cars), Penten (communications securty).

Oh yes: https://xkcd.com/1508/

There is also Cyberus Technology which develops Hedron, yet another L4-based microkernel and ships that as part of a secure workstation targeted at the german government market.

There’s quite a community that has taken the research to successful industry applications over here in Dresden, Germany. :-)

If you’re interested in some of the stories behind the technology I can recommend the Syslog Podcast at https://syslog.show

I think seL4 is orthogonal to the team's core achievements which are in verification of low-level code. Those technologies transfer to other settings.

Reply on news.ycombinator.com