DAO Model Sample Clauses

DAO Model. ‌ The DAO contracts implemented a crowd-funding platform, which raised ap- proximately $150 million before being attacked in June 2016. Here, we present a simplified version of the DAO contract, which allows participants to donate ether to fund contracts, while contracts can then withdraw their funds. The augmented model of the contract is presented in Figure 10. By verifying the safety property presented in Table 1, we can guarantee that none of the two attacks presented in [2] can be successful on our contract. Both of these attacks are possible if the contract sends the amount of ether before decreasing the credit and in the meantime an attacker makes another function call, e.g., to withdraw. Although the former is true for our transition system, i.e., transition 6 happens after transition 5, by-design our contract changes state when the withdraw function is called. In particular, our contract goes from the Initial state to the withdraw state and thus, after executing transition 5, the attacker cannot make another function call. In other words, 6 will always happen right after the execution of 5.