Hacker News Reader

I believe only certain versions and on certain architectures is seL4 verified for. There are no bugs found at the C source code level for these builds of seL4.

View on HN

This issue appears to have affected all architectures. This issue was present in the specification against which seL4 was verified. You can say that there are no bugs by virtue of it following the specification, but if the specification was wrong and in this case it was, then were there really no bugs?

There is always a specification, the question is "was this issue found against a version of seL4 that had been fully specified or not?".

I worked at the lab, I wasn't aware of any bug/issue on the fully specified kernel, that is why I am unsure if this counts or not.

I would need to have a look at the source code and proofs to confirm.

How does “This issue was present in the specification against which seL4 was verified” not imply yes to that question?

Even if it's not exactly seL4, there's good value in taking inspiration for design elements. It would still be a lot more robust than commodity operating systems.

Reply on news.ycombinator.com