  Smart contracts are distributed, self-enforcing programs executing on top of
blockchain networks. They have the potential to revolutionize many industries
such as financial institutes and supply chains. However, smart contracts are
subject to code-based vulnerabilities, which casts a shadow on its
applications. As smart contracts are unpatchable (due to the immutability of
blockchain), it is essential that smart contracts are guaranteed to be free of
vulnerabilities. Unfortunately, smart contract languages such as Solidity are
Turing-complete, which implies that verifying them statically is infeasible.
Thus, alternative approaches must be developed to provide the guarantee. In
this work, we develop an approach which automatically transforms smart
contracts so that they are provably free of 4 common kinds of vulnerabilities.
The key idea is to apply runtime verification in an efficient and provably
correct manner. Experiment results with 5000 smart contracts show that our
approach incurs minor run-time overhead in terms of time (i.e., 14.79%) and gas
(i.e., 0.79%).
