WIXLIB

SmartCheck: Static Analysis of Ethereum Smart Contracts2.1.4 send instead of transfer. The recommended way to perform ether payments is addr.transfer(x), which automaticallythrows an exception if the transfer is unsuccessful, preventing theproblem described in Section 2.1.2. The pattern detects the sendkeyword.2.1.5Re-entrancy. Consider the following code:pragma solidity 0.4.19;contract Fund {mapping ( address uint ) balances ;function withdraw () public {if ( msg . sender . call . value ( balances [ msg . sender ]) () )balances [ msg . sender ] 0;}}The contract at msg.sender can get multiple refunds and retrieveall Fund’s ether by recursively calling withdraw before its shareis set to 0. Besides, it can modify the state of some third contract,which Fund depends on. Use the “checks – effects – interactions“pattern: first check the invariants, then update the internal state,then communicate with external entities (see also Section 2.1.4):function withdraw () public {uint balance balances [ msg . sender ];balances [ msg . sender ] 0;msg . sender . transfer ( balance ) ;// state reverted , balance restored if transfer fails}The pattern detects an external function call which is followedby an internal function call.2.1.6 Malicious libraries. Third-party libraries can be malicious.Avoid external dependencies or ensure that third-party code implements only the intended functionality. The pattern simply detectsthe library keyword (and thus produces some false positives).2.1.7 Using tx.origin. Contracts can call each others’ publicfunctions. tx.origin is the first account in the call chain (alwaysan externally owned one, i.e., not a contract); msg.sender is theimmediate caller. For instance, in a call chain A B C, from theC’s viewpoint, tx.origin is A, and msg.sender is B.Use msg.sender instead of tx.origin for authentication. Consider a wallet:pragma solidity 0.4.19;contract TxWallet {address private owner ;function TxWallet () { owner msg . sender ; }function transferTo ( address dest , uint amount ) public{require ( tx . origin owner ) ; // authenticationdest . transfer ( amount ) ;}}User sends ether to the address of the TxAttackerWallet, whichforwards the call to a TxWallet and obtains all funds, acting as theuser (tx.origin):pragma solidity 0.4.19;interface TxWallet {function transferTo ( address dest , uint amount ) ;}contract TxAttackerWallet {address private owner ;function TxAttackerWallet () { owner msg . sender ; }WETSEB’18, May 27, 2018, Gothenburg, Swedenfunction () payable {TxWallet ( msg . sender ) . transferTo ( owner , msg . sender. balance ) ;}}The pattern detects the environmental variable tx.origin.2.1.8 Transfer forwards all gas. Solidity provides many ways totransfer ether (see Section 2.1.4). addr.call.value(x)() transfersx ether and forwards all gas to addr, potentially leading to vulnerabilities like re-entrancy (see Section 2.1.5). The recommended wayto transfer ether is addr.transfer(x), which only provides thecallee with a “stipend“ of 2300 gas. The pattern detects functionswhose name is call.value and whose argument list is empty.2.2Functional issues2.2.1 Integer division. Solidity supports neither floating-pointnor decimal types. For integer division, the quotient is roundeddown. Account for it, especially when calculating ether or tokenamounts. The pattern detects division (/) where the the numeratorand the denominator are number literals.2.2.2 Locked money. Contracts programmed to receive ethershould implement a way to withdraw it, i.e., call transfer (recommended), send, or call.value at least once. The patterns detectscontracts that contain a payable function but contain neither ofthe withdraw-enabling functions mentioned above.2.2.3 Unchecked math. Solidity is prone to integer over- andunderflow7 . Overflow leads to unexpected effects and can lead toloss of funds if exploited by a malicious account. Use the SafeMathlibrary8 that checks for overflows (multiple implementations exist,e.g. [Saf17]). The pattern detects arithmetic operations , -, *, whichare not inside a conditional statement. This rule was temporarilymuted for testing (Section 4) due to a high false positive rate.2.2.4 Timestamp dependence. Miners can manipulate environmental variables and are likely to do so if they can profit from it.Consider a lottery that distributes prizes depending on whethernow (alias for block.timestamp) is odd or even:if ( now % 2 0) winner pl1 ; else winner pl2 ;A miner can tweak the timestamp and gain unfair advantage.Use block numbers and average time between blocks to estimatethe current time. Use secure sources of randomness, such as RANDAO [Ran17]. The pattern detects the environmental variable now.2.2.5 Unsafe type inference. Solidity supports type inference:the type of i in var i 42; is the smallest integer type sufficientto store the right-hand side value (uint8). Consider a for-loop:for ( var i 0; i array . length ; i ) { /* . */ }The type of i is inferred to uint8. If array.length is biggerthan 256, an overflow will occur. Explicitly define the type whendeclaring integer variables:for ( uint256 i 0; i array . length ; i ) { /* . */ }The pattern detects assignments where the left-hand side is avar and the right-hand side is an integer (matches ˆ[0-9] ).7 Referred8 Seeto as simply overflow for brevity.Section 2.1.6 for advice on library usage.

WETSEB’18, May 27, 2018, Gothenburg, Sweden2.3S. Tikhomirov, E. Voskresenskaya, I. Ivanitskiy, R. Takhaviev, E. Marchenko, Y. AlexandrovOperational issues2.3.1 Byte array. Use bytes instead of byte[] for lower gasconsumption. The pattern detects the construction byte[].2.3.2 Costly loop. Ethereum is a very resource-constrained environment. Prices per computational step are orders of magnitudehigher than with centralized cloud providers. Moreover, Ethereumminers impose a limit on the total number of gas consumed in ablock. In the following example, if array.length is large enough,the function exceeds the block gas limit, and transactions calling itwill never be confirmed:for ( uint256 i 0; i array . length ; i ) { costlyF () ; }This becomes a security issue, if an external actor influencesarray.length. E.g., if array enumerates all registered addresses,and registration is open, an adversary can register many addresses,causing denial of service. The rule includes two patterns: a for-statement with a function call or an identifier insidethe condition; a while-statement with a function call inside the condition.2.4Developmental issues2.4.1 Token API violation. ERC20 is the de-facto standard APIfor implementing tokens – transferable units of value managed bya contract. Exchanges and other third-party services may struggleto integrate a token that does not conform to it. Certain ERC20functions (approve, transfer, transferFrom) return a bool indicating whether the operation succeded. It is not recommended tothrow exceptions (revert, throw, require, assert) inside thosefunctions. Note that library functions may also throw exceptions(see Section 2.1.6).function transferFrom ( address spender , uint value )returns ( bool success ) {require ( value 20 wei ) ;// .}The pattern detects a contract inherited from a contract witha name including the word “token“, which may throw exceptionsfrom inside one of the functions mentioned above.2.4.2 Compiler version not fixed. Solidity source files indicatethe versions of the compiler they can be compiled with:pragma solidity 0.4.19;pragma solidity 0.4.19;// bad : 0.4.19 and above// good : 0.4.19 onlyIt is recommended to follow the latter example, as future compilerversions may handle certain language constructions in a way thedeveloper did not foresee. The pattern detects the version operator ˆin the pragma directive.2.4.3 private modifier. Contrary to a popular misconception,the private modifier does not make a variable invisible. Minershave access to all contracts’ code and data. Developers must account for the lack of privacy in Ethereum. The pattern detects statevariable declarations with a private modifier.2.4.4 Redundant fallback function. Contracts should reject unexpected payments (see Sections 2.1.1, 2.2.2). Before Solidity 0.4.0,it was done manually:function () payable { throw ; }Starting from Solidity 0.4.0, contracts without a fallback functionautomatically revert payments, making the code above redundant.The pattern detects the described construction (only if the pragmadirective indicates the compiler version not lower than 0.4.0).2.4.5 Style guide violation. In Solidity, function9 and event namesusually start with a lower- and uppercase letter respectively:function Foo () ;event logFoo () ;function foo () ;event LogFoo () ;////////badbadgoodgoodViolating the style guide decreases readability and leads to confusion. The pattern detects the described constructions.2.4.6 Implicit visibility level. The default function visibility levelin Solidity is public. Explicitly define function visibility to preventconfusion.function foo () { /* . */ } // badfunction foo () public { /* . */ } // goodfunction bar () private { /* . */ } // goodThe pattern detects function and variable definitions without avisibility modifier.3AUTOMATED ANALYSIS OF SMARTCONTRACTS3.1 Approaches to code analysisDynamic code analysis runs the program and considers only asubset of all execution paths on some input data [LSCL12]. Staticcode analysis may guarantee full coverage without executing theprogram and may run fast enough on code of reasonable size. Staticanalysis usually includes three stages:(1) building an intermediate representation (IR), such as abstractsyntax tree or three-address code, for a deeper analysis compared to analyzing text;(2) enriching the IR with additional information [Wög05] using algorithms such as control- and dataflow analysis (synonym, constant, and type propagation [ASU07]), taint analysis [TPF 09], symbolic execution, abstract interpretation;(3) vulnerability detection w.r.t. a database of patterns, whichdefine vulnerability criteria in IR terms.In this paper, we do not consider formal verification methods, asthey require a rarely available formal specification of the contract’sintended functionality.3.2SmartCheckWe propose SmartCheck – a static analysis tool for Ethereum smartcontracts implemented in Java. SmartCheck runs lexical and syntactical analysis on Solidity source code. It uses ANTLR [ant17] anda custom Solidity grammar to generate an XML parse tree [ASU07]as an intermediate representation (IR). We detected vulnerabilitypatterns by using XPath [xpa] queries on the IR. Thus SmartCheckprovides full coverage: the analyzed code is fully translated to theIR, and all its elements can be reached with XPath matching. Linenumbers are stored as XML attributes and help localize findings in9 Withthe exception of constructors: they must share the name with the contract andthus usually start with an uppercase letter.

SmartCheck: Static Analysis of Ethereum Smart ContractsTable 1: Code issues detected by SmartCheck(gray background – false positives possible)NameS.Balance equal- 2ity (2.1.1)Unchecked ex- 3ternal call (2.1.2)DoS by external 3contract (2.1.3)send instead of 2transfer (2.1.4)Reentrancy (2.1.5)Maliciouslibraries (2.1.6)31Using2tx.origin (2.1.7)Transferfor- 3wardsallgas (2.1.8)Integerdivi- 1sion (2.2.1)Locked2money (2.2.2)Uncheckedmath (2.2.3)Timestamp dependence (2.2.4)Unsafe type inference (2.2.5)Byte array (2.3.1)Costlyloop (2.3.2)12212Token API viola- 1tion (2.4.1)Compiler1versionnotfixed (2.4.2)private modi- 1fier (2.4.3)Redundant1fallback function (2.4.4)Style guide viola- 1tion (2.4.5)Implicit visibil- 1ity level (2.4.6)DescriptionAdversary can manipulate contract logicby forcibly sending it ether. Use non-strictinequality on balancesThe return value is not checked. Alwayscheck return values of functionsExpect external calls to deliberately throwWETSEB’18, May 27, 2018, Gothenburg, SwedenFigure 1: Parse tree for the Balance equality code exampleifStatementThe private modifier does not hide thevariable’s value, only prevents external contracts from editing itThe payment rejection fallback is redundant. Remove the function to save space:payments are rejected automaticallyUnfamiliar capitalization style causes confusion. Start function names with lowercase, events with uppercaseFunctions are public by default. Avoid ambiguity: explicitly declare visibility level{ .expressionexpressionThe return value of send should bechecked. Use transfer, which is equivalent to if (!send()) throw;External contracts should be called after alllocal state updatesUsing external libraries may be dangerous.Avoid external code dependencies, audit allcode that is part of the projectA malicious contract can act on a user’sbehalf. Use msg.sender for authenticationa.call.value()() forwards all gas, allowing the callee to call back. Usea.transfer(): it only provides the calleewith 2300 gas (insufficient for a callback)The quotient is rounded down. Account forit, especially for ether and token amountsThe contract receives ether, but there is noway to withdraw it. Implement a withdrawfunction or reject paymentsWithout extra checks, integer over- andunderflow is possible. Use SafeMathMiners can alter timestamps. Make criticalcode independent of the environmentType inference choses the smallest integertype possible. Explicitly specify typesbyte[] requires more than bytesExpensive computation inside loops mayexceed the block gas limit. Avoid loops withbig or unknown number of stepsThe contract throws where the ERC20 standard expects a bool. Return false insteadContract compiles with future compiler versions. Specify the exact compiler versionblockifConditionifenvVarDefthis.balance 2source code. IR attributes can be enriched with additional information when new analysis methods are implemented. The tool canbe extended to support other smart contact languages by addingan ANTLR grammar and a pattern database (IR-level algorithmsremain unchanged).As an example, consider the Balance equality issue (2.1.1). We aimto detect constructions that test the contract’s balance for equality,for instance:if ( this . balance 42 ether ) {.}.The parse tree of this construction is shown in Figure 1.The corresponding XPath pattern is shown in Listing 1.// expression [ expression // envVarDef[ matches ( text () [1] , " this . balance " ) ]][ matches ( text () [1] , " ! " ) ]Listing 1: XPath pattern for the Balance equality issueIn this case we do not expect false positives, as we are able toprecisely describe the target construction in XPath10 .More complex rules can not be precisely described with XPath,which leads to false positives. Consider the Re-entrancy issue (2.1.5).SmartCheck reports violations of the Checks-Effects-Interactions(CEI) pattern, which does not always lead to re-entrancy (Listing 2).pragma solidity 0.4.19;contract Foo {bool inBar false ;function bar ( address someAddress ) {if ( inBar ) throw ;inBar true ;someAddress . transfer (0) ;inBar false ;}}Listing 2: Violation of CEI not leading to re-entrancy10 Assumingthat ANTLR builds the AST correctly based on the Solidity grammar.

WETSEB’18, May 27, 2018, Gothenburg, SwedenS. Tikhomirov, E. Voskresenskaya, I. Ivanitskiy, R. Takhaviev, E. Marchenko, Y. Alexandrov4 EXPERIMENTAL RESULTS4.1 Goals and definitionsWe compare SmartCheck with three freely available tools aimed atstatically detecting vulnerabilities in Ethereum contracts: Oyente,Remix, and Securify11 and with the results of manual audit.We define a true finding as an issue (detected by a tool withmanual verification or manually) that is a bad practice and shouldbe fixed from our viewpoint (it may or may not be an exploitablevulnerability). All issues found by the tools were manually labeled aseither true positive (TP) or false positive (FP). A false negative (FN)for each of the four tools (Oyente, Remix, Securify, and SmartCheck)is a true finding that was not detected by this tool.For each tool, the false discovery rate (FDR) is the number of FPsfor this tool divided by the number of all issues reported by thistool: FDR FP / (TP FP). False negative rate (FNR) is the numberof FNs for this tool divided by the number of all true findings (foundby any of the tools or manually), which is the sum of TP and FNfor this tool: FNR FN / (TP FN).Section 4.2 assesses FDR and FNR of SmartCheck and three othertools on three typical contracts. Section 4.3 measures the prevalenceof code issues on a large set of real-world contracts.and block the normal operation of the contract. A public function(i.e., such that any Ethereum user can call it) allowed to add anelement to an internal array (Listing 3). Several critical functionsthen iterated through this array (e.g., Listing 4), so an attackercould make those functions permanently fail (a function call wouldrequire more gas than the block gas limit).function createGroup ( string name , uint goal )onlyOpenAuctionreturns ( uint8 err , uint groupIndex ){if ( checkDeadline () false && goal fundingGoal &&goal invoiceAmount ) {groupIndex groups . length ;groups [ groupIndex ]. groupIndex groupIndex ;groups [ groupIndex ]. name name ;groups [ groupIndex ]. goal goal ;EventGroupCreated ( groupIndex , name , goal );return (0 , groupIndex ) ;} else {return (1 , 0) ;}}Listing 3: Adding an element to the internal array4.2Case studiesWe consider three contracts: Genesis (“the platform for the private trust management market“ [Gen17a], source code [Gen17b],analyzed at commit 1ecf99d), Hive (“the first crypto currencyinvoice financing platform“ [Hiv17a], source code [Hiv17b], analyzed at commit 0d54699), and Populous (“an online platformthat matchmakes invoice sellers to invoice buyers hosted on theblockchain“ [Pop17a], source code [Pop17b], analyzed at commit10de4ae).The FDR and FNR for each tool (in % and in absolute numbers)are presented in Table 2.Oyente and Securify did not show any TPs on these threee contracts. Remix detected TPs only in the Populous contract. Remix andSmartCheck showed an overall FDR of 97% and 69% respectively,and an overall FNR of 92% and 47% respectively. This means thatSmartCheck showed better FDR and FNR compared to its closestcompetitor. Overall, SmartCheck reported 87 issues in the threecontracts.Requirements for code analysis tools differ across platforms anddomains. Due to a peculiar security landscape in smart contractprogramming (see Section 1.1), low FN rate is crucial (a missedvulnerabili

Ethereum was introduced in 2014 and launched in 2015 [VB 14]. Ethereum nodes store data, execute smart contracts, and maintain a shared view of the global state using a proof-of-work consensus mechanism similar to that in Bitcoin [Tik17]. Contrary to previ-ous attempts at blockchain programming, e.g., Bitcoin scripting,