3 ms·
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.
by isubasinghe 2y ago
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.
- vacuity 2y agoEven 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.
- deleted 2y ago[deleted]
- ryao 2y agoThis 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?
- isubasinghe 2y agoThere 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.
- ryao 2y agoHow does “This issue was present in the specification against which seL4 was verified” not imply yes to that question?