Smart Contract modeling : comparison of techniques and concrete applications

A Smart Contract is an executable piece of code residing within a blockchain network. Users can interact with it and use it as an automatized third party, in order to ensure correct transactions. Once a Smart Contract has been deployed in the blockchain, its source code cannot technically be modified anymore. Unfortunately, users are able to interact with vulnerable contracts unconsciously and it may cost millions of dollars due to naive bugs leading to unexpected behaviours. A way to prevent those behaviours is by verifying Smart Contracts before their deployment. This master thesis approached this question by comparing three powerful techniques : Static analysis, Fuzzing and Model Checking. These techniques are able to verify several security properties on Smart Contracts. This work will focus on the comparison between those approaches, on the improvement of an existing analysis tool and finally on the detection of vulnerabilities in a real Smart Contract project named Wablieft.