4 ms·

> And for good enough software you should consider that maximum already for any number of users. I don't believe such software exists. (And, to be clear, I'm w

> And for good enough software you should consider that maximum already for any number of users. I don't believe such software exists. (And, to be clear, I'm writing from direct, day-job experience.) EDIT: I take it back. SQLite, cURL. Maybe. EDIT2: I can't reply to the SEL4 response, so here goes. I'm a huge fan of verification tools, but consider the Spectre class of bugs. Verification is always done wrt a mathematical model that you've defined after inspecting the world and writing down the properties you want to track. But the world changes, and the chance that the world changes increases with the number of users of your software. That's the nature of the beast.

chromoblob 3y ago
seL4 is a formally verified OS kernel. https://sel4.systems/About/ https://sel4.systems/About/
chromoblob 3y ago
Spectre is a bug in the processor, not in the software. I agree that when you're stuck with unfinalized buggy processors, adding mitigations in software is reasonable. But the processor could be finalized too. When I had a reply I couldn't reply to, I opened the reply separately in a new tab, and there I could reply to it, try this.
- cscheid 3y ago
  > Spectre is a bug in the processor, not in the software. It's a bug in the processor that causes a bug in the software. It's not a bug in your idealized mathematical model, but try telling that to the people who paid you not to leak private keys. I see my job as an engineer to be to create a product that satisfies the user's expectations (which in this case are eminently reasonable). It matters not one bit that I can point the finger to the chipmakers. I'm still selling something that I now learned doesn't do what I said it would. It's still on me to fix it the best I can. If I care about the product quality, that is.
  - chromoblob 3y ago
    The program must not show bugs when run on a hardware with unforeseeable bugs, you call this reasonable?
    - cscheid 3y ago
      And yet that's what every good engineer did when Spectre came out. Same with the Pentium fdiv bugs, and same with a host of microcode bugs that come up all the time. Not my business to decide what you think is reasonable. That's just what happens in the world, and what (in my view) good engineers sign up for.
      - chromoblob 3y ago
        The choice is between letting hardware be not finalized and letting that force software to be non-finalizable, and letting software be finalizable and forcing the hardware to be finalized too. I like latter more. Finalized hardware is better by itself as well.
        ChadNauseam 3y ago
        We would all like bug-free hardware, but we won't get it and our job is to write good software in the environment we were given
        chromoblob 3y ago
        > we won't get it Why do you think so?
        cscheid 3y ago
        > The choice What choice? I have to fix bugs today as they come.
    - thfuran 3y ago
      If you buy a car and the airbags randomly deploy, would you consider it reasonable for the manufacturer to respond "oh, yeah, that'll happen if you drive it on roads rougher than polished stainless steel. You should only be driving on polished roadways"?

chromoblob 3y ago

seL4 is a formally verified OS kernel. https://sel4.systems/About/ https://sel4.systems/About/

chromoblob 3y ago

Spectre is a bug in the processor, not in the software. I agree that when you're stuck with unfinalized buggy processors, adding mitigations in software is reasonable. But the processor could be finalized too. When I had a reply I couldn't reply to, I opened the reply separately in a new tab, and there I could reply to it, try this.

cscheid 3y ago
> Spectre is a bug in the processor, not in the software. It's a bug in the processor that causes a bug in the software. It's not a bug in your idealized mathematical model, but try telling that to the people who paid you not to leak private keys. I see my job as an engineer to be to create a product that satisfies the user's expectations (which in this case are eminently reasonable). It matters not one bit that I can point the finger to the chipmakers. I'm still selling something that I now learned doesn't do what I said it would. It's still on me to fix it the best I can. If I care about the product quality, that is.
- chromoblob 3y ago
  The program must not show bugs when run on a hardware with unforeseeable bugs, you call this reasonable?
  - cscheid 3y ago
    And yet that's what every good engineer did when Spectre came out. Same with the Pentium fdiv bugs, and same with a host of microcode bugs that come up all the time. Not my business to decide what you think is reasonable. That's just what happens in the world, and what (in my view) good engineers sign up for.
    - chromoblob 3y ago
      The choice is between letting hardware be not finalized and letting that force software to be non-finalizable, and letting software be finalizable and forcing the hardware to be finalized too. I like latter more. Finalized hardware is better by itself as well.
      - ChadNauseam 3y ago
        We would all like bug-free hardware, but we won't get it and our job is to write good software in the environment we were given
        chromoblob 3y ago
        > we won't get it Why do you think so?
      - cscheid 3y ago
        > The choice What choice? I have to fix bugs today as they come.
  - thfuran 3y ago
    If you buy a car and the airbags randomly deploy, would you consider it reasonable for the manufacturer to respond "oh, yeah, that'll happen if you drive it on roads rougher than polished stainless steel. You should only be driving on polished roadways"?