5 ms·

Locks are physical devices and so are susceptible to all manner of wonderful and surprising physical attacks. Programming languages can artificially limit the

Locks are physical devices and so are susceptible to all manner of wonderful and surprising physical attacks. Programming languages can artificially limit the attack surface. (Up to hardware exploits which can subvert the processor itself.)

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.
- 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.
laumars 6y ago
SQLite is a software device and so is susceptible to all manner of wonderful and surprising software attacks
- Quekid5 6y ago
  SQLite is written in a manner/language which only really affords tests, not proof of correctness. (My point was that it might have been written in a language where many of these exploits would not have been possible without subverting the hardware it's running on, but I see from the other responses that I may have phrased it a bit too obliquely.)
  - laumars 6y ago
    Part of the reason SQLite is so prolific is because of the language used, not in spite of it. It’s enabled people to run SQLite on a broad range of hardware, device types and called from any language that supports native C calls (which is a massive array of languages). And let’s not forget the truly amazing performance you get from SQLite too. Had SQLite been written in a language that would have made it easier to perform a proof of correctness then it wouldn’t be nearly as widely used and because of that language choice and then it likely wouldn’t have had the resources (financial nor community input) to complete a proof anyway. So would it have actually been any less buggy if it weren’t a C project? Sometimes worse is better and moaning about “what if” is neither constructive nor even warranted when you consider just how well written SQLite already is and how abundant the tests are.
    - Quekid5 6y ago
      Of course it's popularity is due to using C... but that's not what we were talking about, was it? > Sometimes worse is better and moaning about “what if” is neither constructive[...] ... and yet here we are talking about extremely dangerous and possibly far-reaching vulnerabilities in SQLite.
heavenlyblue 6y ago
An electronic lock is a physical device and you won’t be able to pick it as easy as you are saying.

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.
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.

laumars 6y ago

SQLite is a software device and so is susceptible to all manner of wonderful and surprising software attacks

Quekid5 6y ago
SQLite is written in a manner/language which only really affords tests, not proof of correctness. (My point was that it might have been written in a language where many of these exploits would not have been possible without subverting the hardware it's running on, but I see from the other responses that I may have phrased it a bit too obliquely.)
- laumars 6y ago
  Part of the reason SQLite is so prolific is because of the language used, not in spite of it. It’s enabled people to run SQLite on a broad range of hardware, device types and called from any language that supports native C calls (which is a massive array of languages). And let’s not forget the truly amazing performance you get from SQLite too. Had SQLite been written in a language that would have made it easier to perform a proof of correctness then it wouldn’t be nearly as widely used and because of that language choice and then it likely wouldn’t have had the resources (financial nor community input) to complete a proof anyway. So would it have actually been any less buggy if it weren’t a C project? Sometimes worse is better and moaning about “what if” is neither constructive nor even warranted when you consider just how well written SQLite already is and how abundant the tests are.
  - Quekid5 6y ago
    Of course it's popularity is due to using C... but that's not what we were talking about, was it? > Sometimes worse is better and moaning about “what if” is neither constructive[...] ... and yet here we are talking about extremely dangerous and possibly far-reaching vulnerabilities in SQLite.

heavenlyblue 6y ago

An electronic lock is a physical device and you won’t be able to pick it as easy as you are saying.