3 ms·

From what I understand of DAO and the Turing Complete capability of Ethereum, the fundamental "flaw" in smart contracts is not "more testing for bugs", nor "mor

by jasode 10y ago

From what I understand of DAO and the Turing Complete capability of Ethereum, the fundamental "flaw" in smart contracts is not "more testing for bugs", nor "more static analysis", nor "case insensitive syntax". Instead, the gap that will be always there is related to Rice's Theorem and/or Godel Incompleteness Theorem. E.g. you can't take the rules of a system and use it to prove its own consistency. The other concept that is relevant is the "limits of correctness."[1] Based on Godel Incompleteness & Limits of Correctness, you will always require an outer "context" to verify that the smart contract did what was intended. That outer "context" can't be the Ethereum code -- it has to be humans. Whether it's humans in "an open source council", or arbitrators, or courts. In a similar example with the NASDAQ crash in 2010, they cancelled some "bogus" trades.[2] NASDAQ is mostly automated by computers -- in fact, the "electronic trading" was its selling point over the NYSE. Even with NASDAQ's computer automation (this includes both the computer code inside NASDAQ and computer code of traders' computers) being a weaker form of "smart contracts", NASDAQ still has to have humans be the final judge of which trades were "correct". Is it possible to write a NASDAQ decision tree embedded in source code that will handle all errors thereby eliminating the need for any human intervention? I don't believe it's possible. The idea of "smart contract" source code being the final authority is an unattainable goal. The DAO/Ethereum had the "NASDAQ 2010 cancel trades" moment by forking the code. That decision to fork is the outer context of the "smart contract". In a sibling post, Animats writes, >"A declarative representation with guarantees is needed." A declarative syntax can reduce the bug count but it can't eliminate them and thereby remove humans from being ultimate judge of what is a "incorrect smart contract". For a similar example, consider the following super simple function: double convert_Celsius_to_Fahrenheit(double temperature) { return temperature * 9.0 / 5.0 + 32.0; } According the ideals of Functional Programming, that function is referentially transparent -- it does not reference global variables and just uses what's explicitly passed as a parameter. Also, the operations of multiplication, division, and addition are "well understood." There is no overflow flaw because a "double" datatype can handle all temperatures from Kelvin absolute zero -273 to Plank Temperature of 10^38. It doesn't have any gotos or jumps. It certainly looks like a "zero defect bug free" function. So... what could go wrong with that function that could make it not work the way humans intended? I leave that as an exercise for the reader. (Hint: read "Limits of Correctness".) [1]https://www.student.cs.uwaterloo.ca/~cs492/11public_html/p18-smith.pdf https://www.student.cs.uwaterloo.ca/~cs492/11public_html/p18... [2]http://money.cnn.com/2010/05/07/markets/explaining_wall_street_turmoil/ http://money.cnn.com/2010/05/07/markets/explaining_wall_stre...

nickpsecurity 10y ago
Thanks for the paper. Didn't have it. Just skimming it for now. "legal contracts, and other humanly interpretable specifications, are always stated within a background of common sense, to cover the myriad unstated and unstatable assumptions assumed to hold in force. (Current computer programs, alas, have no common sense, as the cartoonists know so well." (Smith) Most appropriate quote of the paper for purposes of this discussion. Human negotiators have common sense plus legal precedents (and lawyers) that guide the process to create sensible terms. They might argue over them later but the process works well enough. You'll rarely see something enormously simple and stupid happen. Whereas, computer programs, when asked, will happily divide by zero, overwrite their own system files, or make some prick investing in blockchains richer than deserved. They're idiotic. The part of INFOSEC dedicated to reducing impact of inherently risky and idiotic computers running arbitrary programs has been a miserable failure. The ones using constrained, predictable programs on less risky or idiotic HW/SW combos have a steady stream of good results. Especially in safety-critical industry. One trick is they, like legal contracts, are extra clear on the Why, What, and Where of their operation. The typically implicit assumptions are explicit enough to check with regular brains and smart tooling. Smart contracts will need this property as well. "consider the following super simple function:" That function isn't simple because it has floats. I've forgotten too much C to be sure of what the error is. I'm suspecting one or both of two: no sanity check on lower bounds of input value in Celcius, which might affect correctness; errata related to floating point math (esp rounding) which is not decimal math that we teach students to use for conversion functions & likely was in the mental spec developer had in their head. I avoided floating point wherever possible due to its weird issues. Was I close or what was the actual error?
- wolfgke 10y ago
  > You'll rarely see something enormously simple and stupid happen. Because our society trains all people in this area very deeply. If the society would mainly train people really deeply into mathematics and computer science instead, I believe the situation would be exactly opposite.
- pc2g4d 10y ago
  Lack of bounds check on the input was my first thought, too. Need to deal with NaN sanely, too, but usually that takes care of itself as it propagates through any operations.

by jasode 10y ago

nickpsecurity 10y ago

Thanks for the paper. Didn't have it. Just skimming it for now. "legal contracts, and other humanly interpretable specifications, are always stated within a background of common sense, to cover the myriad unstated and unstatable assumptions assumed to hold in force. (Current computer programs, alas, have no common sense, as the cartoonists know so well." (Smith) Most appropriate quote of the paper for purposes of this discussion. Human negotiators have common sense plus legal precedents (and lawyers) that guide the process to create sensible terms. They might argue over them later but the process works well enough. You'll rarely see something enormously simple and stupid happen. Whereas, computer programs, when asked, will happily divide by zero, overwrite their own system files, or make some prick investing in blockchains richer than deserved. They're idiotic. The part of INFOSEC dedicated to reducing impact of inherently risky and idiotic computers running arbitrary programs has been a miserable failure. The ones using constrained, predictable programs on less risky or idiotic HW/SW combos have a steady stream of good results. Especially in safety-critical industry. One trick is they, like legal contracts, are extra clear on the Why, What, and Where of their operation. The typically implicit assumptions are explicit enough to check with regular brains and smart tooling. Smart contracts will need this property as well. "consider the following super simple function:" That function isn't simple because it has floats. I've forgotten too much C to be sure of what the error is. I'm suspecting one or both of two: no sanity check on lower bounds of input value in Celcius, which might affect correctness; errata related to floating point math (esp rounding) which is not decimal math that we teach students to use for conversion functions & likely was in the mental spec developer had in their head. I avoided floating point wherever possible due to its weird issues. Was I close or what was the actual error?

wolfgke 10y ago
> You'll rarely see something enormously simple and stupid happen. Because our society trains all people in this area very deeply. If the society would mainly train people really deeply into mathematics and computer science instead, I believe the situation would be exactly opposite.
pc2g4d 10y ago
Lack of bounds check on the input was my first thought, too. Need to deal with NaN sanely, too, but usually that takes care of itself as it propagates through any operations.