 |
As the blockchain technology develops, the field of application of smart contracts has expanded.
However, if there is a problem with the security vulnerability of the smart contract and the contradictions and errors of the smart contract itself, it has a characteristic that cannot be corrected once it is deployed, which can lead to a fatal accident soon.
One of the most well-known cases of damage, DAO ATTACK, one of the functions of DAO was to participate in crowdsale of investors and get Ether refunded. During the process of this function, there was a flaw in the logic of coding.
Therefore, it was a case in which 3.6 million ETH was stolen by repeatedly requesting a refund. In addition, there are PARITY WALLET hacking and SMART MESH hacking.
Therefore, in this paper, we intend to verify the smart contract through formal modeling, one of the formal specifications, before deploying the smart contract.
|
IEEE/ICACT20210216 Slide.06
[Big Slide]