10 Years SeL4: Still the Best, Still Getting Better

Re:10 Years SeL4: Still the Best, Still Getting Better by im_down_w_otp on Tuesday August 06, 2019 @04:15PM (#20629075)

We're using seL4 as the basis for one of our products which is focused on characterizing components, systems, and their failure modes. Mostly targeting critical "Cyber-Phyiscal Systems" and "Software-Intensive Systems of Systems".

We have a little operating system, or enough of one to facilitate building the rest of our product atop of it, that goes along with seL4. We'd planned to open source parts of it fairly soon, but prioritizing hiring a few more folks (BD, PM, Eng.) has put that effort on-hold temporarily.

Building things with seL4 is easy to do wrong, despite being given a variety of very low-level verified primitives to work with. You still need to put it all together just right. CAmkES is supposed to make this easier, but our experience with it wasn't very good, so we took the hard road and created a Rust-based application framework to go over the top of everything.

[ Parent | on HN ]

Re:10 Years SeL4: Still the Best, Still Getting Better by mmrezaie on Tuesday August 06, 2019 @04:25PM (#20629208)

> seL4 is easy to do wrong

This was our main stopper. seL4 would benefit greatly to teach how everything can be fit together, and where everything can be expected to go.

[ Parent | on HN ]

Re:10 Years SeL4: Still the Best, Still Getting Better by im_down_w_otp on Tuesday August 06, 2019 @04:36PM (#20629336)

We overcame this with a significant amount of Rust-i-ness and effort in understanding the guts of the kernel and how it implements its assurances.

Basically by providing setup, resource management, and communication abstractions that you just can't get wrong because doing something dumb that would be entirely nuts and/or would result in difficult to deal with run-time errors (as the kernel enforces some of its guarantees) ends up being rejected by the compiler ahead of time.

[ Parent | on HN ]

Re:10 Years SeL4: Still the Best, Still Getting Better by repolfx on Wednesday August 07, 2019 @09:25AM (#20634452)

What sort of mistakes were easy to make?

[ Parent | on HN ]

Re:10 Years SeL4: Still the Best, Still Getting Better by anp on Tuesday August 06, 2019 @04:58PM (#20629568)

Was this work a part of the post's unnamed self-driving car company project?

[ Parent | on HN ]

Re:10 Years SeL4: Still the Best, Still Getting Better by im_down_w_otp on Tuesday August 06, 2019 @05:12PM (#20629690)

Nope. Entirely different. Left prior place just over a year ago. Eventually started a new company and closed our Seed funding a few months ago.

We have some self-driving car customers, but that's just because they're gluing together really complicated systems from lots and lots of diverse components, so they're great use cases.

Our goal is much broader scoped beyond AV and is more akin to creating new classes of CAE tools for SISoS & CPS designers/engineers.

[ Parent | on HN ]