3 ms·

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 n

by ryao 2y ago

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?

isubasinghe 2y ago
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.
- ryao 2y ago
  How does “This issue was present in the specification against which seL4 was verified” not imply yes to that question?