3 ms·

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

by 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.
- anyfoo 6y ago
  That is not how privilege boundaries work.
  - c22 6y ago
    Then how do explain privilege escalation attacks other than as a user discovering a path to elevated privileges that was not anticipated by the designers? Can't you "brute force" even the most theoretically rock solid privilege boundary by simply attaching your own computer to the memory in question?
    - anyfoo 6y ago
      > other than as a user discovering a path to elevated privileges that was not anticipated by the designers Most of the time, a barrier to elevated privileges that was not correctly implemented, i.e. a bug, not anything the designer did not anticipate. > Can't you "brute force" even the most theoretically rock solid privilege boundary by simply attaching your own computer to the memory in question? So? Does that mean it's not worth looking at the paths where the attacker does not have physical access of the machine that sits in some data center's secured basement?
tsimionescu 6y ago
> 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. I don't think this is obvious, even for theoretical software, much less for practical software. Even formal methods have limitations. A very public recent example was of the formally proven logic in Intel and other processors around speculative execution (Spectre, Meltdown etc.). That logic was formally proven not to leak information, but the formal model wasn't actually sophisticated enough. Note that these weren't hardware bugs (they weren't bugs in the electrical components of the processor or in the analog logic), they were logic bugs in the processor's code (whether that was microcode or burned into the processor is less relevant). In general, you can prove that a piece of software adheres to some specification, but you can't prove that the specification itself is complete enough. Of course, realistic software has many more layers of uncertainty, and realistic formal verification is far to costly to apply to anything but very short programs.
- anyfoo 6y ago
  Thanks, this is for once in this thread, a real caveat in the application formal verification (or rigorous type systems). It's hard, it's not unlimited, and one may have fail to state crucial properties that matter in the first place. Still, there are a lot of properties that are easy to state, and a lot of properties that are feasible to prove, and the intersection of these two can be very valuable in eradicating common issues in critical software, be it out-of-bounds pointers or your garden variety type confusion. (Again, not always possible, thanks to the halting problem, but often.) The cost may indeed be prohibitive, though.

by comex 6y ago

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.

anyfoo 6y ago
That is not how privilege boundaries work.
- c22 6y ago
  Then how do explain privilege escalation attacks other than as a user discovering a path to elevated privileges that was not anticipated by the designers? Can't you "brute force" even the most theoretically rock solid privilege boundary by simply attaching your own computer to the memory in question?
  - anyfoo 6y ago
    > other than as a user discovering a path to elevated privileges that was not anticipated by the designers Most of the time, a barrier to elevated privileges that was not correctly implemented, i.e. a bug, not anything the designer did not anticipate. > Can't you "brute force" even the most theoretically rock solid privilege boundary by simply attaching your own computer to the memory in question? So? Does that mean it's not worth looking at the paths where the attacker does not have physical access of the machine that sits in some data center's secured basement?

tsimionescu 6y ago

> 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. I don't think this is obvious, even for theoretical software, much less for practical software. Even formal methods have limitations. A very public recent example was of the formally proven logic in Intel and other processors around speculative execution (Spectre, Meltdown etc.). That logic was formally proven not to leak information, but the formal model wasn't actually sophisticated enough. Note that these weren't hardware bugs (they weren't bugs in the electrical components of the processor or in the analog logic), they were logic bugs in the processor's code (whether that was microcode or burned into the processor is less relevant). In general, you can prove that a piece of software adheres to some specification, but you can't prove that the specification itself is complete enough. Of course, realistic software has many more layers of uncertainty, and realistic formal verification is far to costly to apply to anything but very short programs.

anyfoo 6y ago
Thanks, this is for once in this thread, a real caveat in the application formal verification (or rigorous type systems). It's hard, it's not unlimited, and one may have fail to state crucial properties that matter in the first place. Still, there are a lot of properties that are easy to state, and a lot of properties that are feasible to prove, and the intersection of these two can be very valuable in eradicating common issues in critical software, be it out-of-bounds pointers or your garden variety type confusion. (Again, not always possible, thanks to the halting problem, but often.) The cost may indeed be prohibitive, though.