4 ms·

How would you do that? Even if you have thousand lockpickers going at it with thousand tools, all unsuccessful, the 1001th might find a way. Whereas if I tell

by anyfoo 6y ago

How would you do that? Even if you have thousand lockpickers going at it with thousand tools, all unsuccessful, the 1001th might find a way. Whereas if I tell you that x is bigger than y if x is y plus 1, that’s definitive.

ngneer 6y ago
You can prove it in your model of the system, but you are limited to the model. If your model of the system is the same as the adversaries' then your security design may work. Of course, the real definition of security is financial. No one cares if your lock can be picked by the 1001th person if the security claim is it takes at least 1000 lockpickers to be sufficiently incentivized.
- anyfoo 6y ago
  I'm not talking about "security models", I'm talking about plain correctness of software. Any correctness issue (any "bug") can potentially become a security issue if it's reachable through a privilege boundary. And if exploited correctness issues are not in fact the majority of software security issues, they are at least a massive contributor and the subject of this entire discussion. Examples are a sorted list that inadvertently becomes unsorted while the rest of the program still assumes ordering, or more simply and classically, a pointer that's pointing out of its assumed bounds. There is no "security model" to consider on that level, and with respect to lockpicking I just wanted to explain why software engineers have access to wonderful tools and methodologies that designers of physical locks don't.
  - Normal_gaussian 6y ago
    I took a slightly different understanding from that comment than I think you did. I took the comment in two parts; the second being a tangential suggestion that security is financial. The first was more interesting. Taken to be a reply to your claim that x=y+1 implies x>y, it is grounded more in theory. The claim is one grounded in a given model - a prevailing mathematical one - and is undoubetdly correct in that model and in the many of the models we use around us. That does not, surprisingly, make it true. There are countless models in which it is false, though it seems unlikely these are useful models. There are also models which are to a degree isomorphic to the current (standard?) models of fancy. In these may lie a way to subvert the expectation of their version of "x>y when x=y+1"
abjKT26nO8 6y ago
> Whereas if I tell you that x is bigger than y if x is y plus 1, that’s definitive. Most code doesn't check whether incrementing a variable causes an overflow, so in practice the test you're referring to is still vulnerable.
- anyfoo 6y ago
  No, because when you are formally verifying programs, or employing a type system that implicitly does so, you take that overflow and any other "surprising" behavior into account. Verifying that the program either cannot reach such an overflow condition, or otherwise handles it correctly, is exactly the point of formal verification. It's not magic or unpredictable, we know exactly how integers or any other representable data type behaves. (Also note that you were assuming integers here, as floating point would behave yet another way.) I wasn't proposing a "test", I was demonstrating the difference between mathematical rigor and physical reality, and in my chosen domain for x and y, overflow is not happening.
Dylan16807 6y ago
Well, if you want something as primitive as adding 1, you can prove that a solid plate of steel can't be picked. Once you get into moving parts and, even worse, useful moving parts, things get a lot trickier. But if you severely limit your inputs you might be able to get somewhere. Like one of those locks where the mechanism pulls the key completely inside before applying it to the keyway: https://www.youtube.com/watch?v=OLsJDELd4lo https://www.youtube.com/watch?v=OLsJDELd4lo https://www.youtube.com/watch?v=5J2rwawhZWI https://www.youtube.com/watch?v=5J2rwawhZWI I'd expect many designs in that class to be immune to most definitions of 'picking'.

by anyfoo 6y ago

ngneer 6y ago

You can prove it in your model of the system, but you are limited to the model. If your model of the system is the same as the adversaries' then your security design may work. Of course, the real definition of security is financial. No one cares if your lock can be picked by the 1001th person if the security claim is it takes at least 1000 lockpickers to be sufficiently incentivized.

anyfoo 6y ago
I'm not talking about "security models", I'm talking about plain correctness of software. Any correctness issue (any "bug") can potentially become a security issue if it's reachable through a privilege boundary. And if exploited correctness issues are not in fact the majority of software security issues, they are at least a massive contributor and the subject of this entire discussion. Examples are a sorted list that inadvertently becomes unsorted while the rest of the program still assumes ordering, or more simply and classically, a pointer that's pointing out of its assumed bounds. There is no "security model" to consider on that level, and with respect to lockpicking I just wanted to explain why software engineers have access to wonderful tools and methodologies that designers of physical locks don't.
- Normal_gaussian 6y ago
  I took a slightly different understanding from that comment than I think you did. I took the comment in two parts; the second being a tangential suggestion that security is financial. The first was more interesting. Taken to be a reply to your claim that x=y+1 implies x>y, it is grounded more in theory. The claim is one grounded in a given model - a prevailing mathematical one - and is undoubetdly correct in that model and in the many of the models we use around us. That does not, surprisingly, make it true. There are countless models in which it is false, though it seems unlikely these are useful models. There are also models which are to a degree isomorphic to the current (standard?) models of fancy. In these may lie a way to subvert the expectation of their version of "x>y when x=y+1"

abjKT26nO8 6y ago

> Whereas if I tell you that x is bigger than y if x is y plus 1, that’s definitive. Most code doesn't check whether incrementing a variable causes an overflow, so in practice the test you're referring to is still vulnerable.

anyfoo 6y ago
No, because when you are formally verifying programs, or employing a type system that implicitly does so, you take that overflow and any other "surprising" behavior into account. Verifying that the program either cannot reach such an overflow condition, or otherwise handles it correctly, is exactly the point of formal verification. It's not magic or unpredictable, we know exactly how integers or any other representable data type behaves. (Also note that you were assuming integers here, as floating point would behave yet another way.) I wasn't proposing a "test", I was demonstrating the difference between mathematical rigor and physical reality, and in my chosen domain for x and y, overflow is not happening.

Dylan16807 6y ago

Well, if you want something as primitive as adding 1, you can prove that a solid plate of steel can't be picked. Once you get into moving parts and, even worse, useful moving parts, things get a lot trickier. But if you severely limit your inputs you might be able to get somewhere. Like one of those locks where the mechanism pulls the key completely inside before applying it to the keyway: https://www.youtube.com/watch?v=OLsJDELd4lo https://www.youtube.com/watch?v=OLsJDELd4lo https://www.youtube.com/watch?v=5J2rwawhZWI https://www.youtube.com/watch?v=5J2rwawhZWI I'd expect many designs in that class to be immune to most definitions of 'picking'.