Formal Specification and Verification of SmartContracts in Azure BlockchainYuepeng WangUniversity of Texas at Austinypwang@cs.utexas.eduShuvendu K. LahiriMicrosoft Researchshuvendu@microsoft.comShuo ChenMicrosoft Researchshuochen@microsoft.comRong PanUniversity of Texas at Austinrpan@cs.utexas.eduIsil DilligUniversity of Texas at Austinisil@cs.utexas.eduCody BornMicrosoft Azurecoborn@microsoft.comImmad NaseerMicrosoft Azureimnaseer@microsoft.comAbstract—Ensuring correctness of smart contracts isparamount to ensuring trust in blockchain-based systems. Thispaper studies the safety and security of smart contracts inthe Azure Blockchain Workbench, an enterprise Blockchain-as-a-Service offering from Microsoft. As part of this study, weformalize semantic conformance of smart contracts against astate machine model with access-control policy and develop ahighly-automated formal verifier for Solidity that can produceproofs as well as counterexamples. We have applied our verifierVERISOLto analyzeallcontracts shipped with the AzureBlockchain Workbench, which includes application samples aswell as a governance contract for Proof of Authority (PoA).We have found previously unknown bugs in these publishedsmart contracts. After fixing these bugs,VERISOLwas able tosuccessfully perform full verification for all of these contracts.I. INTRODUCTIONAs a decentralized and distributed consensus protocol tomaintain and secure a shared ledger, the blockchain is seen asa disruptive technology with far-reaching impact on diverseareas. As a result, major cloud platform companies, includingMicrosoft, IBM, Amazon, SAP, and Oracle, are offeringBlockchain-as-a-Service (BaaS) solutions, primarily targetingenterprise scenarios, such as financial services, supply chains,escrow, and consortium governance. A recent study by Gartnerpredicts that the business value-add of the blockchain has thepotential to exceed $3.1 trillion by 2030 [16].Programs running on the blockchain are known as smartcontracts. The popular Ethereum blockchain provides a low-level stack-based bytecode language that executes on top ofthe Ethereum Virtual Machine (EVM). High-level languagessuch as Solidity and Serpent have been developed to enabletraditional application developers to author smart contracts.However, because blockchain transactions are immutable, bugsin smart contract code have devastating consequences, andvulnerabilities in smart contracts have resulted in severalhigh-profile exploits that undermine trust in the underlyingblockchain technology. For example, the infamousTheDAOexploit [1] resulted in the loss of almost $60 million worth ofEther, and theParity Walletbug caused 169 million USDworth of ether to be locked forever [4]. The only remedy forthese incidents was to hard-fork the blockchain and revert oneof the forks back to the state before the incident. However,this remedy itself is devastating as it defeats the core valuesof blockchain, such as immutability, decentralized trust, andself-governance. This situation leaves no options for smartcontract programmers other than writing correct code to startwith.Motivated by the serious consequences of bugs in smartcontract code, recent work has studied many types of securitybugs such as reentrancy, integer underflow/overflow, and issuesrelated to delegatecalls on Ethereum. While these low-levelbugs have drawn much attention due to high-visibility incidentson public blockchains, we believe that the BaaS infrastructureand enterprise scenarios bring a set of interesting, yet lesswell-studied security problems.In this paper, we present our research on smart contractcorrectness in the context of Azure Blockchain, a BaaS solutionoffered by Microsoft [3]. Specifically, we focus on a cloudservice named Azure Blockchain Workbench (or Workbenchfor short) [6], [7]. The Workbench allows an enterprisecustomer to easily build and deploy a smart contract applicationintegrating active directory, database, web UI, blob storage, etc.A customer implements the smart contract application (thatmeets the requirements specified in an application policy) anduploads it onto the Workbench. The code is then deployedto the underlying blockchain ledger to function as an end-to-end application. In addition to customer (application) smartcontracts, the Workbench system itself is comprised of smartcontracts that customize the underlying distributed blockchainconsensus protocols. Workbench ships one such smart contractfor the governance of the Ethereum blockchain that uses theProof-of-Authority (PoA) consensus protocol for validatingtransactions. Workbench relies on the correctness of the PoAgovernance contract to offer a trusted blockchain on Azure.Customer contracts in the Workbench architecture implementcomplex business logic, starting with a high-level finite-state-machine (FSM) workflow policy specified in a JSON file.Intuitively, the workflow describes (a) a set of categories ofusers called roles, (b) the different states of a contract, and(c) the set of enabled actions (or functions) at each staterestricted to each role. The high-level policy is useful toarXiv:1812.08829v2 [cs.PL] 29 Apr 2019 design contracts around state machine abstractions as wellas specify the required access-control for the actions. Whilethese state machines offer powerful abstraction patterns duringsmart contract design, it is non-trivial to decide whether agiven smart contract faithfully implements the intended FSM.In this paper, we define semantic conformance checking asthe problem of deciding whether a customer contract correctlyimplements the underlying workflow policy expressed as anFSM. Given a Workbench policyπthat describes the workflowand a contractC, our approach first constructs a new contractC0such thatCsemantically conforms toπif and only ifC0does not fail any assertions.In order to automatically check the correctness of theassertions in a smart contract (such asC0or PoA governance),we develop a new verifier called VERISOL for smart contractswritten in Solidity. VERISOL is a general-purpose Solidityverifier and is not tied to Workbench. The verifier encodes thesemantics of Solidity programs into a low-level intermediateverification language Boogie and leverages the well-engineeredBoogie verification pipeline [14] for both verification andcounter-example generation. In particular, VERISOL takes ad-vantage of existing bounded model checking tool CORRAL [24]for Boogie to generate witnesses to assertion violations, and itleverages practical verification condition generators for Boogieto automate correctness proofs. In addition, VERISOL usesmonomial predicate abstraction [17], [22] to automaticallyinfer so-called contract invariants, which we have found to becrucial for automatic verification of semantic conformance.To evaluate the effectiveness and efficiency of VERISOL, wehave performed an experiment on all11sample applicationsthat are shipped with the Workbench, as well as the PoAgovernance contract for the blockchain itself. VERISOL finds4previously unknown defects in these published smart contracts,all of which have been confirmed as true bugs by the developers(many of them fixed at the time of writing). The experimentalresults also demonstrate the practicality of VERISOL in thatit can perform full verification of all the fixed contracts withmodest effort; most notably, VERISOL can automatically verify10out of11of the fixed versions of sample smart contractswithin 1.7 seconds on average.Contributions.This paper makes the following contributions:1)We study the safety and security of smart contracts presentin Workbench, a BaaS offering.2)We formalize the Workbench application policy languageand define the semantic conformance checking problembetween a contract and a policy.3)We develop a new formal verifier VERISOL for smartcontracts written in Solidity.4)We perform an evaluation of VERISOL on all the contractsshipped with Workbench. This includes all the applicationsamples as well as the highly-trusted PoA governancecontract.5)We report previously unknown bugs that have been con-firmed and several already fixed.Application Roles: Requestor (REQ) Responder (RES)TF: SendResponseTF: SendRequestRequest RespondAR: RESAIR: REQLegendTF: Transition FunctionAIR: Allowed Instance RoleAR: Allowed RoleFig. 1. Workflow policy diagram for HelloBlockchain application.II. OVERVIEWIn this section, we give an example of a Workbenchapplication policy for a sample contract and describe ourapproach for semantic conformance checking between thecontract and the policy.A. Workbench Application PolicyWorkbench requires every customer to provide a policy (ormodel) representing the high-level workflow of the applicationin a JSON file1. The policy consists of several attributes such asthe application name and description, a set of roles, as well asa set of workflows. For example, Figure 1 provides an informalpictorial representation of the policy for a simple applicationcalledHelloBlockchain.2. The application consists of twoglobal roles (see “Application Roles”), namely REQUESTORand RESPONDER. Informally, each role represents a set ofuser addresses and provides access control or permissions forvarious actions exposed by the application. We distinguish aglobal role from an instance role in that the latter applies to aspecific instance of the workflow. It is expected that the instanceroles are always a subset of the user addresses associated withthe global role.As illustrated in Figure 1, the simpleHelloBlockchainapplication consists of a single workflow with two states,namelyRequestandRespond. The data members (or fields)include instance role members (RequestorandResponder)that range over user addresses. The workflow consists of twoactions (or functions) in addition to the constructor function,SendRequestandSendResponse, both of which take a stringas argument.A transition in the workflow consists of a start state, anaction or function, an access control list, and a set of successorstates. Figure 1 describes two transitions, one from each of thetwo states. For example, the application can transition fromRequesttoRespondif a user belongs to the RESPONDER role1https://docs.microsoft.com/en-us/azure/blockchain/workbench/configuration2The example related details can be found on the associated web page: https://github.com/Azure-Samples/blockchain/tree/master/blockchain-workbench/application-and-smart-contract-samples/hello-blockchain (AR) and invokes the actionSendResponse. An “ApplicationInstance Role” (AIR) refers to an instance role data memberof the workflow that stores a member of a global role (suchasRequestor). For instance, the transition fromRespondtoRequestin Figure 1 uses anAIRand is only allowed if theuser address matches the value stored in the instance datavariable Requestor.pragma solidity ^0.4.20;contract HelloBlockchain {//Set of Statesenum StateType { Request , Respond }//List of propertiesStateType public State;address public Requestor ;address public Responder ;string public RequestMessage ;string public ResponseMessage ;// constructor functionfunction HelloBlockchain ( string message )constructor_checker()public{Requestor = msg. sender ;RequestMessage = message ;State = StateType . Request ;}// call this function to send a requestfunction SendRequest (string requestMessage )SendRequest_checker() public{RequestMessage = requestMessage ;State = StateType . Request ;}// call this function to send a responsefunction SendResponse ( string responseMessage )SendResponse_checker() public{Responder = msg. sender ;ResponseMessage = responseMessage ;State = StateType . Respond ;}<modifier definitions>}Fig. 2. Solidity contract for HelloBlockchain application.B. Workbench Application Smart ContractAfter specifying the application policy, a user provides asmart contract for the appropriate blockchain ledger to imple-ment the workflow. Currently, Workbench supports the popularlanguage Solidity for targeting applications on Ethereum.Figure 2 describes a Solidity smart contract that implementstheHelloBlockchainworkflow in theHelloBlockchainapplication. For the purpose of this sub-section, we start byignoring the portions of the code that areunderlined. Thecontract declares the data members present in the configurationas state variables with suitable types. Each contract implement-ing a workflow defines an additional state variableStatetotrack the current state of a workflow. The contract consists ofthe constructor function along with the two functions definedin the policy, with matching signatures. The functions set thestate variables and update the state variables appropriately toreflect the state transitions.The Workbench service allows a user to upload the policy, theSolidity code, and optionally add users and perform variousactions permitted by the configuration. Although the smartcontract drives the application, the policy is used to exposethe set of enabled actions at each state for a given user.Discrepancies between the policy and Solidity code can leadto unexpected state transitions that do not conform to the high-level policy. To ensure the correct functioning and security ofthe application, it is crucial to verify that the Solidity programsemantically conforms to the intended meaning of the policyconfiguration.C. Semantic Conformance VerificationGiven the application policy and a smart contract, wedefine the problem of semantic conformance between thetwo that ensures that the smart contract respects the policy(SectionIII-B). Moreover, we reduce the semantic conformanceverification problem to checking assertions on an instrumentedSolidity program. For theHelloBlockchainapplication, theinstrumentation is provided by adding theunderlinedmodifierinvocations in Figure 2. A modifier is a Solidity languageconstruct that allows wrapping a function invocation with codethat executes before and after the execution.function nondet () returns ( bool ); // no definition// Checker modifiersmodifier constructor_checker (){_;assert ( nondet () /* global role REQUESTOR */==> State == StateType . Request );}modifier SendRequest_checker (){StateType oldState = State;address oldRequestor = Requestor ;_;assert (( msg. sender == oldRequestor &&oldState == StateType . Respond )==> State == StateType . Request );}modifier SendResponse_checker (){StateType oldState = State;_;assert (( nondet () /* global role RESPONDER */ &&oldState == StateType . Request )==> State == StateType . Respond );}Fig. 3. Modifier definitions for instrumented HelloBlockchain application.Figure 3 shows the definition of the modifiers used toinstrument for conformance checking. Intuitively, we wrapthe constructor and functions with checks to ensure that theyimplement the FSM state transitions correctly. For example,if the FSM transitions from a states1to a states2upon theinvocation of functionfby a user with access controlac, thenwe instrument the definition offto ensure that any executionstarting ins1with access control satisfyingacshould transitionto s2.Finally, given the instrumented Solidity program, we dis-charge the assertions statically using a new formal verifier forSolidity called VERISOL. The verifier can find counterexamples (in the form of a sequence of transactions involving calls to theconstructor and public methods) as well as automatically con-struct proofs of semantic conformance. Note that, even thoughthe simpleHelloBlockchainexample does not contain anyunbounded loops or recursion, verifying semantic conformancestill requires reasoning about executions that involve unboundednumbers of calls to the two public functions. We demonstratethat VERISOL is able to find deep violations of the conformanceproperty for well-tested Workbench applications, as wellas automatically construct inductive proofs for most of theapplication samples shipped with Workbench.III. SEMANTIC CONFORMANCE CHECKING FORWORKBENCH POLICIESIn this section, we formalize the Workbench applicationpolicy that we informally introduced in Section II. Our formal-ization can be seen as a mathematical representation of theofficial Workbench application JSON schema documentation.A. Formalization of Workbench Application PoliciesThe Workbench policy for an application allows the user todescribe (i) the data members and actions of an application,(ii) a high-level state-machine view of the application, and (iii)role-based access control for state transitions. The role-basedaccess control provides security for deploying smart contractsin an open and adversarial setting; the high-level state machinenaturally captures the essence of a workflow that progressesbetween a set of states based on some actions from the user.More formally, a Workbench Application Policy is a pair(R, W)whereRis a set of global roles used for accesscontrol, andWis a set of workflows defining a kind of finitestate machine. Specifically, a workflow is defined by a tuplehS, s0, Rw, F, F0, ac0, γi where:• S is a finite set of states, and s0∈ S is an initial state• Rwis a finite set of instance roles of the form(id : t),where id is an identifier and t is a role drawn from R• F(id0, . . . , idk)is a set of actions (functions), withF0denoting an initial action (constructor)• ac0⊆ Ris the initiator role for restricting users that cancreate an instance of the contract• γ ⊆ S × F × (Rw∪ R) × 2Sis a set of transitions. Givena transitionτ = (s, f, ac, S), we writeτ.s, τ.f, τ.ac, τ.Stodenote s, f, ac, and S respectivelyIntuitively,Sdefines the different “states” that the contractcan be in, andγdescribes which state can transition to whatother states by performing certain actions. The transitions areadditionally “guarded” by roles (which can be either global orinstance roles) that qualify which users are allowed to performthose actions. As mentioned earlier in Section II, each “role”corresponds to a set of users (i.e., addresses on the blockchain).The use of instance roles in the workbench policy allowsdifferent instances of the contract to authorize different usersto perform certain actions.B. Semantic ConformanceGiven a contractCand a Workbench Application policyπ, semantic conformance betweenCandπrequires that thecontractCfaithfully implements the policy specified byπ. Inthis subsection, we first define some syntactic requirements onthe contract, and then formalize what we mean by semanticconformance between a contract and a policy.Syntactic conformance. Given a client contractCand a policyπ = (R, W), our syntactic conformance requirement stipulatesthat the contract for eachw ∈ Wimplements all the instancestate variables as well as definitions for each of the functions.Additionally, each contract function has a parameter calledsender, which is a blockchain address that denotes the user orcontract invoking this function. Finally, each contract shouldcontain a state variableswthat ranges overSw, for eachw ∈ W.Semantic conformance. We formalize the semantic conformancerequirement for smart contracts using Floyd-Hoare triples ofthe form{φ} S {ψ}indicating that any execution of statementSstarting in a state satisfyingφresults in a state satisfyingψ(if the execution ofSterminates). We can define semanticconformance between a contract C and a policy π as a set ofHoare triples, one for each pair(m, s)wheremis a methodin the contract andsis a state in the Workbench policy. At ahigh-level, the idea is simple: we insist that, when a function isexecuted along a transition, the resulting state transition shouldbe in accordance with the Workbench policy.Given an application policyπ = (R, W)and workfloww = hS, s0, Rw, F, F0, ac0, γi ∈ W, we can formalize thishigh-level idea by using the following Hoare triples:1) Initiation.{sender ∈ ac0} F0(v1, . . . , vk) {sw= s0}The Hoare triple states that the creation of an instance ofthe workflow with the appropriate access controlac0resultsin establishing the initial state.2) Consecution. Letτ = (s1, f, ac , S2)be a transition inγ. Then, for each such transition, semantic conformancerequires the following Hoare triple to be valid:{sender ∈ ac ∧ sw= s1} f(v1, . . . , vk) {sw∈ S2}Here, the precondition checks two facts: First, thesendermust satisfy the access control, and, second, the startstate must bes1. The post-condition asserts that theimplementation of methodfin the contract results in astate that is valid according to policy π.C. Instrumentation for Semantic Conformance CheckingAs mentioned in Section II, our approach checks semanticconformance of Solidity contracts by (a) instrumenting thecontract with assertions, and (b) using a verification tool tocheck that none of the assertions can fail. We explain ourinstrumentation strategy in this subsection and refer the readerto Section IV for a description of our verification tool chain. Our instrumentation methodology heavily relies on themodifierconstruct in Solidity. A modifier has syntax verysimilar to a function definition in Solidity with a name andlist of parameters and a body that can refer to parameters andglobals in scope. The general structure of a modifier definitionwithout any parameters is [2]:modifier Foo () {pre -stmt ;_;post - stmt;}wherepre-stmtandpost-stmtare Solidity statements.When this modifier is applied to a function Bar,function Bar (int x) Foo (){Bar -stmt ;}the Solidity compiler transforms the body ofBarto executepre-stmt(respectively,post-stmt) before (respectively, af-ter)Bar-stmt. This provides a convenient way to inject codeat multiple return sites from a procedure and also inject codebefore the execution of the constructor code (since a constructormay invoke other base class constructors implicitly).We now define a couple of helper predicates before describ-ing the actual checks. LetP (ac)be a predicate that encodesthe membership of sender in the set ac:P (ac).=false, ac = {}msg.sender = q, ac = {q ∈ Rw}nondet() ac = {r ∈ R}P (ac1) ∨ P (ac2) ac = ac1∪ ac2Herenondetis a side-effect free Solidity function that returnsa non-deterministic Boolean value at each invocation. For thesake of static verification, one can declare a function withoutany definition. This allows us to model the membership checksender ∈ acconservatively in the absence of global roles onthe blockchain.Next, we define a predicate for membership of a contractstate in a set of states S0⊆ S using α(S0) as follows:α(S0).=false, S0= {}sw= s, S0= {s ∈ S}α(S1) ∨ α(S2), S0= S1∪ S2We can now use these predicates to define the source codetransformations below:Constructor. We add the following modifier to constructors:modifier constructor_checker () {_;assert (P (ac0) ⇒ α({s0}));}Here, the assertion ensures that the constructor sets up thecorrect initial state when executed by a user with access controlac0.Other functions. For a functiong, letγg.= {τ ∈ γ | τ =(s1, g, ac, S2)}be the set of all transitions wheregis invoked.call f0(*);while (true ) {if (*) call f1(*);else if (*) call f2(*);...else if (*) call fn(*);}Fig. 4. Harness for Solidity contractsmodifier g_checker () {// copy old StateStateType oldState = sw;// copy old instance role vars..._;assertVτ ∈γg(old (P (τ.ac) ∧ α({τ.s})) ⇒ α(τ.S));}Here, the instrumented code first copies theswvariableand all of the variables inRwinto corresponding “old”copies. Next, the assertion checks that if the function isexecuted in a transitionτ, then state transitions to one ofthe successor states inτ.S. The notationold(e)replacesany occurrences of a state variable (such assw) with the“old” copy that holds the value at the entry to the function.Figure 3 shows the modifier definitions for our running exampleHelloBlockchaindescribed in Section II Although we showthenondet()to highlight the issue of global roles, one cansafely replacenondet()withtruesince the function onlyappears negatively in any assertion. In fact, this observationallows us to add the simplified assertions for runtime checkingas well. Finally, since conjunction distributes over assertions,we can replace the single assertion with an assertion for eachtransition in the implementation.IV. FORMAL VERIFICATION USING VERISOLIn this section, we present our formal verifier calledVERISOL for checking the correctness of assertions in Soliditysmart contracts. Since our verifier is built on top of theBoogie tool chain, it can be used for both verification andcounterexample generation.A. General MethodologyLetC = {λ x0.f0, λ x1.f1, . . . , λ xn.fn}be a smartcontract annotated with assertions where:• λ x0.f0is the constructor• λ xi.fifor i ∈ [1, n] are public functionsOur verification methodology is based on finding a contractinvariant I satisfying the following Hoare triples:|= {true} f0{I} (1)|= {I} fi{I} for all i ∈ [1, n] (2)Here, the first condition states the contract invariant isestablished by the constructor, and the second condition statesthatIis inductive — i.e., it is preserved by every publicfunction inC. Note that such a contract invariant suffices to VeriSolBoogieTranslationInvariantGenerationBoundedModelCheckingSmart Contractwith AssertionsFully VerifiedVerified Up ToK TransactionsCounterexampleFig. 5. Schematic workflow of VERISOL.establish the validity of all assertions in the contract underany possible sequence of function invocations of the contract.To see why this is the case, consider a “harness” that invokesthe functions inCas in Figure 4. This harness first createsan instance of the contract by calling the constructor, andthen repeatedly and non-deterministically invokes one of thepublic functions ofC. Observe that the Hoare triples (1) and(2) listed above essentially state thatIis an inductive invariantof the loop in this harness; thus, the contract invariantIoverapproximates the state of the contract under any sequenceof the contract’s function invocations. Furthermore, when thefunctions contain assertions, the Hoare triple{I} fi{I}canonly be proven ifIis strong enough to imply the assertionconditions. Thus, the validity of the Hoare triples in (1) and(2) establishes correctness under all possible usage patterns ofthe contract.B. OverviewWe now describe the design of our tool called VERISOL forchecking safety of smart contracts. VERISOL is based on theproof methodology outlined in SectionIV-A, and its workflowis illustrated in Figure 5. At a high-level, VERISOL takes asinput a Solidity contractCannotated with assertions and yieldsone of the following three outcomes:•Fully verified: This means that the assertions inCareguaranteed not to fail under any usage scenario.•Refuted: This indicates thatCwas able to find at least oneinput and invocation sequence of the contract functions underwhich one of the assertions is guaranteed to fail.•Partially verified: When VERISOL can neither verify norrefute contract correctness, it performs bounded verificationto establish that the contract is safe up toktransactions.This essentially corresponds to unrolling the ”harness” loopfrom Figure 4ktimes and then verifying that the assertionsdo not fail in the unrolled version.VERISOL consists of three modules, namely (a) BoogieTranslation from a Solidity program, (b) Invariant Generationto infer a contract invariant as well as loop invariants andprocedure summaries, and (c) Bounded Model Checking toexplore assertion failures within all transactions up to a user-specified depthk. In the remaining subsections, we discusseach of these components in more detail.ct ∈ ContractNameset ∈ SolElemTypes ::= integer | string | addressst ∈ SolTypes ::= et | ct | et ⇒ stse ∈ SolExprs ::= c | x | op(se, . . . , se) | se[se]| msg.sender | x.lengthsst ∈ SolStmts ::= x := se | x[se] . . . [se] := y | sst; sst| require(se) | assert(se)| if (se) {sst} else {sst}| while (se) do {sst} | x.push(se)| se := f(se) | se := se.f(se)| se := new C(se) | se := new t[](se)| se := new (t1⇒ t2⇒ . . . ⇒ tk⇒ t)()Fig. 6. A subset of Solidity language.Cdenotes a contract name,tdenotesan elementary Solidity type, and f denotes a function name.C. Solidity to Boogie TranslationIn this subsection, we formally describe our translation ofSolidity source code to the Boogie intermediate verificationlanguage. We start with a brief description of Solidity andBoogie, and then discuss our translation.Solidity Language.Figure 6 shows a core subset of Soliditythat we use for our formalization. At a high level, Solidity isa typed object-oriented programming language with built-insupport for basic verification constructs, such as therequireconstruct for expressing pre-conditions.Types in our core language include integers, strings, contracts,addresses, and mappings. We use the notationτ1⇒ τ2todenote a mapping from a value of typeτ1to a value of typeτ2(whereτ2can be a nested map type). Since arrays can beviewed as a special form of mappinginteger ⇒ τ, we do notintroduce a separate array type to simplify presentation.As standard, expressions in Solidity include constants, localvariables, state variables (i.e., fields in standard object-orientedlanguage terminology), unary/binary operators (denotedop),and array/map lookupe[e0]. Given an arrayx, the expressionx.lengthyields the length of that array, andmsg.senderyields the address of the contract or user that initiates thecurrent function invocation.Statements in our core Solidity language include assignments,conditional statements, loops, sequential composition, arrayinsertion (push), internal and external function calls, contractinstance creation, and dynamic allocations. The constructrequireis used to specify the precondition of a function, andassertchecks that its input evaluates to true and terminatesexecution otherwise. Solidity differentiates between two typesof function calls: internal and external. An internal callse := f(se)invokes the functionfand keepsmsg.senderunchanged. An external callse := se0.f(se)invokes functionfin the contract instance pointed byse0(which may includethis), and uses this as the msg.sender for the callee. bbt ∈ BoogieElemTypes ::= int | Refbt ∈ BoogieTypes ::= bbt | [bbt ]bte ∈ Exprs ::= c | x | op(e, . . . , e) | uf(e, . . . , e)| x[e] . . . [e] | ∀i : bbt :: est ∈ Stmts ::= skip | havoc x | x := e| x[e] . . . [e] := e| assume e | assert e| callx := f(e, . . . , e) | st; st| if (e) {st} else {st} | while (e) do {st}Fig. 7. A subset of Boogie language.We omit several aspects of the language that are desugaredinto our core Solidity language. This includes fairly compre-hensive support for modifiers, libraries and structs.Boogie Language.Since our goal is to translate Solidityto Boogie, we also give a brief overview of the Boogieintermediate verification language. As shown in Figure 7,types in Boogie include integers (int), references (Ref),and nested maps. Expressions (Exprs) consist of constants,variables, arithmetic and logical operators (op), uninterpretedfunctions (uf), map lookups, and quantified expressions.Standard statements (Stmts) in Boogie consist of skip, variableand array/map assignment, sequential composition, conditionalstatements, and loops. Thehavoc xstatement assigns anarbitrary value of appropriate type to a variablex. A procedurecall (callx := f(e, . . . , e)) returns a vector of values thatcan be stored in local variables. Theassertandassumestatements behave as no-ops when their arguments evaluate totrue and terminate execution otherwise. An assertion failure isconsidered a failing execution, whereas an assumption failureblocks.From Solidity to Boogie types.We define a functionµ :SolTypes → BoogieTypesthat translates a Solidity type to atype in Boogie as follows:µ(st).=int, st ∈ { integer, string}Ref , st ∈ {address} ∪ ContractNamesRef , st.= et ⇒ stSpecifically, we translate Solidity integers and strings to Boogieintegers; addresses, contract names, and mappings to Boogiereferences. Note that we represent Solidity strings as integers inBoogie because Solidity only allows equality checks betweenstrings in the core language.From Solidity to Boogie expressions.We present our trans-lation from Solidity to Boogie expressions using judgmentsof the form` e → χin Figure 8, whereeis a Solidityexpression andχis the corresponding Boogie expression. WhileSolidity local variables and the expressionmsg.senderaremapped directly into Boogie local variables and parametersrespectively, state variables in Solidity are translated into arraylookups. Specifically, for each state variablexfor contractC, we introduce a mappingxCfrom contract instancesox ∈ LocalVars` x → x(Var1)v = msg_sender` msg.sender → v(Sender)Type(c) 6= string` c → c(Const1)x ∈ StateVars(C)` x → xC[this](Var2)Type(c) = string c0= Hash(c)` c → StrToInt(c0)(Const2)` x → χ` x.length → Length[χ](Len)` e1→ χ1` e2→ χ2Type(e2) = t1Type(e1[e2]) = t2` e1[e2] → Mµ(t2)µ(t1)[χ1][χ2](Map)` ei→ χii = 1, . . . , n` op(e1, . . . , en) → op(χ1, . . . , χn)(Op)Fig. 8. Inference rules for encoding Solidity expressions to Boogie expressions.Type(e) is a function that returns the static type of Solidity expression e.to the value stored in its state variablex. Thus, reads fromstate variablexare modeled asxC[this]in Boogie. Next, wetranslate string constants in Solidity to Boogie integers usingan uninterpreted function called StrToInt that is applied to ahash of the string3. As mentioned earlier, this string-to-integertranslation does not cause imprecision because Solidity onlyallows equality checks between variables of type string.Similar to our handling of state variables, our Boogieencoding also introduces an array calledLengthto map eachSolidity array to its corresponding length. Thus, a Solidityexpressionx.lengthis translated asLength[χ]whereχisthe Boogie encoding of x.The translation of array/map look-up is somewhat moreinvolved due to potential aliasing issues. First, the basic ideais that for each map of typet1⇒ t2, we introduce a BoogiemapMτ0τwhereτis the Boogie encoding of typet1(i.e.,τ = µ(t1)) andτ0is the Boogie encoding of typet2(i.e.,τ0= µ(t2)). Intuitively,Mτ0τmaps each array/map object toits contents, which are in turn represented as a map. Thus, wecan think ofMτ0τas a two-dimensional mapping where the firstdimension is the address of the Solidity map and the seconddimension is the look-up key. For a nested map expressione1of typet1⇒ t2wheret2is a nested map/array, observe thatwe look upe1inMRefµ(t1)since maps and arrays in Solidityare dynamically allocated. Intuitively, everything that can bedynamically allocated is represented with typeRefin ourencoding to allow for potential aliasing.Example 1.Suppose that contractChas a state variablexofSolidity typemapping(int => int[]), which corresponds tothe typeint => (int => int)in our core Solidity language.3We assume that the hash function is collision-free. In our implementation,we enforce this by keeping a mapping from each string constant to a counter. The expressionx[0][1]will be translated into the BoogieexpressionMintint[e][1]whereeisMRefint[ xC[this] ][0]usingthe rules from Figure 8.From Solidity to Boogie statements.Figure 9 presents thetranslation from Solidity to Boogie statements using judgmentsof the form` s ωindicating that Solidity statementsis translated to Boogie statement(s)ω. Since most rules inFigure 9 are self-explanatory, we only explain our translationfor assignments, function calls, and dynamic allocations.Function calls. Functions in Solidity have two implicit parame-ters, namelythisfor the receiver object andmsg.senderforthe Blockchain address of the caller. Thus, when translatingSolidity calls to their corresponding Boogie version, weexplicitly pass these parameters in the Boogie version. However,recall that the value of the implicitmsg.senderparametervaries depending on whether the call is external or internal. Forinternal calls,msg.senderremains unchanged, whereas forexternal calls,msg.senderbecomes the current receiver object.For both types of calls, our translation introduces a conditionalstatement to deal with dynamic dispatch. Specifically, ourBoogie encoding introduces a mapτto store the dynamic typeof receiver objects at allocation sites, and the translation offunction calls invokes the correct version of the method basedon the content of τ for the receiver object.Dynamic allocation. Dynamic memory allocations in Solidityare translated into Boogie code with the aid of a helperprocedureNew(shown in Figure 10) which always returns afresh reference. As shown in Figure 10, theNewprocedure isimplemented using a global mapAllocto indicate whethera reference is allocated or not. All three types of dynamicmemory allocation (contract, array, and map) use this helperNew procedure to generate Boogie code.In the case of contract creation (labeled NewCont inFigure 9), the Boogie code we generate updates theτmapmentioned previously in addition to allocating new memory.Specifically, given the freshly allocated referencevreturned byNew, we initialize τ [v] to be C and also call C’s constructoras required by Solidity semantics.Next, let us consider the allocation of array objects describedin rule NewArr in Figure 9. Recall that our Boogie encodinguses a map calledLengthto keep track of the size ofevery array. Thus, in addition to allocating new memory, thetranslation of array allocation also updates theLengtharrayand initializes all elements in the array to be zero (or null).Finally, the rule NewMap shows how to translate map alloca-tions in Solidity to Boogie using an auxiliary Boogie procedurecalled MapInit (shown in Figure 10) for map initialization.Given ann-dimensional map, the MapInit procedure iterativelyallocates lower dimensional maps and ensures that valuesstored in the map do not alias each other as well as anyother previously allocated reference.Example 2. The Solidity codex := new (int => int => int)()is translated into the following Boogie code:1 call v := New (); assume Length [v] = 0;2 assume ∀i :: Length [MRefint[v][ i]] = 0;3 assume ∀i :: ¬Alloc [MRefint[v][ i]];4 call NewUnbounded ();5 assume ∀i :: Alloc[MRefint[v][ i]];6 assume ∀i,j :: i=j ∨ MRefint[v][ i] 6= MRefint[v][ j];7 assume ∀i,j :: Mintint[MRefint[v][ i]][j] = 0;8 xC[this ] := v;First of all, we allocate a fresh referencevand initialize thelength ofvand every inner mapv[i]to zero (lines 1 - 2).Second, we allocate fresh references for every inner mapv[i](lines 3 - 5), and ensure the references of inner mapsv[i]andv[j]do not alias ifi 6= j(line 6). Finally, we initializeevery elementv[i][j]to zero and assign referencevto the statevariable x (lines 7 - 8).D. Invariant GenerationAs mentioned earlier, translating Solidity code into Boogie al-lows VERISOL to leverage the existing ecosystem around Boo-gie, including efficient verification condition generation [25].However, in order to completely automate verification (evenfor loop and recursion-free contracts), we still need to infera suitable contract invariant as discussed in SectionIV-B.Specifically, recall that the contract invariant must satisfy thefollowing two properties:1) |= {true} f0{I}2) |= {I} fi{I} for all i ∈ [1, n]VERISOL uses monomial predicate abstraction ( [17], [22],[23]) to automatically infer contract invariants satisfying theabove properties. Specifically, the contract invariant inferencealgorithm conjectures the conjunction of all candidate predi-cates as an inductive invariant and progressively weakens itbased on failure to prove a candidate predicate inductive. Thisalgorithm converges fairly fast even on large examples butrelies on starting with a superset of necessary predicates. Inthe current implementation of VERISOL, we obtain candidateinvariants by instantiating the predicate templatee1 e2whereis either equality or disequality. Here, expressionse1, e2can be instantiated with variables corresponding to roles andstates in the Workbench policy as well as constants. We havefound these candidate predicates to be sufficiently general forautomatically verifying semantic conformance of Workbenchcontracts; however, additional predicates may be required forother types of contracts.E. Bounded Model CheckingIf VERISOL fails to verify contract correctness usingmonomial predicate abstraction, it employs an assertion-directed bounded verifier, namely CORRAL [24], to lookfor a transaction sequence leading to an assertion violation.CORRAL analyzes the harness in Figure 4 by unrolling theloopktimes and uses a combination of abstraction refinementtechniques (including lazy inlining of nested procedures) tolook for counterexamples in a scalable manner. Thus, whenVERISOL fails to verify the property, it either successfully findsa counterexample or verifies the lack of any counterexamplewith k transactions. ` e1→ χ1` e2→ χ2` e1:= e2 χ1:= χ2(Asgn)` e → χ` require(e) assume χ(Req)` e → χ` assert(e) assert χ(Asrt)` e → χ ` s1 ω1` s2 ω2` if (e) {s1} else {s2} if (χ) {ω1} else {ω2}(Cond)` e → χ ` s ω` while (e) do {s} while (χ) do {ω}(Loop)` er→ χr` ei→ χii = 0, . . . , n fresh v Cj<: Type(this) j = 1, . . . , mω ≡ if (τ[this] = C1) {call v := fC1(this, χ1, . . . , χn, msg_sender); χr:= v} else if . . .else if (τ [this] = Cm) {call v := fCm(this, χ1, . . . , χn, msg_sender); χr:= v}` er:= f(e1, . . . , en) ω(IntCall)` er→ χr` ei→ χii = 0, . . . , n fresh v Cj<: Type(e0) j = 1, . . . , mω ≡ if (τ[χ0] = C1) {call v := fC1(χ0, χ1, . . . , χn, this); χr:= v} else if . . .else if (τ [χ0] = Cm) {call v := fCm(χ0, χ1, . . . , χn, this); χr:= v}` er:= e0.f(e1, . . . , en) ω(ExtCall)` er→ χr` ei→ χii = 1, . . . , n fresh vω ≡ call v := New(); assume τ [v] = C; call fC0(v, χ1, . . . , χn, this); χr:= v` er:= new C(e1, . . . , en) ω(NewCont)` x[x.Length++] := e ω` x.push(e) ω(Push)` er→ χr` e → χ fresh v ` v[i] → χiω ≡ call v := New(); Length[v] := χ; assume ∀i :: χi= 0; χr:= v` er:= new t[](e) ω(NewArr)` s1 ω1` s2 ω2` s1; s2 ω1; ω2(Seq)` er→ χrfresh v ` v[i1] . . . [in] → χω ≡ call v := New(); call MapInit(v, n); assume ∀i1, . . . , in:: χ = 0; χr:= v` er:= new (t1⇒ . . . ⇒ tn⇒ t)() ω(NewMap)Fig. 9. Inference rules for encoding Solidity statements to Boogie statements.Type(e)is a function that returns the static type of Solidity expressione. SymbolfCdenotes the functionfin contractC, andfC0denotes the constructor of contractC. The<:relation represents the sub-typing relationship.τis a globalBoogie map that maps receiver objects to their dynamic types. Types for universally quantified Boogie variables are omitted for brevity.var Alloc : [ Ref]bool ;procedure New () returns (ret: Ref) {havoc ret; assume (!Alloc[ ret ]);Alloc[ ret] := true;}procedure NewUnbounded () {var oldAlloc : [ Ref] bool;oldAlloc := Alloc ; havoc Alloc ;assume ∀i::oldAlloc [i] ==> Alloc [i ];}procedure MapInit (v: Ref , n: int) {var j: int; j := 1; Length [v] := 0;while (j < n) {assume ∀i1, . . . , ij::Length[χ(v, i1, . . . , ij)]=0;assume ∀i1, . . . , ij::¬Alloc [χ(v, i1, . . . , ij)];call NewUnbounded ();assume ∀i1, . . . , ij::Alloc [χ(v, i1, . . . , ij)];assume ∀i1, . . . , ij, i0j::(ij= i0j) ∨ χ(v, i1, . . . , ij) 6= χ(v, i1, . . . , i0j);j := j + 1; }}Fig. 10. Auxiliary Boogie procedures. The termχ(v, i1, . . . , ij)denotes thetranslation result of Solidity expressionv[i1] . . . [ij]. Types for universallyquantified Boogie variables are omitted for brevity.V. EVALUATIONWe evaluate the effectiveness and efficiency of VERISOLby performing two sets of experiments on smart contractsshipped with Workbench: (i) semantic conformance checkingfor Workbench samples, and (ii) checking safety and securityproperties for the PoA governance contract. The goal of ourevaluation is to answer the following research questions:RQ1How does VERISOL perform when checking semanticconformance of Workbench application policies?RQ2How applicable is VERISOL on smart contracts withcomplex data structures (such as PoA)?Experimental Setup.Due to limited resources, we set ourtimeout as one hour for every benchmark. All experimentsare conducted on a machine with Intel Xeon(R) E5-1620 v3CPU and 32GB of physical memory, running the Ubuntu 14.04operating system.A. Semantic Conformance for Workbench Application PoliciesBenchmarks.We have collected all sample smart contracts thatare shipped with Workbench and their corresponding applica-tion policies on the Github repository of Azure Blockchain [5].These smart contracts and their policies depict various workflowscenarios that are representative in real-world enterprise usecases. The smart contracts exercise various features of Soliditysuch as arrays, nested contract creation, external calls, enumtypes, and mutual-recursion. For each smart contractCand itsapplication policyπ, we perform program instrumentation as TABLE IEXPERIMENTAL RESULTS OF SEMANTIC CONFORMANCE AGAINST WORKBENCH APPLICATION POLICIES.Name DescriptionOrig InstInit Status Status after Fix Time (s)SLOC SLOCAssetTransfer Selling high-value assets 192 444 Refuted Fully Verified 2.1BasicProvenance Keeping record of ownership 43 95 Fully Verified Fully Verified 1.5BazaarItemListing Multiple workflow scenario for selling items 98 175 Refuted Fully Verified 2.3DefectCompCounter Product counting using arrays for manufacturers 31 68 Fully Verified Fully Verified 1.3DigitalLocker Sharing digitally locked files 129 260 Refuted Fully Verified 1.7FreqFlyerRewards Calculating frequent flyer rewards using arrays 47 90 Fully Verified Fully Verified 1.3HelloBlockchain Request and response (Figure 1) 32 78 Fully Verified Fully Verified 1.3PingPongGame Multiple workflow for two-player games 74 136 Refuted Fully Verified (manual) 2.1RefrigTransport Provenance scenario with IoT monitoring 118 187 Fully Verified Fully Verified 2.2RoomThermostat Thermostat installation and use 42 99 Fully Verified Fully Verified 1.3SimpleMarketplace Owner and buyer transactions 62 118 Fully Verified Fully Verified 1.4Average - 79 159 - - 1.7explained in Section III-C to obtain contract C0. Note that noassertion failure ofC0is equivalent to the semantic conformancebetweenCandπ, so we include such instrumented smartcontracts in our benchmark set.Main Results.Table I summarizes the results of our firstexperimental evaluation. Here, the “Name” column gives thename of the contract, and the “Description” column describesthe contract’s usage scenario. The next two columns givethe number of lines of Solidity code before and after theinstrumentation described in SectionIII-C. The last threecolumns present the main verification results: In particular,“Init Status” shows the result of applying VERISOL on theoriginal smart contract, and “Status after Fix” presents theresult of VERISOL after we manually fix the bug (if any).The fix may require changing either the policy or the contract,depending on the contract author’s feedback. Finally, “Time”shows the running time of VERISOL in seconds when appliedto the fixed contracts.Our experimental results demonstrate that VERISOL isuseful for checking semantic conformance between Workbenchcontracts and the policies they are supposed to implement.In particular, VERISOL finds bugs in4of11well-testedcontracts and precisely pinpoints the trace leading to theviolation. Our results also demonstrate that VERISOL caneffectively automate semantic conformance proofs, as it cansuccessfully verify all the contracts after fixing the originalbug. Moreover, for10out of the11contracts with theexception ofPingPongGame, the invariant inference techniquessufficed to make the proofs completely push-button. Ourcandidate templates for contract invariant did not suffice for thePingPongGamecontract mainly due to the presence of mutuallyrecursive functions between two contracts. This required us tomanually provide a function summary for the mutually recursiveprocedures that states an invariant over the state variableswof the sender contract represented by themsg.sender(e.g.sw[msg.sender] = s1∨ sw[msg.sender] = s2wheresiarestates of the sender contract). This illustrates that we canachieve the power of the underlying sound Boogie modularverification to perform non-trivial proofs with modest manualfunction Accept () public{if ( msg. sender != InstanceBuyer &&msg. sender != InstanceOwner ) {revert ();}...if ( msg. sender == InstanceBuyer ) {...}else {// msg. sender has to be InstanceOwner// from the revert earlierif ( State == StateType . NotionalAcceptance ) {State = StateType . SellerAccepted ;}else if ( State == StateType . BuyerAccepted ) {// NON - CONFORMANCE : JSON transitions// to StateType . SellerAcceptedState = StateType . Accepted ;}}...}Fig. 11. Buggy function Accept of AssetTransfer.overhead. We are currently working on extending the templatesfor contract invariant inference to richer templates for inferringpostconditions for recursive procedures.Bug Analysis.We report and analyze the five bugs thatVERISOL found in the Azure Blockchain Workbench samplecontracts. These bugs can be categorized into two classes: (i)incorrect state transition, and (ii) incorrect initial state. Webriefly discuss these two classes of bugs.Incorrect state transition. This class of bugs arises whenthe implementation of a function in the contract violates thestate transition stated by the policy. VERISOL has found suchnon-conformance in theAssetTransferandPingPongGamecontracts. For instance, let us considerAssetTransfer4as aconcrete example. In this contract, actions are guarded by themembership ofmsg.senderwithin one of the roles or instancerole variables (see Figure 11). VERISOL found the transition4https://github.com/Azure-Samples/blockchain/tree/master/blockchain-workbench/application-and-smart-contract-samples/asset-transfer from stateBuyerAcceptedto stateAcceptedin theAcceptfunction had no matching transitions in the policy. Specif-ically, the policy allows a transition fromBuyerAcceptedtoSellerAcceptedwhen invoking the functionAcceptandmsg.senderequals the instance role variableInstanceOwner.However, the implementation of functionAccepttransitionsto the stateAcceptedinstead ofSellerAccepted. Fromthe perspective of the bounded verifier, this is a fairly deepbug, as it requires at least 6 transactions to reach the stateBuyerAccepted from the initial state.Incorrect initial state. This class of bugs arises when the initialstate of a smart contract is not established as instructed by thecorresponding policy. We have found such non-conformanceinDigitalLockerandBazaarItemListing. For instance,the policy ofDigitalLockerrequires the initial state of thesmart contract to beRequested, but the implementation endsup incorrectly setting the initial state toDocumentReview. IntheBazaarItemListingbenchmark, the developer fails toset the initial state of the contract despite the policy requiringit to be set to ItemAvailable.B. Security Properties of PoA Governance ContractIn this section, we discuss our experience applying VERISOLto PoA governance contracts. We first give some backgroundon PoA and then discuss experimental results.Background on PoA governance contracts.In additionto application samples, Workbench also ships a core smartcontract that constitutes an integral part of the Workbenchsystem stack. PoA is an alternative to the popular Proof-of-Work (PoW) consensus protocol for permissioned blockchains,which consist of a set of nodes running the protocol andvalidating transactions to be appended to a block that will becommitted on the ledger [9]. Validators belong to differentorganizations, where each organization is represented by anadministrator. The protocol for admin addition, removal, voting,and validator set management is implemented as the PoAgovernance contract. It implements the Parity Ethereum’sValidatorSet contract interface and is distributed on the AzureBlockchain github [8]. The smart contract consists of fivecomponent contracts (ValidatorSet,SimpleValidatorSet,AdminValidatorSet,Admin,AdminSet) totaling around 600lines of Solidity code. The correctness of the PoA governancecontract underpins the trust on Workbench as well the rest ofAzure Blockchain offering.The smart contract uses several features that make it achallenging benchmark for Solidity smart contract reasoning.We outline some of them here:•The contracts use multiple levels of inheritance since thetop-level contractAdminValidatorSetderives from thecontractSimpleValidatorSetwhich in turn derives fromValidatorSet interface.•It uses sophisticated access control using Solidity modifiers torestrict which users and contracts can alter states of differentcontracts.•The contracts maintain deeply nested mappings and arraysto store the set of validators for different admins.•The contracts use nested loops and procedures to iterateover the arrays and use arithmetic operations to reason aboutmajority voting.Properties.We examined three key properties of the PoAcontract:P1: At least one admin: The network starts out with a singleadmin at bootstrapping, but the set of admins shouldnever become empty. If this property is violated, theentire network will enter into a frozen state where anysubsequent transaction will revert.P2: Correctness of AdminSet: TheAdminSetis a contractthat exposes a set interface to perform constant timeoperations such as lookup. Since Solidity does notpermit enumerating all the keys in a mapping, the setis implemented as a combination of an array of membersaddressListand a Boolean mappinginSetto mapthe members to true. The property checks the couplingbetween these two data structures — (i)addressListhas no repeated elements, (ii)inSet[a]is true iff thereis an index j such that addressList[j] == a.P3: Element removal: Deleting an element from an arrayis a commonly used operation for PoA contracts. PoAcorrectness relies on invoking this procedure only for anelement that is a member of the array.Bugs found.To check the three correctness properties (P1),(P2), (P3) described above, we first annotated the PoAgovernance contracts with appropriate assertions and thenanalyzed them using VERISOL. In addition to uncovering apreviously known violation of the “at least one admin” property,VERISOL identified a few other bugs that have been confirmedand fixed by the developers. In particular, VERISOL found abug that results in the violation of property (P3): When anadmin issues a transaction to remove a validatorxfrom itslist of validators, a call to eventInitiateChangewill beemitted after removingx(usingdeleteArrayElement). Topersist the change, another call tofinalizeChangeis needed.However, the implementation actually allows two consecutivecallsInitiateChangewithout a call tofinalizeChange.As a result, this bug can result in the PoA contract to fail toremove validators that are initiated to be removed.In addition to the manually-added assertions that check thethree afore-mentioned properties, the PoA governance contractscontain additional assertions that were added by the originaldevelopers. Interestingly, VERISOL also found violations ofthese original assertions. However, these assertion failureswere due to developers mistakenly usingassertinstead ofrequire. Although bothrequireandassertfailures revertan execution, Solidity recommends usingassertonly forviolations of internal invariants that are not expected to failat runtime. VERISOL found five such instances of assertionmisuse. Unbounded verification.Unlike the semantic conformancechecking problem for client contracts, verifying properties (P1),(P2), (P3) of the PoA contracts requires non-trivial quantifiedinvariants and reasoning about deeply nested arrays. Thus, weattempted semi-automated verification of the PoA contracts bymanually coming up with contract/loop invariants and methodpre- and post-conditions. In addition, inductive proof of some ofthe properties also requires introducing ghost variables that arenot present in the original code. Fully automated verification ofthese properties in PoA governance contracts is an ambitious,yet exciting area for future work.VI. RELATED WORKIn this section, we discuss prior work on ensuring thesafety and security of smart contracts. Existing techniques forsmart contract security can be roughly categorized into variouscategories, including static approaches for finding vulnerablepatterns, formal verification techniques, and runtime checking.In addition, there has been work on formalizing the semanticsof EVM in a formal language such as theKFramework [20].Finally, there are several works that discuss a survey andtaxonomy of vulnerabilities in smart contracts [13], [26], [28].Static analysis. The set of static analysis tools are based ona choice of data-flow analysis or symbolic execution to findvariants of known vulnerable patterns. Such patterns include theuse of reentrancy, transaction ordering dependencies, sendingether to unconstrained addresses that may lead to lost ether, useof block time-stamps, mishandled exceptions, callingsuicideon an unconstrained address, etc. Tools based on symbolicexecution include Oyente [26], MAIAN [28], Manticore [10],and Mythril++ [11]. On the other hand, several data-flowbased tools also exist such as Securify [29] and Slither [12].Finally, the MadMax tool [18] performs static analysis tofind vulnerabilities related to out-of-gas exceptions. Thesetools neither check semantic conformance nor verify assertions.Instead, they mostly find instances of known vulnerable patternsand do not provide any soundness or completeness guarantees.On the other hand, VERISOL does not reason about gasconsumption since it analyzes Solidity code, and it also needsthe vulnerabilities to be expressed as formal specifications.Formal verification. F* [15] and Zeus [21] use formal verifi-cation for checking correctness of smart contracts. These ap-proaches translate Solidity to the formal verification languagesof F* and LLVM respectively and then apply F*-based verifiersand constrained horn clause solvers to check the correctnessof the translated program. Although the F* based approachis fairly expressive, the tool only covers a small subset ofSolidity without loops and requires substantial user guidanceto discharge proofs of user-specified assertions. The designof Zeus shares similarities with VERISOL in that it translatesSolidity to an intermediate language and uses SMT basedsolvers to discharge the verification problem. However, thereare several differences in the capabilities of the two works.First, one of the key contributions of this paper is the semanticconformance checking problem for smart contracts, whichZeus does not address. Second, unlike our formal treatmentof the translation to Boogie, Zeus only provides an informaldescription of the translation to LLVM and does not define thememory model in the presence of nested arrays and mappings.Unfortunately, we were unable to obtain a copy of Zeus totry on our examples, making it difficult for us to perform anexperimental comparison for discharging assertions in Soliditycode.Other approaches. In addition to static analyzers and formalverification tools, there are also other approaches that enforcesafe reentrancy patterns at runtime by borrowing ideas fromlinearizability [19]. Another work that is related to this paperis FSolidM [27], which provides an approach to specify smartcontracts using a finite state machine with actions written inSolidity. Although there is a similarity in their state machinemodel with our Workbench policies, they do not consideraccess control, and the actions do not have nested procedurecalls or loops. Finally, the FSolidM tool does not provide anystatic or dynamic verification support.VII. CONCLUSIONIn this work, we described one of the first uses of automatedformal verification for smart contracts in an industrial setting.We provided formal semantics to the Workbench applicationconfiguration, and performed automatic program instrumenta-tion to enforce such specifications. We described a new formalverification tool VERISOL using the Boogie tool chain, andillustrated its application towards non-trivial smart contractverification and bug-finding. For the immediate future, we areworking on adding more features of the Solidity language thatare used in common enterprise workflows and exploring moresophisticated inference for inferring more complex contractinvariants.REFERENCES[1]Explaining the dao exploit for beginners in solid-ity. https://medium.com/\spacefactor\@m{}MyPaoG/explaining-the-dao-exploit-for-beginners-in-solidity-80ee84f0d470,2016.[2]Solidity: Function modifiers. https://solidity.readthedocs.io/en/v0.4.24/structure-of-a-contract.html#function-modifiers, 2016.[3]Azure blockchain. https://azure.microsoft.com/en-us/solutions/blockchain/, 2017.[4]Parity: The bug that put $169m of ethereum on ice? yeah, it was on thetodo list for months. https://www.theregister.co.uk/2017/11/16/parity_flaw_not_fixed, 2017.[5]Applications and smart contract samples for workbench.https://github.com/Azure-Samples/blockchain/tree/master/blockchain-workbench/application-and-smart-contract-samples, 2018.[6]Azure blockchain content and samples. https://github.com/Azure-Samples/blockchain, 2018.[7]Azure blockchain workbench. https://azure.microsoft.com/en-us/features/blockchain-workbench/, 2018.[8]Ethereum on azure. https://github.com/Azure-Samples/blockchain/tree/master/ledger/template/ethereum-on-azure, 2018.[9]Ethereum proof-of-authority on azure. https://azure.microsoft.com/en-us/blog/ethereum-proof-of-authority-on-azure/, 2018.[10] Manticore. https://github.com/trailofbits/manticore, 2018.[11]Mythril classic: Security analysis tool for ethereum smart contracts.https://mythril.ai, 2018.[12]Slither, the solidity source analyzer. https://github.com/trailofbits/slither,2018. [13]Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli. A survey ofattacks on ethereum smart contracts (sok). In Principles of Security andTrust - 6th International Conference, POST , Uppsala, Sweden, April22-29, 2017, Proceedings, pages 164–186, 2017.[14]Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, andK. Rustan M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In Formal Methods for Components and Objects, 4thInternational Symposium, FMCO 2005, Amsterdam, The Netherlands,November 1-4, 2005, Revised Lectures, pages 364–387, 2005.[15]Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, AnithaGollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, AseemRastogi, Thomas Sibut-Pinote, Nikhil Swamy, and Santiago ZanellaBéguelin. Formal verification of smart contracts: Short paper. InProceedings of the 2016 ACM Workshop on Programming Languagesand Analysis for Security, PLAS@CCS 2016, Vienna, Austria, October24, 2016, pages 91–96, 2016.[16]ComputerWorld. Blockchain to generate morethan $10.6b in revenue by 2023. https://www.computerworld.com/article/3237465/enterprise-applications/blockchain-to-generate-more-than-106b-in-revenue-by-2023.html.[17]Cormac Flanagan and K Rustan M Leino. Houdini, an annotationassistant for esc/java. In International Symposium of Formal MethodsEurope, pages 500–517. Springer, 2001.[18]Neville Grech, Michael Kong, Anton Jurisevic, Lexi Brent, BernhardScholz, and Yannis Smaragdakis. Madmax: surviving out-of-gasconditions in ethereum smart contracts. PACMPL, 2(OOPSLA):116:1–116:27, 2018.[19]Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky,Noam Rinetzky, Mooly Sagiv, and Yoni Zohar. Online detection ofeffectively callback free objects with applications to smart contracts.PACMPL, 2(POPL):48:1–48:28, 2018.[20]Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues, Xiaoran Zhu,Philip Daian, Dwight Guth, Brandon M. Moore, Daejun Park, Yi Zhang,Andrei Stefanescu, and Grigore Rosu. KEVM: A complete formalsemantics of the ethereum virtual machine. In 31st IEEE ComputerSecurity Foundations Symposium, CSF 2018, Oxford, United Kingdom,July 9-12, 2018, pages 204–217, 2018.[21]Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma. ZEUS:analyzing safety of smart contracts. In 25th Annual Network and Dis-tributed System Security Symposium, NDSS 2018, San Diego, California,USA, February 18-21, 2018, 2018.[22]Shuvendu Lahiri and Shaz Qadeer. Complexity and algorithms formonomial and clausal predicate abstraction. In International Conferenceon Automated Deduction (CADE ’09). Springer Verlag, March 2009.[23]Shuvendu K. Lahiri, Shaz Qadeer, Juan P. Galeotti, Jan W. Voung, andThomas Wies. Intra-module inference. In Computer Aided Verification,21st International Conference, CAV 2009, Grenoble, France, June 26 -July 2, 2009. Proceedings, pages 493–508, 2009.[24]Akash Lal, Shaz Qadeer, and Shuvendu K. Lahiri. A solver forreachability modulo theories. In Computer Aided Verification - 24thInternational Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012Proceedings, volume 7358, pages 427–443. Springer, 2012.[25]K. Rustan M. Leino. Efficient weakest preconditions. Inf. Process. Lett.,93(6):281–288, 2005.[26]Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and AquinasHobor. Making smart contracts smarter. In Proceedings of the 2016ACM SIGSAC Conference on Computer and Communications Security,Vienna, Austria, October 24-28, 2016, pages 254–269, 2016.[27]Anastasia Mavridou and Aron Laszka. Tool demonstration: Fsolidm fordesigning secure ethereum smart contracts. In Principles of Securityand Trust - 7th International Conference, POST 2018, Held as Part ofthe European Joint Conferences on Theory and Practice of Software,ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings,pages 270–277, 2018.[28]Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Prateek Saxena, and AquinasHobor. Finding the greedy, prodigal, and suicidal contracts at scale.In Proceedings of the 34th Annual Computer Security ApplicationsConference, ACSAC 2018, San Juan, PR, USA, December 03-07, 2018,pages 653–663, 2018.[29]Petar Tsankov, Andrei Marian Dan, Dana Drachsler-Cohen, ArthurGervais, Florian Bünzli, and Martin T. Vechev. Securify: Practicalsecurity analysis of smart contracts. In Proceedings of the 2018 ACMSIGSAC Conference on Computer and Communications Security, CCS2018, Toronto, ON, Canada, October 15-19, 2018, pages 67–82, 2018.