Table 5: Tested Smart Contracts from Ethereum Blockchain
Name Balance Tx Ins Block Cycle
MoonCatRescue 6.08960513010001 6647 8650 458 Y
CryptoPunksMarket 212.510667068223383179 18296 6441 321 N
SafeMathLibExt 0 1 387 32 N
PromissoryToken 1.131884071130000015 359 7642 438 Y
DigiPulse 100.633469345624563517 1559 1856 140 Y
PreTgeExperty 406.607596164599999 176 2537 161 Y
ProtectTheCastle 0.0141 17 2496 166 Y
NoFeePonzi 4.9886 31 842 79 N
NamiMarket 2.23225700000000001 54 5039 338 Y
PonzICO 3.266396182497500183 86 1290 81 N
MultiplyX10 3.00001 3 1234 103 Y
EthergotchiOwnershipV2 0 380 828 56 N
Ownable 0 1 80 8 N
QuizTime 2.011800000727 29 1186 71 N
Dragon 0.004030007539536001 35 5584 421 Y
PublicSaleManager 22.755499999999999 48 2505 181 Y
Insurance 0.354711104826512158 2 1820 1320 N
DiceRoll 0.507739999999513218 8 11809 714 Y
XPS 0 465 2313 128 N
MultiMerkleMine 0 143 1653 113 Y
verified smart contract is high. Further observation, those highly similar smart contract is an updated version of the same source. Considering this circumstance, we treated those smart contract as the same source.
5.3 Compile Result
After doing the comparison, total numbers of unique smart contract we had downloaded are 292. Compiling those source code, we encounter several situations such as semantic error or uncompilable source code which the code is an interface or library rather than a callable smart contract we want. In the end, we use our analysis tool to test total twenty successfully compiled smart contracts. Among those smart contract, half of them contained at least one cycle path inside the control flow graph. The information such the balance of the smart contract, total transactions, instructions in the smart contract, and blocks in the control flow graph of the cycle path for those smart contract all list in table
‧
國立 政 治 大 學
‧
N a tio na
l C h engchi U ni ve rs it y
5. Although some of the smart contract contained cycle path, no positive cycle was found In those twenty on-chain smart contracts. But we generate the path constraints for the cycle path.
(size(calldata) < 4) == 0 ∧ (146CA531 = (F F F F F F F F &(P arameter/10000000...))) == 0 ∧ (3BCF 7D22 = (F F F F F F F F &(P arameter/10000000...))) == 0 ∧ (4316ABBB = (F F F F F F F F &(P arameter/10000000...))) == 0 ∧ (7E32A592 = (F F F F F F F F &(P arameter/10000000...))) == 0 ∧ (94181D27 = (F F F F F F F F &(P arameter/10000000...))) == 0 ∧ (9C8A5A56 = (F F F F F F F F &(P arameter/10000000...))) == 0 ∧ (A2E7241C = (F F F F F F F F &(P arameter/10000000...))) == 0 ∧ (B7D5D4C0 = (F F F F F F F F &(P arameter/10000000...))) == 0 ∧ (BD7B09E4 = (F F F F F F F F &(P arameter/10000000...))) == 0 ∧ (D466A03F = (F F F F F F F F &(P arameter/10000000...))) == 0 ∧ (D4D5D32A = (F F F F F F F F &(P arameter/10000000...))) == 0 ∧ (D94395E2 = (F F F F F F F F &(P arameter/10000000...))) == 0 ∧ (D954CBCB = (F F F F F F F F &(P arameter/10000000...))) == 0 ∧ (E2202A4D = (F F F F F F F F &(P arameter/10000000...))) == 0 ∧ (E684AA5C = (F F F F F F F F &(P arameter/10000000...))) == 0 ∧ (E811F 50A = (F F F F F F F F &(P arameter/10000000...))) == 1 ∧
(14)
Above equations are the path constraints for example P rotectT heCastle. If all the con-straints are feasible, the cycle path will be executed and it will consume 435 gas. To solve those constraints, we have to change the format of the constraint to match to rules for SMT solver. Let SMT solver to find out the possible answer for those symbolic parame-ters. With the answer, we will know if this cycle path is feasible or not.
‧
Table 6: Tested Smart Contracts from III
Name Ins Block Gas
We also run our analysis tool on some smart contract provided by III. There are total six source code being tested and only contract purchaseOrder contained a non-positive cycle. The result is show in table 6. Equation 15 show all the path constraints we generated for this path. If all the constraints are feasible, executing this path will consume massive gas.
On the other hand, we calculate the possible maximum gas consumption for each source code we tested from Ethereum blockchain (table 7). None of the results contained the symbolic gas constraint. All the gas consumption are a constant number. We will continue using our tool to verified those untested smart contracts on the blockchain.
6 Conclusions and Future Work
We have presented our approach to the vulnerability detection of Ethereum smart con-tracts at the level of EVM source code. We demonstrate a smart contract checking model that check EVM stack size and gas consumption. Also we generate an execution path of source code to determine whether the gas consumption of this path exceed the gas limit of
‧
Table 7: Maximum Gas Consumption for Smart Contracts from Ethereum Blockchain
Name Gas PC
‧
blockchain. That give the information of gas usage before executing the smart contract.
Not only prevent the situation of wasting Ether when exception happened, but provide a reference of estimated cost to smart contract user.
Recently, our model can only simulate a single smart contract status. Like other program, Ethereum smart contract is able to communicate with other callable smart contract. So for more comprehensive analysis, we hope to trace the interaction between different contract. That means, as in the future, we want to know the stack status or gas usage when a smart contract involve another smart contract. Either simultaneously checking both smart contracts or our model should be able to deal with message call inside a smart contract.
Furthermore, the main focus for theoretical contributions, where we shift our focus to model checking techniques after having dependency graphs or path constraints. Specif-ically, we will investigate automata-based numeric and string constraint solving as the fundamental solving techniques for vulnerability detection in target applications. The solver aims at solving a core string constraint language for numeric and string constraints that are commonly generated in the target applications during program analysis.
After vulnerabilities have been found, the next question is how to exploit the vulner-ability and how to patch the vulnervulner-ability. For side channel attacks, an ideal attack is to optimize information leakage after each try. As to reduce the risk, one should write the program in a way that has minimal information leakage (which can be quantified with our approach). On the other hand, with symbolic execution, the truth assignment of path conditions also reveals a feasible input to access the program point. The patch of the vulnerability is to restrict the condition so that it becomes infeasible when violation occurs.
References
[1] P. Dai, N. Mahi, J. Earls, and A. Norta, “Smart-contract value-transfer protocols on a distributed mobile application platform,” URL: https://qtum.
org/uploads/-‧
國立 政 治 大 學
‧
N a tio na
l C h engchi U ni ve rs it y
files/cf6d69348ca50dd985b60425ccf282f3. pdf, 2017.
[2] “Solidity-solidity 0.4.21 documentation.” https://solidity.readthedocs.io/en/
develop/.
[3] “Counterparty.” https://counterparty.io/.
[4] “Stellar - develop the world’s new financial system.” https://www.stellar.org/.
[5] “Home — lisk.” https://lisk.io/.
[6] “The dao (organization) - wikipedia.” https://en.wikipedia.org/wiki/The_DAO_
(organization).
[7] N. Atzei, M. Bartoletti, and T. Cimoli, “A survey of attacks on ethereum smart contracts (sok),” in International Conference on Principles of Security and Trust, pp. 164–186, Springer, 2017.
[8] “coloredcoins.org.” http://coloredcoins.org/.
[9] “Create a democracy contract in ethereum.” https://www.ethereum.org/dao.
[10] “Monegraph.” https://monegraph.com/.
[11] K. Delmolino, M. Arnett, A. Kosba, A. Miller, and E. Shi, “Step by step towards creating a safe smart contract: Lessons and insights from a cryptocurrency lab,” in International Conference on Financial Cryptography and Data Security, pp. 79–94, Springer, 2016.
[12] T. Dickerson, P. Gazzillo, M. Herlihy, and E. Koskinen, “Adding concurrency to smart contracts,” in Proceedings of the ACM Symposium on Principles of Distributed Computing, pp. 303–312, ACM, 2017.
[13] M. Herlihy, V. Luchangco, M. Moir, and W. N. Scherer III, “Software transactional memory for dynamic-sized data structures,” in Proceedings of the twenty-second an-nual symposium on Principles of distributed computing, pp. 92–101, ACM, 2003.
‧
國立 政 治 大 學
‧
N a tio na
l C h engchi U ni ve rs it y
[14] L. Luu, D.-H. Chu, H. Olickel, P. Saxena, and A. Hobor, “Making smart contracts smarter,” in Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, pp. 254–269, ACM, 2016.
[15] “Oyente by oyente.” https://oyente.github.io/benchmarks/.
[16] K. Bhargavan, A. Delignat-Lavaud, C. Fournet, A. Gollamudi, G. Gonthier, N. Kobeissi, N. Kulatova, A. Rastogi, T. Sibut-Pinote, N. Swamy, et al., “Formal ver-ification of smart contracts: Short paper,” in Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, pp. 91–96, ACM, 2016.
[17] N. Swamy, C. Hrit¸cu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest, K. Bhar-gavan, C. Fournet, P.-Y. Strub, M. Kohlweiss, et al., “Dependent types and multi-monadic effects in f,” in ACM SIGPLAN Notices, vol. 51, pp. 256–270, ACM, 2016.
[18] A. Dika, “Ethereum smart contracts: Security vulnerabilities and security tools,”
Master’s thesis, NTNU, 2017.
[19] “Securify - formal verification of ethereum smart contracts.” https://securify.ch/.
[20] “Smartdec — smart contracts security audit.” http://smartcontracts.smartdec.
net/.
[21] M. Suiche, “Porosity: A decompiler for blockchain-based smart contracts bytecode,”
DEF CON, vol. 25, 2017.
[22] E. Hildenbrandt, M. Saxena, X. Zhu, N. Rodrigues, P. Daian, D. Guth, and G. Rosu,
“Kevm: A complete semantics of the ethereum virtual machine,” tech. rep., 2017.
[23] S. Amani, M. B´egel, M. Bortin, and M. Staples, “Towards verifying ethereum smart contract bytecode in isabelle/hol,” CPP. ACM. To appear, 2018.
[24] A. Mavridou and A. Laszka, “Tool demonstration: Fsolidm for designing secure ethereum smart contracts,”
‧
國立 政 治 大 學
‧
N a tio na
l C h engchi U ni ve rs it y
[25] “Finite-state machine - wikipedia.” https://en.wikipedia.org/wiki/
Finite-state_machine.
[26] “Nxt - the blockchain application platform.” https://nxtplatform.org/.
[27] P. L. Seijas, S. J. Thompson, and D. McAdams, “Scripting smart contracts for dis-tributed ledger technology.,” IACR Cryptology ePrint Archive, vol. 2016, p. 1156, 2016.
[28] “Zero-knowledge proof - wikipedia.” https://en.wikipedia.org/wiki/
Zero-knowledge_proof.
[29] “Proof-carrying code - wikipedia.” https://en.wikipedia.org/wiki/
Proof-carrying_code.
[30] J. Rubin, M. Naik, and N. Subramanian, “Merkelized abstract syntax trees.”
[31] “Ethereum network status.” https://ethstats.net/.
[32] “Ethereum blockchain explorer and search.” https://etherscan.io/.
[33] “Installing the solidity compiler — solidity 0.4.21 documentation.” http://
solidity.readthedocs.io/en/v0.4.21/installing-solidity.html.
[34] “Remix - solidity ide.” https://remix.ethereum.org/#optimize=false&version=
builtin.
[35] “Graphviz - graph visualization software.” https://www.graphviz.org/.