On reentrency bugs in Ethereum smart contracts part 1
In my previous post on this topic "Basic Model Theory and Input Validation" I mentioned the value of input validation and formal verification for smart contracts. I realize I did not go far enough in that post and my conclusion as a result was inadequate. The bug in The DAO is known as a reentrency bug which means in plain English that the smart contract or a subroutine within it is interrupted in the middle of it's execution. In the case of The DAO this interruption resulted in an unintended and unexpected behavior.
Verification is one aspect of testing a product's fitness for purpose. Validation is the complementary aspect. Often one refers to the overall checking process as V & V.
Validation: "Are we trying to make the right thing?", i.e., is the product specified to the user's actual needs?
Verification: "Have we made what we were trying to make?", i.e., does the product conform to the specifications?
The verification process consists of static/structural and dynamic/behavioral aspects. E.g., for a software product one can inspect the source code (static) and run against specific test cases (dynamic). Validation usually can be done only dynamically, i.e., the product is tested by putting it through typical and atypical usages ("Does it satisfactorily meet all use cases?").
How could this have been prevented? Well for one the ability to know what the smart contract will do would remove reentrency bugs. Reentrency can in specifically be prevented if you can be reasonably certain about what the smart contract is doing and apply the techniques of formal verification, type checking, and general correctness of the smart contract to prevent all reentrency by default.
In order to make smart contracts safe we must move toward mandatory formal verification. This formal verification must include the compiler itself if we are to trust that. The compiler also by default should start in safe mode to block common programmer errors from passing type check.
Evaluation Despite the limitations of our tool (in particular,
it doesn’t support many syntactic features of Solidity),
we are able to translate and typecheck 46 out of the 396
contracts we collected on https://etherscan.io. Out of
these, only a handful are valid in the Eth effect. This is a
clear sign that a large scale analysis of published contract is
likely to uncover widespread vulnerabilities; we leave such
analysis to future work.
References
This post has been ranked within the top 50 most undervalued posts in the first half of Feb 21. We estimate that this post is undervalued by $3.20 as compared to a scenario in which every voter had an equal say.
See the full rankings and details in The Daily Tribune: Feb 21 - Part I. You can also read about some of our methodology, data analysis and technical details in our initial post.
If you are the author and would prefer not to receive these comments, simply reply "Stop" to this comment.