4 ms·

Mostly it involves people making systems that are too complex to trivially analyze. You can not write arbitrarily complex secure code. You need to limit your

by jwlake 5y ago

Mostly it involves people making systems that are too complex to trivially analyze. You can not write arbitrarily complex secure code. You need to limit your scope and do one very simple thing extremely tersely and correctly. You can make powerful systems with simple correct independent components. You can not make complex secure monolithic systems. It gets even worse when you look at contracts with delegation. The problem with most "smart" contracts is they have abstractions, delegation and scope creep.

raverbashing 5y ago
Yes, I agree. Most of the security of smart contracts should be in the VM. Things like self-asserting the results and only finishing the transaction if it actually passes a double-check. Or set value limits to each smart-contract (so even if there's a bug it will only operate on 0.00001 BTC for example).
- admax88q 5y ago
  If your smart contract can only process tiny amounts of money, then it's no useful.
  - raverbashing 5y ago
    That's not what I'm saying. But sure, if you think you can write smart contracts without bugs for all means don't set a limit. I'm saying you should define a ceiling for your smart contract so in case of a bug, no transactions over that ceiling go forward. So if you have a stupid bug that causes you to transfer 1BTC instead of 0.001BTC you don't lose all your money.
    - recursive 5y ago
      What's the distinction? That just means you won't be able to use smart contracts for anything useful.
- jwlake 5y ago
  This is mostly infeasible because the VM has no idea what's worth anything. There is no reasonable price in absolute terms for a BTC or ETH or DOGE or $DUMBCOIN. The key is that the contracts need to be minimal and analyzable, so its ~100 lines of code you can manually analyze. Documented separately all the edge cases, or ideally removed through good design so they simply don't exist. A bunch of problems I've seen in the real world of crypto are annoying edge cases that you can fix with an if statement, or ideally change the design to remove them completely. It's actually a surprisingly hard space because you're trying to make terse, complete and secure code. In normal web/systems programming you have layers of security; internal services, external services, firewalls, access controls, vpns, security by obscurity, etc etc etc. In crypto you have none of that. Everything is 100% public, the code probably should be published, or else it is trivially decompiled. If there is a problem someone will find it if there is value in finding it.
  - raverbashing 5y ago
    Thanks for your comment. Yes I agree the absolute value in some coin is not a great metric. > In normal web/systems programming you have layers of security; In crypto you have none of that. Yes, that's what I mean. Why not? > The key is that the contracts need to be minimal and analyzable Agree, but even short contracts might have bugs. Betting on "self-paying bug bounts" is not a good bet. What I'm proposing is that every smart contract double-checks its expected results
spicybright 5y ago
I don't know much in the field, but formally verifiable programming methods come to mind. You'll potentially have less of a chance for contracts to be exploited (at least compared to what we have now). That said, you can't protect against infrastructure exploits as easily, mathematically flawless program or not.
- foobiekr 5y ago
  Formal methods are about matching the spec. Errors in the spec are still an issue. Moreover, there is very, very little formally verified code in the world, much less than you'd believe. My former professor (RIP) oversaw the formal verification of the F-16 computer software and it still had significant bugs in the end where the specification itself was incomplete or in error. And that was a multi-year, team-scale effort. No one is doing that for smart contracts.
  - impreciouschild 5y ago
    MakerDAO is formally verified. https://medium.com/@MakerDAO/the-code-is-ready-2aee2aa62e73 https://medium.com/@MakerDAO/the-code-is-ready-2aee2aa62e73
  - tialaramex 5y ago
    A nice practical example from TLS 1.3: TLS 1.3 has been formally proven (not an implementation, but the standard itself). To the extent the mathematicians correctly explained what the TLS 1.3 RFC says, and correctly told the machine what TLS 1.3 is supposed to do, the machine proof says this protocol does what we intended. That work assumes a bunch of components are black boxes, they must work. If we ever lose confidence that they work, we've got to throw those out. So for example SHA-256, AES GCM, X25519, the proof doesn't say "We prove these work" it says "Assuming you're right that these do what they're designed to do the rest of your proof holds" Anyway, one of the assumptions in that proof is a surprise to a human implementing TLS 1.3, it isn't explicitly mentioned in the TLS 1.3 document as written. And so the result is, if you didn't obey that assumption, the proof doesn't hold and sure enough you're vulnerable to an attack. The assumption is for Pre-shared Keys (e.g. IoT devices A and B don't want to bother with certificates, so they just use pre-agreed random keys) each device pairing has its own PSK. A person looking at the design figures hey, got two devices Alice and Bob, I can just have a single key K known to both devices, and everything is secure. But that's wrong - and the TLS 1.3 proof doesn't say this will work. Here's what bad guys can do, it's called the Selfie Attack: Alice sends a message to Bob, maybe "Did you feed the cat?" and it's encrypted with key K. Normally Bob receives the message, maybe answers "Yes I fed the cat" also encrypted with key K and all is well. But now Mallory is on a network able to intercept and re-route messages. Alice sends to Bob, "Did you feed the cat?" encrypted with key K. Mallory can't read or tamper with this message, it's encrypted with key K and TLS 1.3 works as designed, but Mallory just re-directs the message back to Alice, "Did you feed the cat?". The message is encrypted with key K, Alice assumes Bob sent it, and replies "No, I didn't feed the cat" also encrypted with key K, which Mallory re-directs again back to Alice, who now mistakenly believes that Bob has told her he hasn't fed the cat. There are obviously a bunch of things you could do to fix this. First of all you could just have more PSKs. If Alice's message to Bob is always encrypted using the Alice->Bob shared key, when Alice actually receives it instead she knows something is wrong immediately. Or you could just prefix each message with To/From information, like an old-fashioned email and that works too so long as you check it. But the important observation is that this is an assumption in a proof that nobody really surfaced until it was too late. If researchers had told the proof system "No, the PSKs can be the same" the proof fails. Or if they'd carefully explained to the TLS Working Group, "We had to spell out that the PSKs must be different" then today RFC 8446 would likely explain that you need to do that or you've got a security problem. But neither happened and this attack slipped between the cracks.

by jwlake 5y ago

raverbashing 5y ago

Yes, I agree. Most of the security of smart contracts should be in the VM. Things like self-asserting the results and only finishing the transaction if it actually passes a double-check. Or set value limits to each smart-contract (so even if there's a bug it will only operate on 0.00001 BTC for example).

admax88q 5y ago
If your smart contract can only process tiny amounts of money, then it's no useful.
- raverbashing 5y ago
  That's not what I'm saying. But sure, if you think you can write smart contracts without bugs for all means don't set a limit. I'm saying you should define a ceiling for your smart contract so in case of a bug, no transactions over that ceiling go forward. So if you have a stupid bug that causes you to transfer 1BTC instead of 0.001BTC you don't lose all your money.
  - recursive 5y ago
    What's the distinction? That just means you won't be able to use smart contracts for anything useful.
jwlake 5y ago
This is mostly infeasible because the VM has no idea what's worth anything. There is no reasonable price in absolute terms for a BTC or ETH or DOGE or $DUMBCOIN. The key is that the contracts need to be minimal and analyzable, so its ~100 lines of code you can manually analyze. Documented separately all the edge cases, or ideally removed through good design so they simply don't exist. A bunch of problems I've seen in the real world of crypto are annoying edge cases that you can fix with an if statement, or ideally change the design to remove them completely. It's actually a surprisingly hard space because you're trying to make terse, complete and secure code. In normal web/systems programming you have layers of security; internal services, external services, firewalls, access controls, vpns, security by obscurity, etc etc etc. In crypto you have none of that. Everything is 100% public, the code probably should be published, or else it is trivially decompiled. If there is a problem someone will find it if there is value in finding it.
- raverbashing 5y ago
  Thanks for your comment. Yes I agree the absolute value in some coin is not a great metric. > In normal web/systems programming you have layers of security; In crypto you have none of that. Yes, that's what I mean. Why not? > The key is that the contracts need to be minimal and analyzable Agree, but even short contracts might have bugs. Betting on "self-paying bug bounts" is not a good bet. What I'm proposing is that every smart contract double-checks its expected results

spicybright 5y ago

I don't know much in the field, but formally verifiable programming methods come to mind. You'll potentially have less of a chance for contracts to be exploited (at least compared to what we have now). That said, you can't protect against infrastructure exploits as easily, mathematically flawless program or not.

foobiekr 5y ago
Formal methods are about matching the spec. Errors in the spec are still an issue. Moreover, there is very, very little formally verified code in the world, much less than you'd believe. My former professor (RIP) oversaw the formal verification of the F-16 computer software and it still had significant bugs in the end where the specification itself was incomplete or in error. And that was a multi-year, team-scale effort. No one is doing that for smart contracts.
- impreciouschild 5y ago
  MakerDAO is formally verified. https://medium.com/@MakerDAO/the-code-is-ready-2aee2aa62e73 https://medium.com/@MakerDAO/the-code-is-ready-2aee2aa62e73
- tialaramex 5y ago
  A nice practical example from TLS 1.3: TLS 1.3 has been formally proven (not an implementation, but the standard itself). To the extent the mathematicians correctly explained what the TLS 1.3 RFC says, and correctly told the machine what TLS 1.3 is supposed to do, the machine proof says this protocol does what we intended. That work assumes a bunch of components are black boxes, they must work. If we ever lose confidence that they work, we've got to throw those out. So for example SHA-256, AES GCM, X25519, the proof doesn't say "We prove these work" it says "Assuming you're right that these do what they're designed to do the rest of your proof holds" Anyway, one of the assumptions in that proof is a surprise to a human implementing TLS 1.3, it isn't explicitly mentioned in the TLS 1.3 document as written. And so the result is, if you didn't obey that assumption, the proof doesn't hold and sure enough you're vulnerable to an attack. The assumption is for Pre-shared Keys (e.g. IoT devices A and B don't want to bother with certificates, so they just use pre-agreed random keys) each device pairing has its own PSK. A person looking at the design figures hey, got two devices Alice and Bob, I can just have a single key K known to both devices, and everything is secure. But that's wrong - and the TLS 1.3 proof doesn't say this will work. Here's what bad guys can do, it's called the Selfie Attack: Alice sends a message to Bob, maybe "Did you feed the cat?" and it's encrypted with key K. Normally Bob receives the message, maybe answers "Yes I fed the cat" also encrypted with key K and all is well. But now Mallory is on a network able to intercept and re-route messages. Alice sends to Bob, "Did you feed the cat?" encrypted with key K. Mallory can't read or tamper with this message, it's encrypted with key K and TLS 1.3 works as designed, but Mallory just re-directs the message back to Alice, "Did you feed the cat?". The message is encrypted with key K, Alice assumes Bob sent it, and replies "No, I didn't feed the cat" also encrypted with key K, which Mallory re-directs again back to Alice, who now mistakenly believes that Bob has told her he hasn't fed the cat. There are obviously a bunch of things you could do to fix this. First of all you could just have more PSKs. If Alice's message to Bob is always encrypted using the Alice->Bob shared key, when Alice actually receives it instead she knows something is wrong immediately. Or you could just prefix each message with To/From information, like an old-fashioned email and that works too so long as you check it. But the important observation is that this is an assumption in a proof that nobody really surfaced until it was too late. If researchers had told the proof system "No, the PSKs can be the same" the proof fails. Or if they'd carefully explained to the TLS Working Group, "We had to spell out that the PSKs must be different" then today RFC 8446 would likely explain that you need to do that or you've got a security problem. But neither happened and this attack slipped between the cracks.