5 ms·

This I don't understand about Ethereum. Just look at all the companies like Microsoft or Apple with millions to spare, or massive community efforts like Linux

This I don't understand about Ethereum. Just look at all the companies like Microsoft or Apple with millions to spare, or massive community efforts like Linux kernel, either with no shortage of means and resources to make their systems resistant to simple programming bugs. But history clearly shows that no amount of processes, audits, static analysis or eyepairs help: bugs just keep on being found where ever security folks look for them, and the harder they look, the more they find. Upside is, these systems can be patched, which is comforting as clearly there just is no bug-free code. Yet, people keep on pouring millions of dollars worth of virtual tokens to these experimental blockchain systems that are fundamentally designed so that any bug of certain class means the money is forever, irreversibly lost - as if these crypto contracts were some mythical new breed of software written by infallible Gods.

zanny 9y ago
This is why Rust is so promising. The problem at Apple / MS / Linux / etc is they are massive houses built on bare foundations. Everything traces its roots back to C, and back to exploitative vulnerabilities in the code. Rust itself is not close to safe since it depends on LLVM which itself can be a source of myriad bugs related to C++. But its proving in my experience to be a much more practical foundation, and going forward there is a lot of value in that.
- adambyrtek 9y ago
  Better languages can help to avoid certain classes of errors, but won't prevent bugs in the business logic of your code, so I'm not sure how this is relevant to contracts.
- bpicolo 9y ago
  Has there ever once been a critical llvm vulnerability? I've seen the occasional bugs related to it, but they tend to crash the compiler rather than produce bad binaries, no?
  - tom_mellior 9y ago
    Here's a list of LLVM bugs found using Csmith: http://embed.cs.utah.edu/csmith/llvm-bugs.html http://embed.cs.utah.edu/csmith/llvm-bugs.html . Plenty of these are wrong code bugs. Security-related compiler bugs very rare, but they do exist, at least in graphics shader compilers: http://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2017/OOPSLA.pdf http://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2017/OOPS... . My impression is that many of these shader compilers are based on LLVM, but this is mostly conjecture. (I do recall a video game crashing on me with internal LLVM errors from the graphics driver.)
- kornish 9y ago
  The bug in question isn't related to memory safety, overflow, or concurrency, though.
- steveklabnik 9y ago
  We do occasionally run into bugs between Rust and C++ semantics with LLVM, but they’ve been pretty minor, and LLVM has largely fixed them, to the point of adding instrinsincs to fix these issues. Bugs happen no matter the language, even if LLVM was in Rust it would have them.
- olliej 9y ago
  this isn't a code error -- it's a logic error. No amount of "safeness" in the language will save you from telling the language, without breaking the rules, from doing something that is "wrong". For instance: sudo rm -rf / Every part of that is completely sound and correct. There are no buffer overflows, emory corruption, or anything. You wrote a completely correct command to do something (probably) really wrong.
  - AstralStorm 9y ago
    This is preventable if you specify fully what you actually want to do. Then there are systems that just prevent ambiguous rules if you really dig into it. (Speaking of assisted theorem prover such as Coq and Isabelle.)
    - zaarn 9y ago
      >This is preventable if you specify fully what you actually want to do. In this case it was fully specified that sudo should run rm with all privileges, which in turn will recursively deleted the root filesystem. The entire execution is fully specified and will execute without fault. There is no mistake in `sudo rm -rf /`. Logical faults may not be preventable with provers, such as when underlying assumptions are wrong. For example, a prover could have verified the parity library as fully okay because it assumes that the initialization function will not be called without delegation. This underlying assumption X -!> Y (X cannot lead to Y) is wrong and X -> Y is the case but the prover only verified that Y -!> X. Provers essentially duplicate your code, forcing you to express the solution and/or problem twice such that if you basically typo on the way, one of the pieces will complain about the other. But it cannot and is incapable of preventing higher level mistakes.
