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!
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.
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