9 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 1y 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 1y 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 1y ago[deleted]
- ryao 1y 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 1y 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 1y agoHow does “This issue was present in the specification against which seL4 was verified” not imply yes to that question?