5 ms·

I don't understand this reasoning at all. Locks attempt to artificially limit the (physical) attack surface as well. This could, in fact, be a reasonable defini

by c22 6y ago

I don't understand this reasoning at all. Locks attempt to artificially limit the (physical) attack surface as well. This could, in fact, be a reasonable definition of a lock. So people come up with wonderful and surprising configurations of matter that cause these artificial limitations to fail providing direct access to the lock's root mechanism (via unanticipated route). This is analogous to virtual attacks on information systems which are hardened against familiar routes of ingress and vulnerable to those which are wonderful and surprising.

anyfoo 6y ago
You can apply formal methods to code that you cannot in physical reality. If I show you the equation “x == y”, you won’t be able to pick 7 and 8 to make the equation true. If I give you a mechanical device that works with beads to answer the same question, you might make it work. Of course computers are eventually physical reality, too, and things like rowhammer show that you don’t even need traditional “bugs” to escape your mathematical utopia. But all the bugs talked about here are entirely the fault of the software.
- vntok 6y ago
  Well one could try to change the meaning of "==" to make the equation true. Think about comparator overloading in supported languages where the x and/or y variables are actually objects, for example.
  - anyfoo 6y ago
    I was talking about algebra, not about C++.
- laumars 6y ago
  Except you can artificially alter the value of x or y via numerous different methods of attack via frameworks that supersede the code which has been written the formal methods against.
  - anyfoo 6y ago
    Then you did not do actual formal verification, but something wrong and useless.
    - laumars 6y ago
      Fuzz attacks have proven that edge cases are inescapable
      - anyfoo 6y ago
        Fuzzing is only relevant where formal verification cannot be exhaustively applied (which is reality in turing complete languages), or is too cost-prohibitive. In a formally verified program, fuzzing is redundant and useless. Are you going to fuzz the program "x = y+1; return x;", or are you convinced already that it will always return either y+1 (with y treated as a natural number, not a finite width integer), or 0 (if y was the maximum value in the unsigned data type of x), and that it will never access memory out of bounds? Formal verification is exactly that, just usually in less obvious scenarios. Advanced type systems do the same implicitly by making expressions that would violate such properties (or where they cannot be proven) not type check.
        Sharlin 6y ago
        > x = y+1; return x; Funny you should use that specific example, because your analysis fails to account for the case where a) this is C or C++, b) y has a signed integer type, and c) its value is the maximum value of said type. In that case the behavior is, infamously, undefined, and anything can happen including accessing memory out of bounds. This is exactly the sort of corner case that fuzzing is designed to reveal. Formal analysis of the function would, of course, also flag the fact that the set of values of y for which the program is well-defined is not the entire domain of its type.
        skissane 6y ago
        > In that case the behavior is, infamously, undefined, and anything can happen including accessing memory out of bounds Undefined per the standard, yes. Undefined per a particular implementation? Well, that’s up to each particular implementation. A compiler is free to make stronger guarantees than the standard requires. And, a formal verification is allowed to presume a particular compiler, and rely on whatever stronger guarantees it makes. Which means of course that the verification is only valid as long as that compiler is used, and changing the compiler requires revisiting the verification (even if only just to confirm that the new compiler makes the same guarantees) - but, in many cases, especially the cases in which formal verification is in the most demand (safety critical systems), that’s an acceptable limitation.
comex 6y ago
I don’t know about the GP’s wording, but there is a difference. It is possible for a piece of software to be perfectly secure against software-based attacks, i.e. there‘s no possible data you can send it that will cause it to misbehave. It is not possible for a lock to be perfectly secure against physical attacks; if nothing else, you can always break it with brute force. Of course, even perfect software is susceptible to physical attacks on the hardware it’s running on, but that’s different.
- ngneer 6y ago
  No, there is no difference. Locks and software implement or abide by control laws. In your analogy, if you give perfect software an input and it behaves as expected, then that is the same as walking up to a locked door, trying to open it and failing. Both systems are susceptible to control bypass.
  - anyfoo 6y ago
    The point is that for some programs[1], you can prove that all inputs will lead to an output with certain properties. With a physical lock, you cannot. For physical locks, you cannot even rigorously define the "input". [1] Not always, unfortunately, if your language is turing complete. You might be able to prove weaker, but still very useful statements, like "no input will cause a point to be dereferenced out of bounds".
    - ngneer 6y ago
      Yes, you may prove such a statement about a program. But you will not be able to prove that about the physical system where the program is running (assuming you want to run your program and not just reason about it as a mathematical object). If you need an example, consider Plundervolt.
