0

I'm really in need of help with my thesis project. I'm currently finding the gap that my adviser is asking for and I seem to be having a hard time with it. What I could think of is actually creating a tool that reads smart contracts and see the flaws and vulnerabilities of the coded smart contract. Could someone explain to me if this is possible and if there are any references that you might want to share or also some ideas for my thesis project. Currently studying computer science btw! Thank you in advance!

  • There's a debugger made by the Truffle guys that you can check out – smatthewenglish Aug 26 '17 at 11:26
  • i think you ask about formal verification tools : look at ethereum.stackexchange.com/questions/11092/… – Badr Bellaj Aug 26 '17 at 11:53
  • I on the other hand think the "flaws and vulnerabilities" refer to known exploits and common contract mistakes. I do not think it is suitable topic for a thesis because a) it requires some experience with smart contracts and b) new exploits are emerging – comodoro Aug 26 '17 at 14:24
  • Also, even after formal verification, that only proves that the code does what the specification specifies. This does not prove that the specification does not have unintended consequences. It is probably impossible to prove that any program deployed in the real world has no unintended consequences. We can't even get laws written correctly and we've had millennia of trying to get that right. (Killing = bad. Except self-defence. Except self-defence using excessive force. Except self-defence using excessive force when under the heat of the moment fog-of-war/stress. Etc.) – lungj Aug 26 '17 at 16:27
1

In the fully general case, this is logically impossible, because it reduces to solving the "halting problem." (What education level is this "thesis" at? I'd expect any computer science researcher to be familiar with this fundamental principle of computability.)

You /can/ scan bytecode for particular behaviors, function calls, and so on, but as soon as any kind of indirection or user-supplied input is allowed, those scans end up being heuristics, rather than iron-clad proofs.

Another way to formulate that: It's totally possible to fully verify a program when all the inputs are known, and the program is not allowed to branch backwards in execution stream or use non-inlinable function calls (so, no possibility of recursion.) This, in turn, is vaguely related to why FORTRAN compilers were so great at optimizing. Once you scratch this topic for real, you'll find a wealth of interesting results stretching back to the dawn of von Neuman computing!

Delving into the area of "static program analysis" is probably going to be fruitful. There are lots of both theoretical and practical results in the field, although more of them are aimed towards finding buffer overflows in C code than trying to find whether a program "is bad."

The other question is how you define "bad" -- it's not clear to me that you can even come up with a stringent formal definition of what a "bad" program is, that would be both useful and non-trivial.

0

What you are alluding to is static program analysis. In general it's not possible to create a fully automated tool that can check for all vulnerabilities with perfect recall and precision.

Good tools for checking the presence of vulnerabilities do exist. For instance, https://contract-library.com performs security analyses for all smart contracts on the Ethereum mainnet and the testnets. Here's an example of a vulnerable contract: https://contract-library.com/contracts/Ethereum/0xb91824d10079a44864a9bec11b4ae022d7732e05

Some of the vulnerabilities it can catch are gas-related ones. Here is our paper which describes some of these analyses if you're interested in replicating/improving upon our results: https://www.nevillegrech.com/assets/pdf/madmax-oopsla18.pdf

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.