DennisP 9y ago
The saving grace of Ethereum contracts is that they're very short. Many are under a thousand lines of code, so it's not crazy expensive to pay expert auditors to review every line. It also looks like an ideal use of formal verification techniques, and there's a lot of work going into making that practical. Plus you can keep things a lot safer by writing your contracts in the simplest, most obviously-correct way possible. The fact that you can do these things doesn't save you from people who don't. Parity's last audit happened before they made a major architectural change; if they'd gotten new audits this probably would have been caught. They also have the most complex wallet code I've seen, often dipping into assembly. It's true that you can't be completely sure of avoiding bugs, but with decent practices I think it's less of a problem on Ethereum that it is in medical equipment, airliners, and nuclear reactors.
- mbrock 9y ago
  It's kind of like, do you think it's humanly possible to correctly encode the rules of chess in, say, 6502 assembly? You probably won't do it on the first try. And you wouldn't immediately bet a million dollar on it. But is it possible? Yes. A multisig wallet shouldn't be more complicated. Could you prove the correctness of the 6502 chess? Sure. Formal methods are not black magic. You need a semantics of the machine and a formalization of the rules. Can you make mistakes in specifying? Yeah, duh. So combine it with peer review and throw in a bug bounty and fuzzing.
  - schoen 9y ago
    Chess is a nice example in this analogy because there are rules that people are less familiar with and might well forget about or implement incorrectly. For example, the complete castling rules are not trivial, like with the king not passing through a square currently attacked by an opposing piece https://en.wikipedia.org/wiki/Castling#Requirements https://en.wikipedia.org/wiki/Castling#Requirements and some people may neglect or misimplement en passant https://en.wikipedia.org/wiki/En_passant https://en.wikipedia.org/wiki/En_passant and the rules related to repetitive situations in the end game: https://en.wikipedia.org/wiki/Threefold_repetition https://en.wikipedia.org/wiki/Threefold_repetition https://en.wikipedia.org/wiki/Fifty-move_rule https://en.wikipedia.org/wiki/Fifty-move_rule (Implementing the threefold repetition rule requires maintaining historical state of a different kind than any other chess rule!) I've seen impressive hyperminimalist chess implementations that were missing these things, but that totally felt like real chess almost all of the time.
trhway 9y ago
Bugs almost always mean lost money. In block chains it is just more direct and visible.
AstralStorm 9y ago
There is a way, reforming everything as an automatic math proof. Because even security is driven by capitalism sort term gains almost nobody does this. It takes time and sometimes serious math skills.

zanny 9y ago

This is why Rust is so promising. The problem at Apple / MS / Linux / etc is they are massive houses built on bare foundations. Everything traces its roots back to C, and back to exploitative vulnerabilities in the code. Rust itself is not close to safe since it depends on LLVM which itself can be a source of myriad bugs related to C++. But its proving in my experience to be a much more practical foundation, and going forward there is a lot of value in that.

adambyrtek 9y ago
Better languages can help to avoid certain classes of errors, but won't prevent bugs in the business logic of your code, so I'm not sure how this is relevant to contracts.
bpicolo 9y ago
Has there ever once been a critical llvm vulnerability? I've seen the occasional bugs related to it, but they tend to crash the compiler rather than produce bad binaries, no?
- tom_mellior 9y ago
  Here's a list of LLVM bugs found using Csmith: http://embed.cs.utah.edu/csmith/llvm-bugs.html http://embed.cs.utah.edu/csmith/llvm-bugs.html . Plenty of these are wrong code bugs. Security-related compiler bugs very rare, but they do exist, at least in graphics shader compilers: http://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2017/OOPSLA.pdf http://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2017/OOPS... . My impression is that many of these shader compilers are based on LLVM, but this is mostly conjecture. (I do recall a video game crashing on me with internal LLVM errors from the graphics driver.)
