The author found that some of the transaction-related loopholes were due to a mismatch between the actual transfer amount and the amount reflected in the internal bookkeeping of the contract.

The VULTRON can detect irregular transactions due to various types of adversarial exploits.

There are a lot of attempts to detect vulnerabilities in smart contracts, but these techniques follow a case-by-case approach: analyzing contract procedures and matching previously observed attack patterns. Therefore, the accuracy and recall rate of these technologies depends on the degree of pattern specificity and the synthesis of the pattern set.

ContractFuzzer proposes seven specific patterns observed in the contract procedure to detect seven vulnerabilities. Because the patterns collected are limited and they are syntacticly modeled, the analysis has both false positives and false positives.

For example, a pattern used to detect inconsistencies in exception handling, called exception out-of-order, checks only if functions in the nested call chain throw exceptions. If the root function does not throw an exception, but subsequent calls throw an exception, this is considered a vulnerability. If all exceptions are handled correctly on the call chain, a false positive is generated.

Oyente describes previously known vulnerabilities as in-process properties, and then uses symbol execution to verify those properties.

Zeus relies on model checks to release properties from previously known vulnerabilities and user-specific policies.

Securify performs domain-specific validation of smart contracts. Again, it assumes that a domain pattern for a specific type of vulnerability is provided in advance.

Almost all the existing vulnerability patterns (defined at the syntactic-level) can be traced back (semantically) to the mismatch between the actual transferred amount in a transaction and the amount reflected on the contract’s internal bookkeeping.

Based on this, this paper proposes "VULTRON", a precise and general smart contract vulnerability detection technique, which allows to drill down to the very root of the problem.

The essence of VULTRON is to build an oracle that can effectively distinguish irregular transactions (usually results of malicious exploits) from normal ones. this oracle is general enough to cover the previously reported vulnerabilities without the limitation of any particular smart contract programming language or blockchain technology.

This approach can be easily adapted and implemented on other platforms. The proposed oracle improves and enables a wide spectrum of downstream analysis techniques, including static analysis such as symbolic execution [1], program verification [5], and dynamic techniques (e.g., testing and fuzzing [3], [7]).

Vulnerabilities in smart contracts are usually caused by inconsistencies between the implementations and the intended semantics [5]. Transaction-related vulnerabilities can be (most of them have already been) exploited to carry out attacks, e.g., stealing funds from vulnerable contracts.

contract model

in Ethereum’s case, each contract has a contract balance (bal) representing the total amount of funds remaining in the contract, which is out of the contract program’s control.

contracts managing shared assets also need to keep track of participants’ individual account balances, called the bookkeeping balances. Contract programs uses an internal bookkeeping variable (e.g., balances in Fig. 1), which is modeled as M, to record the bookkeeping balances.

Two contracts, SimpleDAO (the victim, in Fig. 1) and Attacker (in Fig. 2), are deployed on the blockchain. The reentrancy vulnerability of SimpleDAO can be exploited by Attacker as follows. (1) Attacker invokes the donate function of SimpleDAO to donate 1 wei, and the balance of SimpleDAO is increased by 1 wei automatically and implicitly. Then, the bookkeeping balance of Attacker is increased by 1 wei accordingly (Line 4). (2) Attacker invokes the withdraw function to withdraw 1 wei. The withdraw function first checks whether the bookkeeping balance of Attacker is sufficient (Line 7), and then transfers 1 wei to Attacker (Line 8). Due to the fallback function mechanism, since Attacker receives money, its fallback function (the one with no name at Lines 4 ′ –6 ′ ) will be triggered, and it invokes the withdraw function of SimpleDAO to withdraw money again. Note that balances update at Line 9 is still not executed. (3) The withdraw function is reentered before the bookkeeping balance of Attacker is updated correctly in its first invocation (Line 9). Thus, in the second invocation, the condition checking at Line 7 still passes, which is not supposed to happen, and the money transfer at Line 8 proceeds, which is not supposed to happen as well. This behavior recursively draws out all the money in SimpleDAO.

The proposed balance invariant, formulated in Definition 1, can help detect the reentrancy attack. Suppose, initially, the balance of SimpleDAO is 10, and the bookkeeping balances of all participants are initialized to zero. Thus, the difference K is 10. After the attack step (1), K is still 10 because the SimpleDAO’s balance is increased by 1, so as the bookkeeping balance of Attacker. After the attack step (2), the balance invariant is violated because the SimpleDAO’s balance is decreased by 1, but the bookkeeping balance of Attacker does not change, i.e., the difference K becomes 9. Once the proposed balance invariant is violated, we can conclude that the contract is vulnerable.

Exception Disorder. The issue of exception disorder is due to inconsistencies in exception handling. In Solidity, exceptions may be raised in several situations, e.g., the execution runs out of gas, the command throw is executed, etc. However, Solidity is not uniform in handling exceptions. Within a chain of nested calls, there could be two types of exception handling mechanisms [15]: (1) If all the functions in the chain are direct calls, the execution stops and all side effects are reverted, including transfers of Ether. (2) If a function in the chain is a call (the same for delegatecall and send), the exception is propagated along the chain, reverting all side effects, until it reaches the call. From that point on, the execution is resumed with call returning false.

Programmers not familiar with the exception mechanism may handle exceptions incorrectly. The transaction invariant, as formulated in Definition 2, can help detect the exception disorder vulnerability. For example, Fig. 3 is a simplified version of “King of Ether Throne”, where Line 8 may cause an exception disorder. In this example, there is no bookkeeping variable and hence we insert a ghost variable into the contract. If the return value (Line 8) is used as a branch condition of a if-statement, we update the ghost variable in its True branch. Otherwise, we update the ghost variable immediately after Line 8. Suppose KotET attempts to transfer 10 wei to an account r and this transfer fails. The ghost variable (i.e., M(KotET)) is deducted by 10, but r.bal is not increased, which violates the transaction invariant.

