4 ms·
I see four issues in its issue tracker with the "bug" label. Of these, one seems not to be reproducible on real hardware, one of them looks like a feature requ
by Jweb_Guru 4y ago
I see four issues in its issue tracker with the "bug" label. Of these, one seems not to be reproducible on real hardware, one of them looks like a feature request, one of them is a bug in deliberately non-verified code (therefore doesn't say anything about formal verification), and the remaining one involves a hardware-level timeout due to bootloader code taking too long. If you believe this is the error rate of any non formally verified software, that these are exploitable from a security perspective, or that these are indicative of some serious failure in the specification process, you have a very different understanding of software than I do. i.e., I would imagine when people talk about "software is only as good as its specification" they are imagining some dramatic flaw that undermines the guarantees of the system, rather than "I can't use the last 4 KiB in the address space."
- jcelerier 4y agoI mean, just look at the commits with "fix" in the specs folder: https://github.com/seL4/l4v/commits/master?after=4f0bbd4fcbc850ee00e2b111e861bdb79172c341+244&branch=master&path%5B%5D=spec&qualified_name=refs%2Fheads%2Fmaster https://github.com/seL4/l4v/commits/master?after=4f0bbd4fcbc...
- Jweb_Guru 4y agoNone of the "issues" in the first few pages look serious (most of them seem to be about portability to new architectures), so why don't we save some time and have you link to the specification bug you believe undermined the security guarantees of the system? So far you have only asserted such a bug exists.
- jcelerier 4y agoWhy are you talking about security guarantees? A bug is a bug, the point is to show that formal specifications don't prevent bugs. In some cases a warning text not showing up due to a bug or the wrong byte being sent to the serial port can have more severe consequences that any CVE-assignable issue.