5 ms·

I suppose it would be nice to require at least 100% line coverage for tested encryption-related functionality, when tested by a fuzzer. Deviations from this cou

by _flux 3y ago

I suppose it would be nice to require at least 100% line coverage for tested encryption-related functionality, when tested by a fuzzer. Deviations from this could be easily detected in CI. Testing cannot be used to prove that a flaw doesn't exist, only that it does.

Retr0id 3y ago
> Testing cannot be used to prove that a flaw doesn't exist This is not universally true, formal methods can take you a long way, depending on the problem domain. And sometimes you can test for every possible input. This usually isn't feasible, but it's nice when it is.
- dllthomas 3y ago
  Formal methods aren't "testing". As you say, though, exhaustive testing is sometimes possible.
  - bluGill 3y ago
    It is normally safe to assume the exhaustive testing isn't possible because the total states to exhaustively tests exceeds the number of atoms in the universe. There are a few exceptions, but in general we should assume it is always impossible to exhaustively test programs. Which means we need to use something else to find what the limits are and test only those, or use formal methods (both would be my recommendation - though I'll admit I have yet to figure out how to use formal methods)
    - dllthomas 3y ago
      > in general we should assume it is always impossible to exhaustively test programs The whole program? Yes. For testing individual components, there's no need to assume. The answer is very likely either clearly yes (the input is a handful of booleans) or clearly no (the input is several integers or even unbounded) and for those cases where it's not immediately clear (one i16? Three u8s?) it's probably still not hard to think through for your particular case in your particular context.
      - mananaysiempre 3y ago
        Brute forcing a single 32-bit input has also been usefully performed in some cases, such as for single-precision implementations of special functions[1]. [1] https://randomascii.wordpress.com/2014/01/27/theres-only-four-billion-floatsso-test-them-all/ https://randomascii.wordpress.com/2014/01/27/theres-only-fou...
        bluGill 3y ago
        32 bits is a bit over 4 billion states, so that is doable. However a lot of algorithms can have more than 32 bits of states and so quickly get beyond what is doable.
        dllthomas 3y ago
        > 32 bits is a bit over 4 billion states, so that is doable. Whether 4B is doable depends on how much work you're doing for each of those states, but yes, "4B" alone certainly doesn't rule it out. There's also a question of whether it goes with your most frequently run tests or is something that's only run occasionally. > However a lot of algorithms can have more than 32 bits of states and so quickly get beyond what is doable. I'm pretty confident we're all in agreement there.
  - Retr0id 3y ago
    I agree that it's not testing in the strict sense, but fuzzing isn't really testing either. The work done by a a theorem prover and a fuzzer isn't all that different (and sufficiently advanced fuzzers use SMT solvers etc.)
    - NovemberWhiskey 3y ago
      This seems to neglect the fundamental difference between static and dynamic analysis. Formal methods approaches don’t usually need me to run my code.
    - _flux 3y ago
      I guess I need to disagree :). Why isn't fuzzing testing? Ultimately it ends up running the code and seeing if it works—for some definition of "working", that is, it doesn't crash—even if it may pick the ways it chooses the input by considering how the code behaves while running it. Also, how is even "smart fuzzing" similar to theorem provers in any way? Fuzzers still think in terms of runs, but a theorem considers all cases. The best fuzzer wouldn't be able to tell if a sort algorithm works for all inputs, presuming the input size is unbounded. Actually, my understanding is that a fuzzer wouldn't be able to prove if identity function works for all kinds of objects it may be given.
      - dllthomas 3y ago
        I think fuzzing is doing testing, but often using other techniques (including sometimes formal methods) to improve the effectiveness of that testing.