Smart contracts are mainly used to manage the transfer of assets and perform bookkeeping [10].

given that the majority of smart contracts share specific data structures and underlying business logic, it is possible to come up with common invariants for them, whereas this is not possible to do for general-purpose computer programs.

More specifically, the reasonable smart contracts usually satisfy the following two invariants for their transactions.

1. The balance invariant requires that the difference between the contract balance and the sum of all participants’ bookkeeping balances remain constant, before and after a transaction. This invariant is defined within a single contract, i.e., intracontract, and it ensures the integrity of the bookkeeping balances. If the bookkeeping balances are not updated correctly after a transaction (which violates the balance invariant), then it indicates that an irregular event has happened during that transaction. For example, when an underflow happens during an outgoing transaction, the contract balance naturally goes down while the bookkeeping balances go up instead.

the consistency of incoming transactions can be guaranteed by the balance invariant or other contract’s outgoing transaction invariant. In some cases, a transaction may fail in the middle and funds are not transferred, but it may not be captured by the contract’s bookkeeping variables, resulting in a vulnerability.

2.the consistency of incoming transactions can be guaranteed by the balance invariant or other contract’s outgoing transaction invariant. In some cases, a transaction may fail in the middle and funds are not transferred, but it may not be captured by the contract’s bookkeeping variables, resulting in a vulnerability.

Identifying Bookkeeping Variables.

Almost all contracts performing meaningful transactions among multiple parties contain such a variable, usually coming with the name balances or balanceOf.

Some contracts do not have bookkeeping variables, e.g., King of the Ether [11]. In these cases, a ghost variable and its corresponding updates can be inserted by our analysis. The bookkeeping variable can either be given by the user as an input to our approach or be automatically identified using taint analysis [12].

最开始先执行几个常规的transactions, 观察contract中的所有全局变量是如何变化的，找到一个始终与之相匹配的变量和逻辑。

Handling Non-Currency Assets.

The bookkeeping balances of some contracts may not refer to the crypto-currency directly. This is often the case in ERC20-compliant contracts. In these contracts, participants’ digital assets are reflected in terms of the number of available tokens rather than Ether. These noncurrency assets can be converted to Ether by multiplying with their prices. The current price of the said assets is stored in some location (e.g., the variable price), which can be identified with similar techniques used for locating bookkeeping variables.

Verifying Invariants.

The invariants are then translated to program assertions and then be verified either statically or dynamically. The gas consumption of a transaction should also be taken into account in the translation, which is not included in our contract model and invariants. The assertions can be inserted into the compiled Ethereum Virtual Machine (EVM) bytecode, at the end of every function, which can then be checked by existing verification tools [2], [5]. Alternatively, we can instrument the EVM itself to enforce the invariants at runtime. This will prevent irregular transactions from happening even if the deployed contract programs are vulnerable.

This is again attributed to the particular way how smart contracts work – they do not crash and the execution may be silently reverted in cases of irregularities.

REFERENCES

[1] J. Chang, B. Gao, H. Xiao, J. Sun, and Z. Yang, “sCompile: Critical path identification and analysis for smart contracts,” arXiv, 2018.

[2] P. Tsankov, A. Dan, D. D. Cohen, A. Gervais, F. Buenzli, and M. Vechev, “Securify: Practical security analysis of smart contracts,” in CCS, 2018.

[3] B. Jiang, Y. Liu, and W. Chan, “ContractFuzzer: fuzzing smart contracts for vulnerability detection,” in ASE, 2018, pp. 259–269.

[4] L. Luu, D.-H. Chu, H. Olickel, P. Saxena, and A. Hobor, “Making smart contracts smarter,” in CCS, 2016.

[5] S. Kalra, S. Goel, M. Dhawan, and S. Sharma, “Zeus: Analyzing safety of smart contracts,” in NDSS, 2018.

[6] I. Nikolic, A. Kolluri, I. Sergey, P. Saxena, and A. Hobor, “Finding the greedy, prodigal, and suicidal contracts at scale,” arXiv, 2018.

[7] C. Liu, H. Liu, Z. Cao, Z. Chen, B. Chen, and B. Roscoe, “ReGuard:

finding reentrancy bugs in smart contracts,” in ICSE, 2018.

[8] “Ethereum project,” https://www.ethereum.org/, accessed 2018.

[9] “Solidity,” https://solidity.readthedocs.io/en/v0.4.25/, accessed 2018.

[10] K. Chatterjee, A. K. Goharshady, and Y. Velner, “Quantitative analysis of smart contracts,” in European Symposium on Programming, 2018.

[11] “King of the Ether,” https://github.com/kieranelby/KingOfTheEtherThrone/, accessed 2018.

[12] M. G. Kang, S. McCamant, P. Poosankam, and D. Song, “Dta++: dynamic taint analysis with targeted control-flow propagation.” in NDSS, 2011.

[13] “Truffle Suite,” https://truffleframework.com/, accessed 2018.

[14] “Underflow example,” http://www.dasp.co/, accessed 2018.

[15] N. Atzei, M. Bartoletti, and T. Cimoli, “A survey of attacks on Ethereum smart contracts (sok),” in Principles of Security and Trust, 2017.

[16] Y. Xiong, X. Liu, M. Zeng, L. Zhang, and G. Huang, “Identifying patch correctness in test-based program repair,” in ICSE, 2018.

[A statement that the right to interpret all content and copyright belongs to the original author of the paper, this note is used only for learning.]