5 ms·

As powerful as fuzzing is, this is a good reminder why it’s not a substitute for formal verification in high-integrity or critical systems.

er4hn 4y ago
I would argue the issue was not checking the coverage of new code vs what was being tested.
- naasking 4y ago
  The OP is pointing out that what "the issue" is depends on whether you want high confidence that your code has few bugs, or you want certainty that your code contains no bugs.
  - tsimionescu 4y ago
    > you want certainty that your code contains no bugs Well, everyone would want that, but it's not possible. Formal verification comes nowhere close to promising that, especially not on a large project. I'm pretty sure OpenSSL is larger than any formally verified software to date (perhaps CompCert is larger?).
    - mpweiher 4y ago
      "Beware of bugs in the above code; I have only proved it correct, not tried it." Donald Knuth
fulafel 4y ago
.. or more pragmatically, safer languages where errors aren't exploitable to get remote code execution. (I guess that semantics can also be seen as a formally verified property)
- marginalia_nu 4y ago
  Given log4shell happened in one of the more aggressively sandboxed languages with mainstream adoption, the outlook isn't great.
  - chowells 4y ago
    Sandboxing is mostly irrelevant to the log4j error. You'd have to tell the sandbox to turn off reflection, which isn't really feasible in Java. And that's because Java is so poorly designed that big libraries are all designed to use reflection to present an API they consider usable. Compare that to a language designed well enough that reflection isn't necessary for good APIs, for instance.
    - marginalia_nu 4y ago
      Dunno if I agree that libraries need reflection. Some do, but primarily in the dependency injection and testing space. That's not really where you'd expect RCE-problems.
      - chowells 4y ago
        Yeah, I should say where developers don't think they need to use reflection. Like, the log4j thing came from (among other design errors) choosing to use reflection to look up filters for processing data during logging. Why would log4j's developers possibly think reflection is an appropriate tool for making filters available? Because it's the easy option in Java. Because it's the easy option, people are already comfortable with it in other libraries. Because it's easy and comfortable, it's what gets done. Some languages make reflection much more difficult (or nearly impossible) and other APIs much easier. It's far more difficult to make that class of error in languages like that.
    - strbean 4y ago
      > big libraries are all designed to use reflection to present an API they consider usable. whistles in python
userbinator 4y ago
There's no replacement for intelligence. Turning the world into authoritarian dystopia in search of that replacement seems to be the popular thing to do, unfortunately.

er4hn 4y ago

I would argue the issue was not checking the coverage of new code vs what was being tested.

naasking 4y ago
The OP is pointing out that what "the issue" is depends on whether you want high confidence that your code has few bugs, or you want certainty that your code contains no bugs.
- tsimionescu 4y ago
  > you want certainty that your code contains no bugs Well, everyone would want that, but it's not possible. Formal verification comes nowhere close to promising that, especially not on a large project. I'm pretty sure OpenSSL is larger than any formally verified software to date (perhaps CompCert is larger?).
  - mpweiher 4y ago
    "Beware of bugs in the above code; I have only proved it correct, not tried it." Donald Knuth

fulafel 4y ago

.. or more pragmatically, safer languages where errors aren't exploitable to get remote code execution. (I guess that semantics can also be seen as a formally verified property)

marginalia_nu 4y ago
Given log4shell happened in one of the more aggressively sandboxed languages with mainstream adoption, the outlook isn't great.
- chowells 4y ago
  Sandboxing is mostly irrelevant to the log4j error. You'd have to tell the sandbox to turn off reflection, which isn't really feasible in Java. And that's because Java is so poorly designed that big libraries are all designed to use reflection to present an API they consider usable. Compare that to a language designed well enough that reflection isn't necessary for good APIs, for instance.
  - marginalia_nu 4y ago
    Dunno if I agree that libraries need reflection. Some do, but primarily in the dependency injection and testing space. That's not really where you'd expect RCE-problems.
    - chowells 4y ago
      Yeah, I should say where developers don't think they need to use reflection. Like, the log4j thing came from (among other design errors) choosing to use reflection to look up filters for processing data during logging. Why would log4j's developers possibly think reflection is an appropriate tool for making filters available? Because it's the easy option in Java. Because it's the easy option, people are already comfortable with it in other libraries. Because it's easy and comfortable, it's what gets done. Some languages make reflection much more difficult (or nearly impossible) and other APIs much easier. It's far more difficult to make that class of error in languages like that.
  - strbean 4y ago
    > big libraries are all designed to use reflection to present an API they consider usable. whistles in python

userbinator 4y ago

There's no replacement for intelligence. Turning the world into authoritarian dystopia in search of that replacement seems to be the popular thing to do, unfortunately.