- c22 6y ago
  I am not convinced. If your software is secured with any sort of key then you can break this with brute force also. All other attempts to prevent unauthorized access are applications of varying degrees of obfuscation and indirection, the same as in physical lock design.

by c22 6y ago

anyfoo 6y ago

You can apply formal methods to code that you cannot in physical reality. If I show you the equation “x == y”, you won’t be able to pick 7 and 8 to make the equation true. If I give you a mechanical device that works with beads to answer the same question, you might make it work. Of course computers are eventually physical reality, too, and things like rowhammer show that you don’t even need traditional “bugs” to escape your mathematical utopia. But all the bugs talked about here are entirely the fault of the software.

vntok 6y ago
Well one could try to change the meaning of "==" to make the equation true. Think about comparator overloading in supported languages where the x and/or y variables are actually objects, for example.
- anyfoo 6y ago
  I was talking about algebra, not about C++.
laumars 6y ago
Except you can artificially alter the value of x or y via numerous different methods of attack via frameworks that supersede the code which has been written the formal methods against.
- anyfoo 6y ago
  Then you did not do actual formal verification, but something wrong and useless.
  - laumars 6y ago
    Fuzz attacks have proven that edge cases are inescapable
    - anyfoo 6y ago
      Fuzzing is only relevant where formal verification cannot be exhaustively applied (which is reality in turing complete languages), or is too cost-prohibitive. In a formally verified program, fuzzing is redundant and useless. Are you going to fuzz the program "x = y+1; return x;", or are you convinced already that it will always return either y+1 (with y treated as a natural number, not a finite width integer), or 0 (if y was the maximum value in the unsigned data type of x), and that it will never access memory out of bounds? Formal verification is exactly that, just usually in less obvious scenarios. Advanced type systems do the same implicitly by making expressions that would violate such properties (or where they cannot be proven) not type check.
      - Sharlin 6y ago
        > x = y+1; return x; Funny you should use that specific example, because your analysis fails to account for the case where a) this is C or C++, b) y has a signed integer type, and c) its value is the maximum value of said type. In that case the behavior is, infamously, undefined, and anything can happen including accessing memory out of bounds. This is exactly the sort of corner case that fuzzing is designed to reveal. Formal analysis of the function would, of course, also flag the fact that the set of values of y for which the program is well-defined is not the entire domain of its type.
        skissane 6y ago
        > In that case the behavior is, infamously, undefined, and anything can happen including accessing memory out of bounds Undefined per the standard, yes. Undefined per a particular implementation? Well, that’s up to each particular implementation. A compiler is free to make stronger guarantees than the standard requires. And, a formal verification is allowed to presume a particular compiler, and rely on whatever stronger guarantees it makes. Which means of course that the verification is only valid as long as that compiler is used, and changing the compiler requires revisiting the verification (even if only just to confirm that the new compiler makes the same guarantees) - but, in many cases, especially the cases in which formal verification is in the most demand (safety critical systems), that’s an acceptable limitation.

comex 6y ago

I don’t know about the GP’s wording, but there is a difference. It is possible for a piece of software to be perfectly secure against software-based attacks, i.e. there‘s no possible data you can send it that will cause it to misbehave. It is not possible for a lock to be perfectly secure against physical attacks; if nothing else, you can always break it with brute force. Of course, even perfect software is susceptible to physical attacks on the hardware it’s running on, but that’s different.

ngneer 6y ago
No, there is no difference. Locks and software implement or abide by control laws. In your analogy, if you give perfect software an input and it behaves as expected, then that is the same as walking up to a locked door, trying to open it and failing. Both systems are susceptible to control bypass.
- anyfoo 6y ago
  The point is that for some programs[1], you can prove that all inputs will lead to an output with certain properties. With a physical lock, you cannot. For physical locks, you cannot even rigorously define the "input". [1] Not always, unfortunately, if your language is turing complete. You might be able to prove weaker, but still very useful statements, like "no input will cause a point to be dereferenced out of bounds".
  - ngneer 6y ago
    Yes, you may prove such a statement about a program. But you will not be able to prove that about the physical system where the program is running (assuming you want to run your program and not just reason about it as a mathematical object). If you need an example, consider Plundervolt.
c22 6y ago
I am not convinced. If your software is secured with any sort of key then you can break this with brute force also. All other attempts to prevent unauthorized access are applications of varying degrees of obfuscation and indirection, the same as in physical lock design.