kornish 9y ago
The bug in question isn't related to memory safety, overflow, or concurrency, though.
steveklabnik 9y ago
We do occasionally run into bugs between Rust and C++ semantics with LLVM, but they’ve been pretty minor, and LLVM has largely fixed them, to the point of adding instrinsincs to fix these issues. Bugs happen no matter the language, even if LLVM was in Rust it would have them.
olliej 9y ago
this isn't a code error -- it's a logic error. No amount of "safeness" in the language will save you from telling the language, without breaking the rules, from doing something that is "wrong". For instance: sudo rm -rf / Every part of that is completely sound and correct. There are no buffer overflows, emory corruption, or anything. You wrote a completely correct command to do something (probably) really wrong.
- AstralStorm 9y ago
  This is preventable if you specify fully what you actually want to do. Then there are systems that just prevent ambiguous rules if you really dig into it. (Speaking of assisted theorem prover such as Coq and Isabelle.)
  - zaarn 9y ago
    >This is preventable if you specify fully what you actually want to do. In this case it was fully specified that sudo should run rm with all privileges, which in turn will recursively deleted the root filesystem. The entire execution is fully specified and will execute without fault. There is no mistake in `sudo rm -rf /`. Logical faults may not be preventable with provers, such as when underlying assumptions are wrong. For example, a prover could have verified the parity library as fully okay because it assumes that the initialization function will not be called without delegation. This underlying assumption X -!> Y (X cannot lead to Y) is wrong and X -> Y is the case but the prover only verified that Y -!> X. Provers essentially duplicate your code, forcing you to express the solution and/or problem twice such that if you basically typo on the way, one of the pieces will complain about the other. But it cannot and is incapable of preventing higher level mistakes.

DennisP 9y ago

The saving grace of Ethereum contracts is that they're very short. Many are under a thousand lines of code, so it's not crazy expensive to pay expert auditors to review every line. It also looks like an ideal use of formal verification techniques, and there's a lot of work going into making that practical. Plus you can keep things a lot safer by writing your contracts in the simplest, most obviously-correct way possible. The fact that you can do these things doesn't save you from people who don't. Parity's last audit happened before they made a major architectural change; if they'd gotten new audits this probably would have been caught. They also have the most complex wallet code I've seen, often dipping into assembly. It's true that you can't be completely sure of avoiding bugs, but with decent practices I think it's less of a problem on Ethereum that it is in medical equipment, airliners, and nuclear reactors.

mbrock 9y ago
It's kind of like, do you think it's humanly possible to correctly encode the rules of chess in, say, 6502 assembly? You probably won't do it on the first try. And you wouldn't immediately bet a million dollar on it. But is it possible? Yes. A multisig wallet shouldn't be more complicated. Could you prove the correctness of the 6502 chess? Sure. Formal methods are not black magic. You need a semantics of the machine and a formalization of the rules. Can you make mistakes in specifying? Yeah, duh. So combine it with peer review and throw in a bug bounty and fuzzing.
- schoen 9y ago
  Chess is a nice example in this analogy because there are rules that people are less familiar with and might well forget about or implement incorrectly. For example, the complete castling rules are not trivial, like with the king not passing through a square currently attacked by an opposing piece https://en.wikipedia.org/wiki/Castling#Requirements https://en.wikipedia.org/wiki/Castling#Requirements and some people may neglect or misimplement en passant https://en.wikipedia.org/wiki/En_passant https://en.wikipedia.org/wiki/En_passant and the rules related to repetitive situations in the end game: https://en.wikipedia.org/wiki/Threefold_repetition https://en.wikipedia.org/wiki/Threefold_repetition https://en.wikipedia.org/wiki/Fifty-move_rule https://en.wikipedia.org/wiki/Fifty-move_rule (Implementing the threefold repetition rule requires maintaining historical state of a different kind than any other chess rule!) I've seen impressive hyperminimalist chess implementations that were missing these things, but that totally felt like real chess almost all of the time.

trhway 9y ago

Bugs almost always mean lost money. In block chains it is just more direct and visible.

AstralStorm 9y ago

There is a way, reforming everything as an automatic math proof. Because even security is driven by capitalism sort term gains almost nobody does this. It takes time and sometimes serious math skills.