- bluGill 3y ago
  Formal methods catch a different class of problem from other tests and so are worth it. However they cannot catch everything. The classic example: "midpoint = (high + low) / 2" is easy to formally prove correct - but in fact it isn't correct because high + low could overflow.
  - dinosaurdynasty 3y ago
    Any formal system worth its salt is going to model overflow.
    - Jtsummers 3y ago
      And with SPARK/Ada it will. When I was learning it that was actually a very common thing that it caught in my code (various forms of over/underflow errors). In practice most of them would not occur, but a few could have under real-world use-cases.
  - thfuran 3y ago
    If you've formally proved that correct, then either it can't overflow or there's a massive bug in the prover.
  - mathgradthrow 3y ago
    I don't mean to be rude, but why are you commenting on formal methods when you clearly have no idea what they are?
    - bluGill 3y ago
      The specific example I gave was from a 1982 paper (I forget who wrote it, but a big name in computer science) where that was used to prove an algorithm and thus argue that he didn't need to test it as it was proved correct. The famous Donald Knuth has also stated "Beware of bugs in the above code; I have only proved it correct, not tried it.", which again hints that there are limits to proved programs. I'll admit that I don't know much about them, what I know meringues me - but I can't figure out how to use them in the real world. However I know enough to know that they are not perfect.
- _flux 3y ago
  True, I should have remembered to express it as Non-exhaustive testing cannot... I also consider formal methods not testing. But model checking (e.g. with tlc) is something in between, and sort of takes advantage of the "This usually isn't feasible, but it's nice when it is.": when you limit your domain enough, it becomes feasible, yet exhaustively checking each small-world scenario gives a pretty good confidence on the model being correct.
taviso 3y ago
> Testing cannot be used to prove that a flaw doesn't exist, only that it does. FWIW, I wrote a similar blog post about a different encryption bug that really seemed like it should have been found by fuzzing, and had 100% coverage. https://googleprojectzero.blogspot.com/2021/12/this-shouldnt-have-happened.html https://googleprojectzero.blogspot.com/2021/12/this-shouldnt... Not that I disagree with you, just a practical example.
- jcims 3y ago
  It's pretty remarkable how effective fuzzing is despite the layers upon layers of optimizations/assumptions that it requires in order to be feasible at all (eg max_len = 10000). I haven't tinkered with fuzzing since afl was a toddler but its mechanism for pruning the test space seemed so brilliant and tweakable at the time. It would be interesting to find a way to create excursions into these various parameter spaces but some of them are baked into the infrastructure in such a way that it makes it difficult.
deleted 3y ago
[deleted]

by _flux 3y ago

Retr0id 3y ago

> Testing cannot be used to prove that a flaw doesn't exist This is not universally true, formal methods can take you a long way, depending on the problem domain. And sometimes you can test for every possible input. This usually isn't feasible, but it's nice when it is.

dllthomas 3y ago
Formal methods aren't "testing". As you say, though, exhaustive testing is sometimes possible.
- bluGill 3y ago
  It is normally safe to assume the exhaustive testing isn't possible because the total states to exhaustively tests exceeds the number of atoms in the universe. There are a few exceptions, but in general we should assume it is always impossible to exhaustively test programs. Which means we need to use something else to find what the limits are and test only those, or use formal methods (both would be my recommendation - though I'll admit I have yet to figure out how to use formal methods)
  - dllthomas 3y ago
    > in general we should assume it is always impossible to exhaustively test programs The whole program? Yes. For testing individual components, there's no need to assume. The answer is very likely either clearly yes (the input is a handful of booleans) or clearly no (the input is several integers or even unbounded) and for those cases where it's not immediately clear (one i16? Three u8s?) it's probably still not hard to think through for your particular case in your particular context.
    - mananaysiempre 3y ago
      Brute forcing a single 32-bit input has also been usefully performed in some cases, such as for single-precision implementations of special functions[1]. [1] https://randomascii.wordpress.com/2014/01/27/theres-only-four-billion-floatsso-test-them-all/ https://randomascii.wordpress.com/2014/01/27/theres-only-fou...
      - bluGill 3y ago
        32 bits is a bit over 4 billion states, so that is doable. However a lot of algorithms can have more than 32 bits of states and so quickly get beyond what is doable.
        dllthomas 3y ago
        > 32 bits is a bit over 4 billion states, so that is doable. Whether 4B is doable depends on how much work you're doing for each of those states, but yes, "4B" alone certainly doesn't rule it out. There's also a question of whether it goes with your most frequently run tests or is something that's only run occasionally. > However a lot of algorithms can have more than 32 bits of states and so quickly get beyond what is doable. I'm pretty confident we're all in agreement there.
