3 ms·

It depends on the algorithm. If the algorithm is immune to faults, the worst thing that can happen is that you produce an invalid signature, which will then be

It depends on the algorithm. If the algorithm is immune to faults, the worst thing that can happen is that you produce an invalid signature, which will then be rejected. This turns the security concern into a more mundane performance concern.

dspillett 9y ago
> It depends on the algorithm ... If the algorithm is immune to faults The truly paranoid would never believe any algorithm is immune to faults. Even if full mathematical code analysis shows it to be so, can you prove that the proving analysis algorithm itself is immune to faults? It is potentially faulty turtles all the way down!
- loup-vaillant 9y ago
  The higher that tower of turtles, the stronger the confidence. The proof checker can be ran several times to account for faults. Then you don't need to run it at all (it's proven). And you can use another proof checker (or that proof checker itself) to prove that the proof checker works. Etc. Now there's the problem of the compiler, which gives a upper bound on the confidence you can have: if there's a bug in it, you're screwed even with a correct algorithm. > Even if full mathematical code analysis shows it to be so Come to think of it, that may not be possible for lots and lots of algorithms —whose mathematical security is only conjectured to begin with. Thanks for pointing that out.
  - dspillett 9y ago
    I expect (though I'm not theoretical mathematician so I'm happy to be told how wrong I am!) any formal proof method will have algorithms that it can't do anything with, and that there will exist those that none can deal with. Presumably there is a code version of Gödel's incompleteness theorems somewhere in Turing's work or similar.
    - loup-vaillant 9y ago
      Correct, you cannot prove everything. But you can prove many things. Many programs we care about can be proven correct (for whatever definition of "correct" we manage to formally specify), and those we can't prove correct can probably be transformed into provable versions —assuming they're short enough.
    - DonbunEf7 9y ago
      In particular, a system usually cannot prove itself consistent. However, we have developed systems expressly for the purpose of being as consistent as our intuition for logic could allow it to be. I'm willing to trust Metamath [0] based on the formalism that they've chosen, which is a dead-simple term-rewriting formalism that is suitable for building pretty much any mathematical structure, given enough time and effort. A better question would be whether, in a theoretical sense, fault-free algorithms even exist. There are similar questions, like whether one-way functions exist, where we have lots of evidence to suggest that the answer is "yes" but we have yet to prove it. [0] http://us.metamath.org/ http://us.metamath.org/
  - AstralStorm 9y ago
    You can skip the step of compiler fault by directly verifying machine code or by refining an algorithm provably into machine code. This is what SEL4 people are doing. The remaining part is verifying if your machine model is correct. Not trivial for some CPU and memory controller as complex as x86. (Even though just a subset of operations are used.) Doing this also allows you a proof against fault attacks and timing attacks.

dspillett 9y ago

> It depends on the algorithm ... If the algorithm is immune to faults The truly paranoid would never believe any algorithm is immune to faults. Even if full mathematical code analysis shows it to be so, can you prove that the proving analysis algorithm itself is immune to faults? It is potentially faulty turtles all the way down!

loup-vaillant 9y ago
The higher that tower of turtles, the stronger the confidence. The proof checker can be ran several times to account for faults. Then you don't need to run it at all (it's proven). And you can use another proof checker (or that proof checker itself) to prove that the proof checker works. Etc. Now there's the problem of the compiler, which gives a upper bound on the confidence you can have: if there's a bug in it, you're screwed even with a correct algorithm. > Even if full mathematical code analysis shows it to be so Come to think of it, that may not be possible for lots and lots of algorithms —whose mathematical security is only conjectured to begin with. Thanks for pointing that out.
- dspillett 9y ago
  I expect (though I'm not theoretical mathematician so I'm happy to be told how wrong I am!) any formal proof method will have algorithms that it can't do anything with, and that there will exist those that none can deal with. Presumably there is a code version of Gödel's incompleteness theorems somewhere in Turing's work or similar.
  - loup-vaillant 9y ago
    Correct, you cannot prove everything. But you can prove many things. Many programs we care about can be proven correct (for whatever definition of "correct" we manage to formally specify), and those we can't prove correct can probably be transformed into provable versions —assuming they're short enough.
  - DonbunEf7 9y ago
    In particular, a system usually cannot prove itself consistent. However, we have developed systems expressly for the purpose of being as consistent as our intuition for logic could allow it to be. I'm willing to trust Metamath [0] based on the formalism that they've chosen, which is a dead-simple term-rewriting formalism that is suitable for building pretty much any mathematical structure, given enough time and effort. A better question would be whether, in a theoretical sense, fault-free algorithms even exist. There are similar questions, like whether one-way functions exist, where we have lots of evidence to suggest that the answer is "yes" but we have yet to prove it. [0] http://us.metamath.org/ http://us.metamath.org/
- AstralStorm 9y ago
  You can skip the step of compiler fault by directly verifying machine code or by refining an algorithm provably into machine code. This is what SEL4 people are doing. The remaining part is verifying if your machine model is correct. Not trivial for some CPU and memory controller as complex as x86. (Even though just a subset of operations are used.) Doing this also allows you a proof against fault attacks and timing attacks.