6 ms·

Yes. Looks like it's back to the 1960s, 70s, 80s, ... You found a parser that you've formally verified won't break. Great, I've heard that before. The far bigg

Yes. Looks like it's back to the 1960s, 70s, 80s, ... You found a parser that you've formally verified won't break. Great, I've heard that before. The far bigger part of the problem is the spec - writing a formal spec is (for practical purposes) a similar process to writing a program, and similarly bug-prone. It's nice to have a clearly defined spec language, but that doesn't stop bugs/fault/problems and (by Gödel) can't stop a determined fool (fools are just too ingenious)!

Jweb_Guru 4y ago
Okay, so go break it, since it's so easy :) People routinely say that "a formally verified program is only as good as its specification!" but many fewer people actually go on to demonstrate that they can break said programs, assuming that this is simply "a matter of engineering" which is not in fact the case. I'm also not sure what Gödel has to do with any of this, as most specification languages are not Turing-complete (unless this is some oblique statement about the metalogic in which case... again, show me your proof of false :)).
- jcelerier 4y ago
  SEL4 is formally verified and still has bugs
  - 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 ago
      I 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 ago
        None 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 ago
        Why 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.
- seoaeu 4y ago
  Nobody said it was easy. If you think verification reduces bugs, then surely you can find a bug in Linux’s unverified TCP parsing?
  - Jweb_Guru 4y ago
    Many people have found bugs in unverified parsing routines in the Linux kernel. All I'm asking is for someone to find a single one in one of Microsoft's new parsers. Surely, if specification bugs are just as commonplace as other kinds of programming issues, this shouldn't be too big of a request. I'm mostly just tired of people pretending that formal verification produces buggy software at a rate that is in any way comparable to "ordinary" programming. Empirically, it doesn't, and people who claim it does have scant evidence to back up those claims. Are there specification bugs? Sure. Do they happen at the same rate that bugs in comparable unverified code (let alone C code) occur? Not even close.
    - deleted 4y ago
      [deleted]
    - seoaeu 4y ago
      Yeah, but you haven’t found bugs in the Linux kernel’s TCP parser. Your argument basically boils down to “X is true. If you think I’m wrong, then prove it by <extremely difficult task>” (It turns out that verification does reduce bugs, but the refusal of folks here to audit parsers doesn’t prove anything either way)

Jweb_Guru 4y ago

Okay, so go break it, since it's so easy :) People routinely say that "a formally verified program is only as good as its specification!" but many fewer people actually go on to demonstrate that they can break said programs, assuming that this is simply "a matter of engineering" which is not in fact the case. I'm also not sure what Gödel has to do with any of this, as most specification languages are not Turing-complete (unless this is some oblique statement about the metalogic in which case... again, show me your proof of false :)).

jcelerier 4y ago
SEL4 is formally verified and still has bugs
- 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 ago
    I 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 ago
      None 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 ago
        Why 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.
seoaeu 4y ago
Nobody said it was easy. If you think verification reduces bugs, then surely you can find a bug in Linux’s unverified TCP parsing?
- Jweb_Guru 4y ago
  Many people have found bugs in unverified parsing routines in the Linux kernel. All I'm asking is for someone to find a single one in one of Microsoft's new parsers. Surely, if specification bugs are just as commonplace as other kinds of programming issues, this shouldn't be too big of a request. I'm mostly just tired of people pretending that formal verification produces buggy software at a rate that is in any way comparable to "ordinary" programming. Empirically, it doesn't, and people who claim it does have scant evidence to back up those claims. Are there specification bugs? Sure. Do they happen at the same rate that bugs in comparable unverified code (let alone C code) occur? Not even close.
  - deleted 4y ago
    [deleted]
  - seoaeu 4y ago
    Yeah, but you haven’t found bugs in the Linux kernel’s TCP parser. Your argument basically boils down to “X is true. If you think I’m wrong, then prove it by <extremely difficult task>” (It turns out that verification does reduce bugs, but the refusal of folks here to audit parsers doesn’t prove anything either way)