- Retr0id 3y ago
  I agree that it's not testing in the strict sense, but fuzzing isn't really testing either. The work done by a a theorem prover and a fuzzer isn't all that different (and sufficiently advanced fuzzers use SMT solvers etc.)
  - NovemberWhiskey 3y ago
    This seems to neglect the fundamental difference between static and dynamic analysis. Formal methods approaches don’t usually need me to run my code.
  - _flux 3y ago
    I guess I need to disagree :). Why isn't fuzzing testing? Ultimately it ends up running the code and seeing if it works—for some definition of "working", that is, it doesn't crash—even if it may pick the ways it chooses the input by considering how the code behaves while running it. Also, how is even "smart fuzzing" similar to theorem provers in any way? Fuzzers still think in terms of runs, but a theorem considers all cases. The best fuzzer wouldn't be able to tell if a sort algorithm works for all inputs, presuming the input size is unbounded. Actually, my understanding is that a fuzzer wouldn't be able to prove if identity function works for all kinds of objects it may be given.
    - dllthomas 3y ago
      I think fuzzing is doing testing, but often using other techniques (including sometimes formal methods) to improve the effectiveness of that testing.
bluGill 3y ago
Formal methods catch a different class of problem from other tests and so are worth it. However they cannot catch everything. The classic example: "midpoint = (high + low) / 2" is easy to formally prove correct - but in fact it isn't correct because high + low could overflow.
- dinosaurdynasty 3y ago
  Any formal system worth its salt is going to model overflow.
  - Jtsummers 3y ago
    And with SPARK/Ada it will. When I was learning it that was actually a very common thing that it caught in my code (various forms of over/underflow errors). In practice most of them would not occur, but a few could have under real-world use-cases.
- thfuran 3y ago
  If you've formally proved that correct, then either it can't overflow or there's a massive bug in the prover.
- mathgradthrow 3y ago
  I don't mean to be rude, but why are you commenting on formal methods when you clearly have no idea what they are?
  - bluGill 3y ago
    The specific example I gave was from a 1982 paper (I forget who wrote it, but a big name in computer science) where that was used to prove an algorithm and thus argue that he didn't need to test it as it was proved correct. The famous Donald Knuth has also stated "Beware of bugs in the above code; I have only proved it correct, not tried it.", which again hints that there are limits to proved programs. I'll admit that I don't know much about them, what I know meringues me - but I can't figure out how to use them in the real world. However I know enough to know that they are not perfect.
_flux 3y ago
True, I should have remembered to express it as Non-exhaustive testing cannot... I also consider formal methods not testing. But model checking (e.g. with tlc) is something in between, and sort of takes advantage of the "This usually isn't feasible, but it's nice when it is.": when you limit your domain enough, it becomes feasible, yet exhaustively checking each small-world scenario gives a pretty good confidence on the model being correct.

taviso 3y ago

> Testing cannot be used to prove that a flaw doesn't exist, only that it does. FWIW, I wrote a similar blog post about a different encryption bug that really seemed like it should have been found by fuzzing, and had 100% coverage. https://googleprojectzero.blogspot.com/2021/12/this-shouldnt-have-happened.html https://googleprojectzero.blogspot.com/2021/12/this-shouldnt... Not that I disagree with you, just a practical example.

jcims 3y ago
It's pretty remarkable how effective fuzzing is despite the layers upon layers of optimizations/assumptions that it requires in order to be feasible at all (eg max_len = 10000). I haven't tinkered with fuzzing since afl was a toddler but its mechanism for pruning the test space seemed so brilliant and tweakable at the time. It would be interesting to find a way to create excursions into these various parameter spaces but some of them are baked into the infrastructure in such a way that it makes it difficult.

deleted 3y ago

[deleted]