3 ms·
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
by im_down_w_otp 7y ago
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.
- mmrezaie 7y ago> 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.
- im_down_w_otp 7y agoWe 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.
- repolfx 7y agoWhat sort of mistakes were easy to make?
- anp 7y agoWas this work a part of the post's unnamed self-driving car company project?
- im_down_w_otp 7y agoNope. 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.