Cosimo Laneve
email: cosimo.laneve@unibo.it

Claudio Sacerdoti Coen

On the prediction of smart contracts' behaviours

Smart contracts are pieces of software stored on the blockchain that control the transfer of assets between parties under certain conditions. In this paper we analyze the bahaviour of smart contracts and the interaction with external actors in order to maximize objective functions. We define a core language of programs with a minimal set of smart contract primitives and we describe the whole system as a parallel composition of smart contracts and users. We therefore express the system behaviour as a first logic formula in Presburger arithmetics and study the maximum profit for each actor by solving arithmetic constraints.

Introduction

Smart contracts are programs that run on distributed networks with nodes storing a common state in the form of a blockchain. These programs are gaining more and more interest because they implement the so-called decentralized applications, which are applications that can handle and transfer assets of considerable value (usually, in the form of cryptocurrency like Bitcoin). Several decentralized applications have already been applied to asset management scenarios ranging from food supply chain management to energy market management and to identity notarization. The smart contracts of such applications are written in programming languages that are targeted to different blockchains. Two such languages are Solidity for Ethereum (which is imperative) [START_REF][END_REF] and Liquidity for Tezos (which is functional) [START_REF] Ocamlpro | Welcome to Liquidity's documentation![END_REF].

Decentralized applications consist of smart contracts and users, such as humans performing either computer actions or physical ones. Since they run on systems that have no coercing central authority, the uncertainty of the overall emerging behaviour is very high and this is a critical issue when asset movements are at the core of applications. Therefore it becomes important to understand the protocols between interacting parties and, when possible, use smart contracts to regulate behaviours of users that systematically try to maximize their revenues or to minimize losses. For example, a client behaves in different ways in order to minimize the cost κ of a good (e.g. he may choose one company or another). On the other hand, the interacting company tries to maximize its revenue; therefore it strives for the greatest value κ such that the client has still a convenience in acquiring its own good. Determining the least value κ is complex because it may not only depend on the price, but also on the trademark, the delivery type, etc.

In this paper, to suitably address the foregoing issues, (i ) we adhere to a formal modelling approach, (ii ) define an analysis technique and (iii ) prototype the verification process. A precise account of the work follows.

As regards the formal modelling, since (human) users and smart contracts act concurrently and independently, we adopt methods and techniques from the domain of process algebras. As such, we depart from most of the literature on application of formal methods to smart contracts that study their properties as sequential programs. In Section 2 we introduce a unified calculus of actors -both contracts and users, the scl calculus -that is expressive enough (it is Turing complete) and features method invocations, field updates, conditional behaviour, recursion and failures. According to the semantics of scl, systems, which are parallel compositions of smart contracts and users, perform transactions, e.g. sequences of smart contract operations that are triggered by users. Transactions may return a value or may fail; in the first case the states of smart contracts that have taken part in the transaction are committed; in the second case the states backtrack to the last committed one. In parallel to transactions, users may evolve internally in a nondeterministic way (on the contrary, smart contracts' behaviours are deterministic). The model of scl is a transition system that enables symbolic analysis of properties -see Section 3. In particular, transitions retain two informations: one is a standard label, say µ, highlighting the action performed, the other one, say ψ, is a formula that records the choices and the guards of conditionals. The two labels play different roles in our analysis technique.

Given the model of a scl program, in Section 4 we define an objective function as a map from labels µ to integer expressions. For example, such function may return 1 if the label has a given type, or it may return some expression on the symbolic names occurring in the label. In general we are interested in determining computations that maximize or minimize the sum of the values of an objective function on their labels and in selecting strategies that allow users to behave correspondingly. Once this is done, we analyze whether tuning up and down the symbolic names may generate more profit or reduce loss for one interacting party. To this aim, we select a sensible state S and the corresponding transition system rooted at S (we assume there is no cycle and that the transition system is finite). By means of the labels µ and ψ of the transitions, we define a first order logic formula, called the characteristic formula, that summarizes the transition system describing concisely the values of the objective function for every possible run.

When the model is Presburger (a decidable fragment of arithmetics where formulas contains only integer numbers, equality, strict inequality, addition and multiplication by a constant), the characteristic formula belongs to an extension of Presburger arithmetics that can be decided via quantifier elimination. The formula without quantifiers allows us to reason about strategies that bring to goals with higher values (e.g. maximize the profit) for each actor by solving arithmetic constraints. The general cases of infinite, acyclic models are addressed in our technique by analyzing finite unfoldings.

We are currently terminating the implementation in OCaml of a tool that, given a set of contracts, an initial state and an objective function, automatically extracts the open model, computes the characteristic formula and applies quantifier elimination over it. This elimination step also checks whether the formula is satisfiable, i.e. it detects the reachable final states and computes the set of values of the objective function that can be observed in runs that lead to them. These sets are represented as linear mappings over domains that are union of polytopes, i.e. solutions of a systems of linear inequations in normal form. The inequations constrain the choices that users can take according to those of other users or to external inputs to the system. Maximizing linear functions over linear inequations is mathematically trivial.

We conclude in Section 5 by discussing future research directions.

Related works. In the past few years formal methods have been largely used to analyze smart contracts with the aim of verifying the security of potentially dangerous compositions with untrusted codes. One of the most cited motivation has been the famous TheDAO attack [START_REF] Siegel | Understanding the dao attack[END_REF] that stole several million dollars during a crowdfunding procedure and caused an hard fork in the Ethereum blockchain. An initial contribution is [START_REF] Bhargavan | Formal verification of smart contracts: Short paper[END_REF], which proposes an analysis framework based on a compilation of Solidity to F * , a functional language aimed at program verification with a powerful type and effect system. Using F * types, they are able to trace Ethers (the Ethereum cryptocurrency) and discover critical patterns in smart contracts. A different technique has been followed by [START_REF] Luu | Making smart contracts smarter[END_REF] and [START_REF] Mueller | Smashing Ethereum smart contracts for fun and real profit[END_REF], sticking to symbolic execution. Similarly to our technique, they use symbolic values for inputs and study symbolic computations by mean of the formula that accumulates the constraints on the inputs. This formula is different from our characteristic formula in Section 4. In particular, while our formula describes every possible computation and we use constraints on symbols to determine values that maximize some quantity, in [START_REF] Luu | Making smart contracts smarter[END_REF] and [START_REF] Mueller | Smashing Ethereum smart contracts for fun and real profit[END_REF], they are interested in discovering critical patterns of a single computation.

In the same line of verifying and validating smart contracts, the contribution [START_REF] Bigi | Validation of decentralised smart contracts through game theory and formal methods[END_REF] combines formal methods and game theory to analyze protocols that also involve players (human users) with different/competing gaming strategies. The technique is the following: game theory is used to analyze the behaviour of the players in the protocol, then the resulting strategies are modelled in a probabilistic system for automated validation. Our approach is somehow the opposite: we define the overall system (or part of it) in a formal model and derive the strategies by analyzing the model. In this paper, we stick to a discrete model (the choice operator in users' behaviours is not probabilistic), leaving to future research the extension to stochastic models.

Another contribution that is close to our one is [START_REF] Chatterjee | Quantitative analysis of smart contracts[END_REF]. In this case, the authors define a simplified language for smart contracts that is loop-free. Then they pro-vide an automatic translation into stateful concurrent games and analyze these games by means of interval abstraction that is demonstrated to be sound. The technique is very powerful and of practical relevance, considering that models of concurrent games are very large. Unlike to this work, our modelling technique is based on process algebra and our analysis relies on Presburger arithmetics formulae. The evaluation of the practical relevance of our technique is postponed to future research.

The calculus of smart contracts

In this section we define a core language of programs featuring a minimal set of smart contract primitives, such as method invocations, field updates, conditional behaviour, recursion and failures.

We use a countable set of variables, ranged over by x, y, z, a countable set of smart contract names, ranged over by a, b, c, and a countable set of user names, ranged over by id , id , id . Smart contract names and user names are generically addressed by α, α , . . . and we assume they are partitioned into disjoint sets such that names of a same set belong to a same class and those in different sets belong to different classes. The property that a name α belongs to a class C is expressed by α ∈ C.

Classes C have the form C : (F , M ) where F is a sequence of field definitions T f, M is a sequence of method definitions T m(T x){ s m } with T x and s m respectively being the formal parameters and the body of m. In the whole paper, we assume that sequences of declarations T x and method declarations M do not contain duplicate names. Types T are either naturals Nat or names α. Hereafter we write k for possibly empty, finite sequences k 1 , . . . , k n of various entities.

The syntax of statements, rhs-expressions and expressions is given in Figure 1. A statement s may be either a return of an expression, or a field update (plus a continuation), or a conditional or the nondeterministic choice s + s . We assume that bodies of smart contract methods (i ) do not have nondeterministic choice (they are deterministic) and (ii ) do not have expressions with fail, except for return fail.

A rhs-expression z may be either an expression e or a synchronous method invocation. An expression e may be either a standard expression or fail. In e op e , op is a standard operation on naturals. We assume that method bodies of users also have the expression isfailed(e) that returns 1 if the value of e is fail, 0 otherwise.

The semantics of scl statements is defined by a transition relation

α : s, µ -→ ψ s ,
where s and s , with an abuse of notation, are runtime statements, and are memories, e.g. maps from field names to values v, µ is either empty or v.m(v ), and ψ is a formula. The transition means that executing s in an actor α with a memory amounts to produce an action µ and a formula ψ and executing s in States and runtime statements:

::= [• • • , f → v, • • • ] (memories) v ::= naturals | α | fail (values) s ::= • • • | 0 | id | id[v] | α.f = •;s | s;s | s + x s (runtime statements) runtime statement transition µ -→
ψ (µ may be empty or α; ψ is a formula):

[upd] e α, = v α : α.f = e;s, -→ true s, [f → v] [meth] e α, = v e α, = v fail / ∈ v, v v ∈ C m(x) = sm ∈ C s = sm{ v ,v / x,this } α : α.f = e.m(e );s, v.m(v ) -→ true s ;α.f = •;s, [meth-fail] e id, = v e id, = v fail ∈ v, v id : id.f = e.m(e );s, -→ true s, [f → fail] [return] e α, = v α : return e;s, -→ true s[v], [if-true] e α, = 0
α : if e then s else s ;s , -→ true s;s , [if-false] e α, = 0
α : if e then s else s ;s , -→ true s ;s , [fix]
x fresh . Actions µ are commitments to the context, formulas ψ are essential for our analysis in the next sections.

id : (s1 + s2);s, -→ true (s1 + x s2);s, [choice] i ∈ {1, 2} id : (s1 + x s2);s, -→ x=i si;s,
Runtime statements, as reported in Figure 1, extend statements with 0 representing termination, id recording the user that initiated the transaction, id [v] returning a value to the user id , α.f = •;s representing a continuation waiting for a value that will replace the symbol •, with s;s denoting the sequential composition, and s + x s , an alternative form of s + s that retains the fresh variable to be used for recording the choice (this information is necessary in the analysis of Section 4). Sequential composition is considered associative.

The following auxiliary functions are used in the semantic rules:

-[f → v] is the memory update, namely ( [f → v])(f) = v and ( [f → v])(g) = (g), when g = f.
-s[v] is the delivery of a value v to a runtime statement s, namely

s[v] def =              α.f = v;s if s = α.f = •;s and v = fail id .f = fail;s if s = id .f = •;s and v = fail id [fail] if s = a.f = •;s ;id and v = fail id [v] if s = id
It is worth to observe that (α.f = •;s )[fail] behaves in different ways according to α being a user or a smart contract. In the first case the field of the user is updated with fail -which is possible for users -, in the second case the whole statement fails and the failure is reported to the user that triggered the whole transaction. -e α, is a partial function that returns the value of e. The value of fields of α is retrieved in the memory of α: α.f α, = (f). The function is undefined if e tries to use fields of an actor = α. We omit the definition of e α, when e is an operation, but we require that it must be fail when one of the arguments is fail. e α, returns the tuple of values of e.

Let us comment some semantic rules in Figure 1. Rule [upd] defines the semantics of a field update: the expression e is evaluated in an actor α with a memory ; the resulting memory binds the value to the field f. Rule [meth] defines method invocations α.f = e.m(e );s when the evaluation of e and e does not return a failure. In this case, the method dispatch is performed by using the value v of the carrier (because every name belongs to a class) and the statement to evaluate becomes the instance of the body of m, followed by the update α.f = •, where • represents a place-holder, and the continuation s. The transition is labelled

v.m(v )
-→ true meaning that we are invoking the method m of actor v with actual parameters v . Rule [meth-fail] addresses failures in the evaluation of expressions of a method invocation; in this case the invocation is not performed and the field is updated with fail. Rule [return] defines the semantics of return e. There are two types of return continuations s: one is α.f = •;s -see rule [meth] -, the other one is id (this will be clear in the semantics of scl programs). Additionally, the semantics depends on whether α is a smart contract or a user, and on whether the value v is a failure or not. To manage all these cases we use the auxiliary function s [v]. The semantics of conditionals is standard. On the contrary, the semantics of nondeterminism is not standard and deserves few comments. First of all, nondeterminism may only occur in user codes, therefore the actor here is id . Then, we need to keep track of the nondeterministic choices in order to study the behaviour of smart contract programs. To this aim we use a fresh variable x each time a choice is about to be performed and (s 1 + s 2 );s transits into an intermediate statement (s 1 + x s 2 );s. In turn this statement becomes either s 1 ;s or s 2 ;s and the choice is recorded by letting x = 1 or x = 2 in the formula labelling the transition, respectively.

States:

S ::= s | a( • ) | id( , s) | S | S (states)
Auxiliary functions commit(•) and backtk (•) (the two functions are homomorphic with respect to |):

commit(s) = s commit(a( • )) = a( • ) commit(id( , s)) = id( , s) backtk (s) = s backtk (a( • )) = a( • ) backtk (id( , s)) = id( , s) State transition µ -→
ψ (µ may be empty, α, or fail; ψ is a formula):

[sc-move] a : s, -→ ψ s , a( • ) | s -→ ψ a( • ) | s [id-move] id : s, -→ ψ s , id( , s) -→ ψ id( , s ) [invk] a : s, a .m(v) -→ ψ s , a = a a( • ) | a ( • ) | s -→ ψ a( • ) | a ( • ) | s [invk-self] a : s, a.m(v) -→ ψ s , a( • ) | s -→ ψ a( • ) | s [invk-sc] id : s, a.m(v) -→ ψ s ;id.f = •;s , • / ∈ s id( , s) | a( • ) | 0 -→ ψ id( , id.f = •;s ) | a( • ) | s ;id [invk-id-self] id : s, id.m(v) -→ ψ s , id( , s) -→ ψ id( , s ) [end-ok] v = fail id( , s) | id[v] -→ true id( , s[v]) | 0 [end-fail] id( , s) | id[fail] fail -→ true id( , s[fail]) | 0 [cmt] S -→ ψ S S | S -→ ψ commit(S ) | S [bkt] S fail -→ ψ S S | S fail -→ ψ backtk (S ) | S [tau] S -→ ψ S S | S -→ ψ S | S
Fig. 2. Semantics of scl.

Semantics of scl programs

A smart contract program is a pair D, S , where D is a finite set of class definitions and S is state. States, as defined in Figure 2, are parallel composition of actors a( • ), called smart contracts, or actors id ( , s), called users, and exactly one runtime statement, called blockchain-statement. Smart contracts have pairs of memories • where is the current memory and is the last committed memory. In case of commits, the current memory becomes the last committed memory; in case of failures, the system will backtrack by restoring . In a state, names a and id are unique. As usual, parallel composition in states is associative and commutative. The semantics of a smart contract program is defined by means of transition relation S States may evolve in two ways: either by a transition of the blockchainstatement or by a transition of a user.

The blockchain-statement may evolve because of an empty-labelled statement transition -rule [sc-move] -or because of a method invocations of a smart contract -see rules [invk] and [invk-self]. In this last case, the state must contain the smart contract whose method is invoked in the label of the transition. Users have a behaviour, which is modelled by a runtime statement, and evolve concurrently either with empty-labelled transitions -rule [id-move] -or with selfinvocations -rule [invk-id] (therefore a user cannot invoke another user, e.g. user interactions are always mediated by a smart contract). When the blockchainstatement is 0, a user may invoke a smart contract's method -rule [invk-sc]. This is the only way to start a blockchain transaction and, in this case, in order to return the result to the caller, method's body is suffixed with user's name. The transaction terminates either successfully returning a not-fail value to the user that triggered it -rule [end-ok] -or with a failure -rule [end-fail]. In the first case, the smart contracts that were involved in the transaction are committed -rule [cmt] -, e.g. their current local memory is saved; in the second case the smart contracts backtrack -rule [bkt] -e.g. their current memory is deleted and the current one becomes the last memory that has been committed. Backtrack and commit are defined by the auxiliary functions backtk (•) and commit(•) in Figure 2.

We conclude by noticing that blockchain-statements are executed sequentially and in a deterministic way (because they originated in smart contracts' methods). On the contrary, users' method are performed concurrently and are nondeterministic (because the operator + may occur in their code).

Example 1. We use a simple example to illustrate the technicalities we have introduced. The example is about garbage collection and defines the interactions between a citizen and a smart bin. In particular, a citizen gets rid of the garbage in two ways: either throwing the garbage bags into a smart bin or dumping it (littering the street, for instance). The throwing in the bin is performed by invoking a method "throw"; this invocation returns a natural value that corresponds to a cash prize for having behaved well. If the garbage bag is dumped, the prize is 0. Every two garbage bags, the cash owned by the citizen is deposited in his bank account (in order to reduce his overall garbage taxes). The classes of the citizen and of the smart bin are displayed in Figure 3 (notice that the citizen is a user, while the bin is a smart contract). For simplicity, the management of failures has been removed by the codes of Figure 3. The smart bin class has a method throw whose behaviour depends on the value of the field h. When h is 0, two bags can be taken: the field h is set to 1 and a prize k is returned to the citizen, subtracting it from the field a that represents the money hold by the bin. When the second bag arrives, a value k is returned to the citizen (notice that k may be different from k ), after having re-charged the field a and asked to the truck to empty the bin, re-setting h to 0.

Let us discuss a possible state and its transitions. Let man ∈ Citizen, bin ∈ Garbage bin, bank ∈ Bank and truck ∈ Truck. We assume that Bank has methods deposit and withdraw (with the obvious meanings); Truck has a method empty that empties the bin and returns 0. Let also

m = [v 1 → 0, v 2 → 0, tmp → 0] b = [h → 0, a → k + k, tmp → 0] s = man.tmp = man.behaviour(bin, bank );return 0 S = man( m , s) | bin( b • b ) | bank ( • ) | truck ( • ) | 0 We have S -→ true man( m , s ) | bin( b • b ) | bank ( • ) | truck ( • ) | 0
where s = s bh ;man.tmp = •;return 0 and s bh is the body of behaviour with the instantiation { bin,bank ,man / bin,bank,this }. In this state, s bh may evolve either by invoking bin.throw() (throwing the garbage into the bin) or by updating v 1 to 0 (illegal dumping of garbage). Let us discuss the first alternative, which is more interesting. Therefore, let s = s bh ;man.tmp = •;return 0, where s bh = man.v1 = •;(man.v2 = bin.throw();CONT + man.v2 = 0;CONT) Then we have the following transitions (x 1 and x 2 are two fresh variables for tracing the choices that has been done):

man( m , s ) | bin( b • b ) | bank ( • ) | truck ( • ) | 0 -→ true -→ x1=1 man( m , s bh ) | bin( b • b ) | bank ( • ) | truck ( • ) | s thw ;man -→ true 4 man( m , s bh ) | bin( b • b ) | bank ( • ) | truck ( • ) | man[k] -→ true man( m , s bh { k / • }) | bin( b • b ) | bank ( • ) | truck ( • ) | 0 -→ true -→ x2=1 man( m , s bh ) | bin( b • b ) | bank ( • ) | truck ( • ) | s thw ;man
where s thw is the instance of the body of throw with the name bin for this;

m = m [v 1 → k], b = b [h → 1, a → k ] and s bh = man.v2 = •;CONT. The continuation is omitted.

The open semantics and the analysis model

A decentralized application is never a closed system: smart contract's methods can always be invoked not only by users and the smart contracts designed to interact with them, but also by unknown actors. Therefore, to study properties of our systems, we need to analyse open configurations. In particular, we need to reason on invocations without any knowledge of the actual parameters of the caller. A standard solution of this problem is to use symbolic variables -see Figure 4 -, i.e. extending values with (unbound) variables and admitting that operators return terms, such as x + 1, in addition to integers and actor names. Therefore the evaluation function e α, may now return terms with symbolic variables and it follows that actor's fields may also record terms with symbolic variables.

The extensions of runtime statements transitions in Figure 1 and of state transitions in Figure 2 where the formulas of transitions report whether the guard is true ( = 0) or false (= 0). These formulas and those of the rule [choice] will enable the analysis of smart contract systems in Section 4.

As regards the open state transition, we extend the rules of Figure 2 with those for invoking a method of a unspecified smart contract -rules [invk-open] and [invk-open-id]. We discuss the former, the latter one is similar. The function • / ∈ s returns true if • does not occur in the runtime statement s (which is always the case when a method body is istantiated). This expedient is used to select in s ;a.f = •;s , a, the prefix representing the instance of method's body and to drop it because we don't want to analyze behaviours of unspecified actors. Henceforth, the rule delivers to the continuation either a symbolic variable or fail, therefore covering every possible output of the invocation.

Rule [input-open-sc] defines the invocation of a smart contract method by a hypothetical user. In this case, actual parameters are all fresh symbolic variables and the instance of method body is suffixed by the name of the hypothetical user. According to the returned value is fail or not, we will have a backtrack -rule The open transition system in Figure 4 defines a model that is a tuple (S, S 0 , T ), where S is a non-empty set of states, S 0 ∈ S is the initial state, and T ⊆ S × S × Θ × Ψ is the set of labelled transitions. The set Θ is the collection of labels {ε, fail, , v = a .m(v), id : z} (ε represents the empty label) while Ψ is a set of formulae. As usual

S 1 , S 2 , µ, ψ ∈ T is abbreviated into S 1 µ -→ ψ S 2 .
Actually, in Section 4 we use a slightly different model than the foregoing one, that we call analysis model. In the forthcoming analysis we need to deal with the constant fail. To this aim, in order to remain in Presburger arithmetics, we decided to encode fail by extending the Nat type to Integers. Henceforth fail is encoded by -1 and we use a function |ψ| replacing every occurrence of fail with -1 and turning every actor name into a (global) integer variable. We also extend labels Θ with a new label, written (x), which is meant to expose in the (µ may be empty, , fail, a.m(v), or id : z; ψ is a formula): An (analysis) model is finite if the set of states S is finite; it is a Presburger model if the set of conditions Ψ and the actual parameters used in Θ range respectively over Presburger formulas and Presburger expressions. We recall that Presburger arithmetics is the decidable subset of classical first order logic over integer numbers where the only predicates allowed are equality and (strict) inequality and the only function symbols are addition between integer expressions and multiplication of an integer expression by a constant.

[invk-open] a : s, a .m(v ) -→ true s ;a.f = •;s , • / ∈ s v either x fresh or fail S | a( • ) | s v=a .m(v ) -→ a / ∈S S | a( • ) | (a.f = •;s )[v] [invk-open-id] id : s, a.m(v ) -→ true s ;id.f = •;s , • / ∈ s v either x fresh or fail S | id( , s) v=a.m(v ) -→ a / ∈S S | id( , (id.f = •;s )[v]) [input-open-sc] id, z fresh a ∈ C m(x) = sm ∈ C s = sm{ z,a / x,this } S | a( • ) | 0 id:z -→ id / ∈S S | a( • ) | s ;id [end-open] v = fail S | id[v] -→ id / ∈S commit(S) | 0 [end-fail-open] S | id[fail] fail -→ id / ∈S backtk (S) | 0
Example 2. In Figure 5 we illustrate the analysis model of a citizen and a garbage bin discussed in Example 1. In order to have a more compact picture, we have collapsed empty-labelled transitions. We have also used a simple hack to have finite models: we have added an empty labelled transition from state 17 to state 1, even if they are not exactly equal as systems states. This is because the stack of the citizen grows at every call since we do not optimize tail recursion in the transition systems of Figure 2. However, our analyzer always performs these optimizations. We also remark that the two models are also Presburger models.

Due to lack of space, Figure 5 does not report the interactions between the citizen, the garbage bin and other actors. The complete model has a large number of states because of all possible interactions. In particular, every time the citizen wants to throw out her garbage, she can either succeed immediately -and in that case an empty labelled move is performed by the system via the [invk-sc] rule -or she can be pre-empted by an unknown id via the [input-open-sc] rule.

Observables and strategies

A user can behave in different ways and obtain different results because of the choice operator + that may occur in its code. In this section we study users' behaviours and how choices influence results in a sensible way.

-→ ψ1 • • • µn -→ ψn S n+1 , its ω-observation is 1≤i≤n ω(µ i ).
In Example 1, a citizen is interested into maximizing the amount of cash-back that is saved in the bank, i.e. its objective function called ω C , is defined as follows

ω C (µ) = v 1 + v 2 if µ = = bank.deposit(v 1 + v 2 ) 0 otherwise
We notice that the result of an objective function may be a term containing symbolic names. (As a consequence our analysis will enable programmers to design smart contracts with instances of symbolic names that support "optimal strategies" -see below.) Contrary to citizens, the city hall is interested on minimizing the amount of garbage dumped or, equivalently, to maximize the amount of garbage thrown in the bins. Thus its objective function ω H is defined as follows

ω H (µ) = 1 if µ = = bin.throw() 0 otherwise
A strategy is a function that determines the transition to perform in states where the next statement to execute is a choice. Since these decisions are taken by users, which only have a partial understanding of the state (every user has full visibility of its own state and of smart contracts' states, they cannot access the internal state of other users), in general, a user can only devise "sub-optimal" strategies. A strategy is optimal with respect to an objective function ω, if, for any other strategy, all the possible future computations (which follow by the behaviour of the other users involved) cannot yield a higher ω-observation. Users that, at any choice point, try to maximize some objective function are called rational. In the rest of the section we are interested into rational users.

In general we cannot expect the existence of optimal strategies, nor we can expect that a strategy that is optimal for a given objective function is also optimal for another objective function. For example, if we just analyze the model of our citizen in isolation (see Figure 5), we can only deduce the following facts about the pair of objective functions ω C , ω H , i.e. the first element observes the cash-back (according to the citizen objective function) and the second one the number of calls to throw() (according to the city hall objective function):

1. the strategy that dumps the garbage twice at each execution 1-17 yields the pair 0, 0 ; 2. the two strategies that dump the garbage once yield the pairs v 1 , 1 and v 2 , 1 respectively, for some v 1 , v 2 ; 3. the strategy that never dumps the garbage yield the pair

v 1 + v 2 , 2 , for some v 1 , v 2 .
Note that v 1 and v 2 are not fixed: a garbage bin may return different values at every invocation of throw(), depending on its own internal logic and on the interaction with other actors. From the point of view of the city hall, the optimal strategy for the citizen is clearly the last one. From the point of view of the citizen, instead, there is no optimal strategy: it depends on the behaviour of the garbage bin that is unknown since we are analyzing the citizen in isolation.

Here is where smart contracts enter into the picture. A smart contract is used to regulate interaction between (human) users. In many real world examples, the smart contract is designed so that the system obtained composing humans with contracts has two relevant properties: (i ) every user has an optimal strategy and (ii ) the optimal users' strategies also maximizes the objective function of the smart contract programmer. In Example 1, this second function is exactly ω H , that is the programmer aims at minimizing the garbage dumped by citizens. If we combine the citizen and the smart contract and we analyze again the model obtained, we realize that the garbage bin sometimes pays back k coins and sometimes k coins. In particular, the strategy of point 1 always yield 0, 0 , both strategies of point 2 sometimes yield k, 1 and sometimes k , 1 , while the strategy of point 3 can yield any pair of observations among k +k, 2 , k +k , 2 , k +k, 2 , k +k , 2 . It follows that the strategy of point 1 is clearly not optimal for the citizen, but the remaining three are incomparable because, for example, getting a k from one strategy frequently can be better than getting a k + k from another strategy.

Our analysis, however, suggests a simple solution to the programmer: if the programmer chooses k = k > 0, then the four strategies now yield the pairs 0, 0 , k, 1 , k, 1 , 2k, 2 . In this case, the last strategy is optimal both for the citizen and for the city hall. The same result can be obtained picking any value for k and k such that 0 < k < 2k < 4k, so that getting two cashbacks is always better than getting just one of them.

In the rest of the section, the analysis models will be acyclic and finite, namely models such that the transition relation has always finite maximal computations. These models can be obtained by unfolding cyclic models up to a certain depth. This makes sense in the context of smart contracts where the executions are always bound in the number of steps by some quantity called gas that is bought by the caller (a user) with the virtual currency of the blockchain [START_REF]Ethereum's white paper[END_REF]. It also makes sense in examples like Example 1 where the model is one big cycle; therefore it is sufficient to maximize the objective function over just one iteration of the loop.

Automatic analysis

We use an automatic technique to verify whether an analysis model retains optimal strategies for some objective function or whether maximizing some objective function -e.g. the cash-back to the citizen -implies the maximization of other objective functions -e.g. the amount of garbage thrown into smart bins. Given an objective function, our technique derives a first order logic formula specifying every possible observation with respect to unknown symbolic inputs and to the internal choices of every agent.

Let Q be the following map from labels to a possibly empty sequence of quantifiers:

Q((x)) = ∃x Q(x = a.m(v)) = ∀x Q(id : z) = ∀id ∀z Q(µ) = ε (otherwise)
Let also M = (S, S 0 , T ) be finite and acyclic and ω be an objective function.

The characteristic formula S 0 M ω is the first-order logic formula defined as follows when there is at least one transition S µ -→ ψ S ∈ T :

S M ω = S µ -→ ψ S ∈T Q(µ) ψ ∧ O(S, {ω(µ)}) ∧ S M ω ;
when there is no µ, ψ, S such that S µ -→ ψ S ∈ T (S is final):

S M ω =
where is the proposition "true".

The binary predicate O(S, A) in the characteristic formula is to be read as follows: there exists a computation originating from S that eventually leaves the state S observing one element of the set A. For example, O(13, {v 1 + v 2 }) means that there will be a transition from state 13 where the user observes v 1 + v 2 ; O(15, {2}) ∨ (O(12, {v 1 , v 2 }) means that either state 15 will be reached and left observing 2, or the state 12 will be reached and left observing either v 1 or v 2 .

In order to ease the reading, we simplify the characteristic formula as follows:

-G∧O(S, {0}) is simplified to G because observing 0 is useless for maximizing an objective function; -G ∧ is simplified to G; -∀x.G is simplified to G when x does not occur in G (similarly for ∃).

After these simplifications, the characteristic formula for the objective function ω C of the citizen (we remove the empty-labelled transition from state 17 to state 1 in Figure 5) is:

1 M ω C = ∃x x = 1 ∧ ∀v1∃y (y = 1 ∧ ∀v2 O(13, {v1 + v2})) ∨ (y = 2 ∧ O(14, {v1 + 0})) ∨ x = 2 ∧ ∃z z = 1 ∧ ∀v2 O(15, {0 + v2}) ∨ z = 2 ∧ O(16, {0 + 0}) (1)
The characteristic formula for the objective function ω H of the city hall instead is:

1 M ω H = ∃x x = 1 ∧ O(3, {1}) ∧ ∃y((y = 1 ∧ O(9, {1})) ∨ y = 2) ∨ x = 2 ∧ ∃z (z = 1 ∧ O(11, {1})) ∨ z = 2 (2)

Quantifier elimination

When the analysis model is Presburger, the characteristic formula belongs to the extension of Presburger arithmetics with the observation predicate O(S, A).

It turns out that this fragment of first order logic can be decided via quantifier elimination [START_REF] Pope | Formalizing constructive quantifier elimination in Agda. In Proceedings. of MSFP@FSCD[END_REF]: at every step the formula is rewritten so that each innermost quantifier is existential, and then that quantified formula is replaced with a logically equivalent one where the existentially bound variable no longer occurs.

As a special bonus, the sets A of observation predicates can be rewritten in the elimination step in such a way that at the end we can recover from the quantifier free formula a set of polytopes that describe the value of all possible variables in every observable state that can be reached, together with the observation performed in that state. It is then easy to compare different strategies observing the value taken by the objective function when its input ranges over the polytope. The quantifier elimination algorithm starts rewriting an innermost quantified subformula into the normal form

∃x.l ≤ kx ∧ kx ≤ u ∧ i i O(S i , A i )
where x / ∈ l, u and F stands for either F or ¬F . Then it replaces the formula with its logically equivalent one

( li∈l uj ∈u l i ≤ u j ) ∧ i i O(S i , {a ∈ A i | l ≤ kx ∧ kx ≤ u})
Afterwards the algorithm loops on another innermost quantifier until no quantifiers are left. Special care is required to avoid simplifying ∨ F into and ⊥ ∧ F into ⊥ to avoid loosing the polytopes recoverable from F . Example 3. We illustrate the quantifier elimination technique on the characteristic formula (1). In the following, the underlined formulas are the next ones to be simplified. For the sake of readability, we shorten expressions as 0 + 0 into 0 and v + 0 into v.

1 M ω C = ∃x x = 1 ∧ ∀v1∃y (y = 1 ∧ ∀v2 O(13, {v1 + v2})) ∨ (y = 2 ∧ O(14, {v1})) ∨ x = 2 ∧ ∃z z = 1 ∧ ∀v2 O(
∨ x = 2 ∧ ∃z z = 1 ∧ O(15, {v2}) ∨ ∃z z = 2 ∧ O(16, {0}) ⇐⇒ ∃x x = 1 ∧ ∀v1 O(13, {v1 + v2 | y = 1}) ∨ O(14, {v1 | y = 2}) ∨ x = 2 ∧ O(15, {v2 | z = 1}) ∨ O(16, {0 | z = 2}) ⇐⇒ ∃x x = 1 ∧ ¬∃v1 ¬O(13, {v1 + v2 | y = 1}) ∧ ¬O(14, {v1 | y = 2}) ∨ x = 2 ∧ O(15, {v2 | z = 1}) ∨ O(16, {0 | z = 2}) ⇐⇒ ∃x x = 1 ∧ O(13, {v1 + v2 | y = 1}) ∨ O(14, {v1 | y = 2}) ∨ x = 2 ∧ O(15, {v2 | z = 1}) ∨ O(16, {0 | z = 2}) ⇐⇒ ∃x x = 1 ∧ O(13, {v1 + v2 | y = 1}) ∨ x = 1 ∧ O(14, {v1 | y = 2}) ∨ x = 2 ∧ O(15, {v2 | z = 1}) ∨ x = 2 ∧ O(16, {0 | z = 2}) ⇐⇒ ∃x x = 1 ∧ O(13, {v1 + v2 | y = 1}) ∨ ∃x x = 1 ∧ O(14, {v1 | y = 2}) ∨ ∃x x = 2 ∧ O(15, {v2 | z = 1}) ∨ ∃x x = 2 ∧ O(16, {0 | z = 2}) ⇐⇒ O(13, {v1 + v2 | x = 1 ∧ y = 1}) ∨ O(14, {v1 | x = 1 ∧ y = 2}) ∨ O(15, {v2 | x = 2 ∧ z = 1}) ∨ O(16, {0 | x = 2 ∧ z = 2})
Applying the above technique to the equation ( 2), we derive

O(3, {1 | x = 1}) ∧ O(9, {1 | x = 1 ∧ y = 1}) ∨ O(11, {1 | x = 2 ∧ z = 1})
We notice that, in the case of this last formula, the best strategy to maximize ω H is to choose x = 1 ∧ y = 1 that yields the observation 1 + 1 = 2. More precisely, the strategy consists in picking the branch 1 of the rule

+ v 2 | x = 1 ∧ y = 1}) ∨ O(14, {v 1 + 0 | x = 1 ∧ y = 2}) ∨ O(15, {0 + v 2 | x = 2 ∧ z = 1}) ∨ O(16, {0 + 0 | x = 2 ∧ z = 2})
there is no best strategy to maximize ω C because, for example, by choosing x = 1 ∧ y = 1, one can observe any value in the set {v 1 + v 2 }. In fact, putting the citizen in parallel with the garbage bin, the formal parameters v 1 and v 2 can only be instantiated with either k or k , according to the interleaving of the moves of the citizen with the other actors. In particular, running the analysis again on the larger model -due to the interleaving -, we obtain the characteristic formula:

O({k + k | x = 1 ∧ y = 1}) ∨ O({k + k | x = 1 ∧ y = 1}) ∨ O({k + k | x = 1 ∧ y = 1}) ∨ O({k + k | x = 1 ∧ y = 1}) ∨ O({k | x = 1 ∧ y = 2}) ∨ O({k | x = 1 ∧ y = 2}) ∨ O({k | x = 2 ∧ z = 1}) ∨ O({k | x = 2 ∧ z = 1}) ∨ O({0 | x = 2 ∧ z = 2})
In this case, there is still no optimal choice because, for example, by taking x = 1 ∧ y = 1 one may observe k + k, which may be smaller than k that is observed for x = 1 ∧ y = 2. As already discussed, it is sufficient for the implementor to pick 0 < k < 2k < 4k to force the existence of a best strategy which is x = 1 ∧ y = 1 and that coincides with the best strategy from the city hall point of view, as expected.

Remark 1. The standard formal specification languages to verify and specify properties of transition systems are temporal logics [START_REF] Pnueli | The temporal logic of programs[END_REF]. Actually one may use tools that are based on these logics, such as [START_REF] Asirelli | A model-checking tool for families of services[END_REF], to automatically analyze systems based on smart contracts. In fact, our characteristic formula is actually a compilation of linear-time temporal logics with Presburger constraints, which is decidable [START_REF] Demri | Linear-time temporal logics with presburger constraints: an overview[END_REF]. We have preferred the current presentation because it is the one we use in our prototype implementation.

Implementation

We are terminating the implementation in OCaml of a tool that, given a set of actors, an initial state and an objective function, automatically extracts the analysis model, computes the characteristic formula and applies quantifier elimination over it.

Initially we hoped to be able to reuse off-the-shelf implementations of Presburger quantifier elimination by dropping the O predicate and recovering the polytopes from the tools. But the tools we analyzed are unable to spit out the polytopes. In fact, because of the double-exponential complexity of quantifier elimination over the number of alternations of quantifiers, the tools avoid quantifier elimination and rather use model checking or reduction to finite state automata. However, these two techniques can only enumerate the points in the polytope, without providing a closed description of it [START_REF] Haase | A survival guide to presburger arithmetic[END_REF][START_REF] Ganesh | Deciding presburger arithmetic by model checking and comparisons with other methods[END_REF]. Therefore we decided to implement quantifier elimination straight away. We need to evaluate whether our quantifier elimination is is doable in practice on characteristic formulae generated from realistic examples of smart contracts. This is left as future work, once the whole implementation is completed. We will also study the application of other techniques, like temporal logic, to analyse the formal calculus and the models introduced in the paper. To ease these analyses, we will write transpilers from our smart calculus language to existing languages, initially targeting both Solidity and Liquidity.

Conclusions

In this paper we have introduced a unified calculus for modelling smart contracts and users, which are the primary actors of decentralized applications. These applications run on blockchain systems and handle and transfer assets of considerable value. We have therefore studied how to regulate by means of smart contracts the interaction between (rational) users that systematically try to maximize their revenue or to minimize losses. This is achieved by expressing the system behaviour as a formula in Presburger arithmetics and solving arithmetic constraints. Our technique is amenable to automated verification and we are currently completing an OCaml implementation.

The analysis of smart contracts for deriving strategies and distilling the most meaningful ones opens unexpected connections between (micro) economy and computer science that deserves further investigations. While this direction of research has been already pointed out in other contributions (see e.g. [START_REF] Bigi | Validation of decentralised smart contracts through game theory and formal methods[END_REF]), we believe that there is much work still to be done.

As regards our calculus, several extensions must be considered. First of all, the types must be extended with simple dynamic data types, such as arrays and maps. Then, if we want to model faithfully the (human) users, we need to take into account probabilities because users are not always 100% rational; they may be irrational with some percentage.

Dedication. Cosimo is proud to dedicate this paper to Stefania Gnesi and to the unforgettable Friday afternoons spent together with Alessandro Fantechi. Stefania and Alessandro have been Cosimo's Master Thesis advisors and they first led him to concurrent systems, formal methods and temporal logics. Thank you Stefania!

  = return e | this.f = z;s | if e then s else s | s + s (statements) z ::= e | e.m(e) (rhs-expressions) e ::= naturals | x | α | fail | this | this.f | e op e (expressions)

Fig. 1 .

 1 Fig. 1. Syntax and runtime statement semantics of scl.

S

  , where µ may be either empty or or fail, and ψ is a formula.The class declarations are kept implicit in the transition relation. The reader may find the formal definition of µ

Fig. 3 .

 3 Fig. 3. The citizen and garbage bin classes

  [end-fail-open] -or a commit -rule [end-open] -, respectively.

  Symbolic values:v ::= . . . | x | v op v (open-true] e α, = v α : if e then s else s ;s , -→ v =0 s;s , [if-open-false]e α, = v α : if e then s else s ;s ,

Fig. 4 .SS

 4 Fig. 4. The open semantics of scl.

Fig. 5 .

 5 Fig. 5. The models of the citizen and the bin

Definition 1 .

 1 Let (S, S 0 , T ) be a scl analysis model. An objective function ω maps labels µ of transitions S µ -→ ψ S in T to some integer expression. Given a computation S 1 µ1

  15, {v2}) ∨ z = 2 ∧ O(16, {0}) ⇐⇒ ∃x x = 1 ∧ ∀v1∃y (y = 1 ∧ ¬∃v2 ¬O(13, {v1 + v2})) ∨ (y = 2 ∧ O(14, {v1})) ∨ x = 2 ∧ ∃z z = 1 ∧ ¬∃v2 ¬O(15, {v2}) ∨ z = 2 ∧ O(16, {0}) ⇐⇒ ∃x x = 1 ∧ ∀v1∃y (y = 1 ∧ ¬¬O(13, {v1 + v2})) ∨ (y = 2 ∧ O(14, {v1})) ∨ x = 2 ∧ ∃z z = 1 ∧ ¬¬O(15, {v2}) ∨ z = 2 ∧ O(16, {0}) ⇐⇒ ∃x x = 1 ∧ ∀v1 ∃y(y = 1 ∧ O(13, {v1 + v2})) ∨ ∃y(y = 2 ∧ O(14, {v1}))

  are given in Figure 4. As regards runtime statements, the rules [if-true] and [if-false] are replaced by [if-open-true] and [if-open-false]

  [choice] in the state . . . + x . . . and the branch 1 in the state . . . + y . . .. With an abuse of notation, we will indicate strategies as conjunctions i∈1..n x i = k i .Let us discuss strategies for ω C . According to the formula O(13, {v 1

Research partly supported by the H2020-MSCA-RISE project ID 778233 "Behavioural Application Program Interfaces (BEHAPI)".


Dr Carlos N Ibarra-Cerdeña

Ph. D Maria I Rocha-Gaso

Ph. D Maria I ; Rocha-Gaso

J Luis

Ph. D Denis Villarreal-Gómez

Ph. D.; Frederic Beyseen

Ph. D Marco A Sarry

Ph. D Carlos N Reyna- Carranza

Ph.D Ibarra-Cerdeña

M.-I Rocha-Gaso

L.-J Villarreal-Gomez

D Beyssen

F Sarry

M.-A Reyna-Carranza

Ibarra -Cerdeña

Biosensors to diagnose Chagas disease: A review 1

Keywords: Chagas disease, biosensors, detection technologies, diagnosis, neglected diseases. 21

Chagas disease (CD), which mostly affects underprivileged people, has turned into one 9 of Latin America's main public health problems. Prevention of the disease requires early diagnosis, 10 initiation of therapy, and regular blood monitoring of the infected individual. However, the majority 11 of the infections go undiagnosed because of general mild symptoms and lack of access to medical 12 care. Therefore, more affordable and accessible detection technologies capable of providing early 13 diagnosis and parasite load measurements in settings where CD is prevalent are needed to enable 14 enhanced intervention strategies. This review discusses currently available detection technologies 15 and emerging biosensing technologies for a future application to CD. Even if biosensing 16 technologies still require further research efforts to develop portable systems, we arrive to the 17 conclusion that biosensors could improve diagnosis and the patients' treatment follow-up, in terms 18 of rapidity, small sample volume, high integration, ease of use, real-time and low cost detection 19 compared to current conventional technologies. 20

Introduction 22

Chagas disease (CD), discovered in 1909 by the Brazilian physician Carlos Chagas [START_REF] Chagas | Nova tripanozomiaze humana: estudos sobre a morfolojia e o ciclo evolutivo do 269 Schizotrypanum cruzi n. gen., n. sp., ajente etiolojico de nova entidade morbida do homem[END_REF], nowadays 23 has turned into one of Latin America's main public health problems [START_REF] Hotez | The neglected tropical diseases of 272 Latin America and the Caribbean: a review of disease burden and distribution and a roadmap for 273 control and elimination[END_REF]. Based in disability-adjusted 24 life-years as a measure of disease burden, CD figure as the most important parasitic vector-borne 25 illness in the Region of Americas, seven times higher than Malaria and up to three times more than 26 Dengue [START_REF]Global burden of disease estimates for[END_REF], and yet it is still absent in the agenda of the public health policies and practices of 27 many endemic countries [START_REF] Gascon | The need for global collaboration to tackle hidden public health 276 crisis of Chagas disease[END_REF][START_REF] Tarleton | 280 Development and Evaluation of a SPR-based Immunosensor for Detection of Anti-Trypanosoma cruzi 281 Antibodies in Human Serum[END_REF]. More generally, ranks fourth in mortality and eighth in morbidity 28

Manuscript

Click here to view linked References among world neglected tropical diseases (6), and is estimated that between eight and eleven 29 million people are infected, while 100 million are at risk of acquiring the disease; the main cause 30 being to live in proximity with disease vectors [START_REF] Sánchez-Camargo | Comparative evaluation of 11 commercialized rapid diagnostic tests for detecting Trypanosoma 285 cruzi antibodies in serum banks in areas of endemicity and nonendemicity[END_REF]. CD is caused by the parasitic presence of the 31

Trypanosoma cruzi in the organism, which is mainly transmitted by contamination with infected 32 feces of blood-sucking triatomine vectors during a human blood meal. Nevertheless, it can also be 33 transmitted through blood transfusions, organ transplants, infected mothers to their unborn 34 children and ingestion of contaminated food (i. e. Oral transmission; [START_REF] Who | CONTROL OF CHAGAS DISEASE Second report of the WHO Expert Committee World Health[END_REF]. Although disease 35 progression can be associated with the mechanism of infection, with oral transmission causing the 36 most severe outbreaks [START_REF] Coura | The main sceneries of chagas disease transmission. The vectors, blood and oral 290 transmissions -A comprehensive review[END_REF], people living at risk regions are susceptible to polyparasitism (i.e. [START_REF] Roux-Marchand | Rayleigh Surface Acoustic Wave As an 354 Efficient Heating System for Biological Reactions : Investigation of Microdroplet Temperature 355 Uniformity[END_REF] Coinfections and superinfections with different strains of T. cruzi), with unknown effects in the 38 variability of the disease progression and response to treatments [START_REF] Perez | Chagas disease: The challenge of polyparasitism?[END_REF]. [START_REF] Belluzo | Favorably orienting recombinant 359 proteins to develop amperometric biosensors to diagnose Chagas' disease[END_REF] CD mostly affects underprivileged people and the majority of the T. cruzi infections go undiagnosed 40 because of general mild symptoms and lack of access to medical care [START_REF] Ramsey | 294 Opportunity cost for early treatment of Chagas disease in Mexico[END_REF]. Due to this fact, CD is 41 considered as a Neglected Tropical Disease whose improvement in diagnosis and treatment today 42 requires research and development efforts with non-profit interests. The highest prevalence of 43 Chagas disease has been reported in Bolivia (6.75-15.4 %), followed by Paraguay (0.69-9.3 %), 44 Panama (0.01-9.02 %), Brazil (0.8-1.30 %), Mexico (0.5-6.8 %) and Argentina (4.13-8.2 %) 45 [START_REF] Liu | Preventing the transmission of American trypanosomiasis and its spread into 296 non-endemic countries[END_REF]. Citing a case, this disease causes almost 6% of the annual deaths in Mexico and the 46 seroprevalence can roughly be estimated at least in 3% due to a lack of active epidemiological 47 surveillance (most cases are detected during blood screening procedures in blood banks). Yet, less 48 than 0.5% of the infected individuals have access to treatment in this country as a result of 49 anachronisms in the normativity, among other failures in the public health system [START_REF] Manne | Barriers to 298 treatment access for Chagas disease in Mexico[END_REF]. [START_REF] Barfield | A 386 Highly Sensitive Rapid Diagnostic Test for Chagas Disease That Utilizes a Recombinant Trypanosoma 387 cruzi Antigen[END_REF] Even if CD mainly affects tropical countries, with nowadays ease of traveling and migration, other 51 countries are also being affected by this infection [START_REF] Schmunis | Chagas disease: a Latin American health problem becoming a world 300 health problem[END_REF]. Several cases have been reported in USA, 52

Canada, Europe and in Western Pacific regions like Japan and Australia [START_REF] Schmunis | Chagas disease: a Latin American health problem becoming a world 300 health problem[END_REF][START_REF] Conners | A global systematic review of Chagas disease 302 prevalence among migrants[END_REF][START_REF] Requena-Méndez | 304 Prevalence of Chagas Disease in Latin-American Migrants Living in Europe: A Systematic Review and 305 Meta-analysis[END_REF]. Notably, CD 53 continues to be an inconspicuous public health problem, with limited medical awareness, either 54 because it is commonly targeted in people with relatively low medical access or because it can 55 currently occur in unexpected regions. Thus, the treatment of CD urgently needs to generalize and 56 standardize diagnostic procedures. 57 Biosensors are relatively new analytical devices that can help to detect the presence of specific 58 compounds and pathogens in liquid environments and complex mixtures like: water and blood 59 serum. Although these devices have been formerly used in the alimentary industry (mostly to 60 detect toxins and infectious pathogens), they are been increasingly used to diagnose human 61 diseases [START_REF] Sin | Advances and challenges in biosensor-based diagnosis of 307 infectious diseases[END_REF]. Therefore, these devices can be employed for the diagnosis of CD. The development 62 of biosensors requires a biological active component to be immobilized onto the surface of a 63 transducer. The selective recognition layer, towards T. cruzi specific antigens present in patients' 64 blood serum, can selectively detect the target analyte generating a signal response in the sensor 65 (see Figure 1). Depending on their transducing principle biosensors can be electrochemical, 66 acoustic or optic. 67

In this work, we firstly introduce a brief description of the disease. Secondly, we present a review 68 of biosensor technologies whose applicability to diagnose CD has been investigated. Finally, we 69 mention the benefits and drawbacks of applying biosensors as solutions to this major public health 70 issue and the infrastructure required to conduct biosensor experiments for this application. 71

Brief description of CD and current needs 72

CD passes through two successive stages: an acute phase and a chronic phase. The acute phase 73 occurs at the following 6-8 weeks after infection. The acute phase is followed by the chronic phase 74 of CD, which lasts for the rest of the life of the infected individual, and has different forms. In the 75 Figure 1. General scheme of a biosensor detection strategy. A biosensor is composed of a biochemical interface where specific bio-species are absorbed; a transducer which translates the recognition event to another physical response that can be measured and an electronic system which acquires and records the signal.

indeterminate form, an equilibrium between the parasite and the immunological response of the 76 infected individual is reached and most infected patients appear healthy, with no evidence of organ 77 damage that could be found by current standard methods of clinical diagnosis [START_REF] Who | CONTROL OF CHAGAS DISEASE Second report of the WHO Expert Committee World Health[END_REF]. About 50-70% 78 of infected individuals will remain in this condition for the rest of their lives. However, several years 79 after the chronic phase has started, 10-40% of infected individuals will pass to the cardiac form of 80 the disease and will develop injuries of various organs, mainly the heart, the digestive system, and 81 occasionally, the peripheral nervous system [START_REF] Who | CONTROL OF CHAGAS DISEASE Second report of the WHO Expert Committee World Health[END_REF][START_REF] Prata | Clinical and epidemiological aspects of Chagas disease[END_REF]. These important symptomatic changes occur 82 10-20 years after the acute phase of the disease and include a broad range of types of damage. 83

The clinical manifestations vary from mild symptoms to heart failure and, frequently, sudden 84 cardiac death [START_REF] Prata | Clinical and epidemiological aspects of Chagas disease[END_REF]. The acute phase of CD is recognized only in an estimated 1-2% of all 85 individuals acquiring the infection (8) due to a lack of access to sufficient medical care. Thus, more 86 than any other parasitic disease, CD is closely related to social and economic development. 87

Paradoxically, acute phase is the most appropriate period for drug treatment, showing relatively 88 high levels of sero-conversion, while organ damage is prevented [START_REF] Pinto Ay Das | Clinical Follow-Up of Responses to Treatment with Benznidazol in Amazon: A Cohort 311 Study of Acute Chagas Disease[END_REF]. Conversely, it has been 89

shown that drug treatment with Trypanocidal therapy in patients with established Chagas 90 cardiomyopathy, can cause seroconversion, but does not stop cardiac clinical deterioration [START_REF] Morillo | Randomized Trial of Benznidazole for Chronic 315 Chagas' Cardiomyopathy[END_REF]. 91

Given that no vaccine is currently available to prevent CD, vector control, diagnosis tests, 92 opportune drug treatment, and clinical follow-up are the most effective methods to fight against 93 the disease (21). Nevertheless, all these measures suffer of several hindrances imposed by the 94 synergistic negative effects of diverse vulnerability components of CD risk, such as ecological 95 factors (i.e. land-use changes) -that are broadening the contact zones between humans and 96 parasites (Lopez-Cancino et al., 2015)-, the chronic failure of health care policies hindering the 97 reduction of CD incidence (5), the limited awareness of physicians ( 22), and several socio-cultural 98 practices that perpetuate CD exposure in endemic regions [START_REF] Ventura-Garcia | Socio-322 Cultural Aspects of Chagas Disease: A Systematic Review of Qualitative Research[END_REF]. Health policies to control/reduce 99 vectorial exposure to CD in Latin America are challenged for the relatively high diversity of vectors 100 that shows a broad environmental tolerance. Likewise, a wide territory of America is suitable for CD 101 vectorial transmission [START_REF] Fergnani | Large-scale patterns in morphological 324 diversity and species assemblages in Neotropical Triatominae (Heteroptera: Reduviidae)[END_REF][START_REF] Ibarra-Cerdeña | Phylogeny 327 and niche conservatism in North and Central American triatomine bugs (Hemiptera: Reduviidae: 328 Triatominae), vectors of Chagas' disease[END_REF][START_REF] Ramsey | Atlas of Mexican Triatominae (Reduviidae: Hemiptera) and 331 vector transmission of Chagas disease[END_REF][START_REF] Gurgel-Gonçalves | Chagas disease: 335 Changes in knowledge and management[END_REF]. 102

In order to face the epidemiological challenges due to the increasing complexity of interactions 103 among the transmission routes of T. cruzi in endemic and non-endemic countries, access to early 104 diagnostic and treatment seems as the most cost-efficient ways to reduce the CD burden [START_REF] Ramsey | 294 Opportunity cost for early treatment of Chagas disease in Mexico[END_REF]. 105 Several paths of scientific advances and discoveries envisage an optimistic future to reduce CD 106 burden coming from a better understanding of CD transmission and management toward its 107 interruption (28). The fact that the World Health Organization (WHO) has made a commitment with 108 Bill and Melinda Gates Foundation and other stakeholders to control the most neglected diseases by 109 2020, including CD among them, opens an opportunity window to orientate research priorities. This 110 commitment, launched in 2012, was called the London Declaration 111 (http://www.unitingtocombatntds.org/). However, claims have been raised to urge implicated 112 organizations to set the needed measures to reach these goals, among which improved diagnosis 113 (i.e. precision and accessibility) seems as one of the most important first steps [START_REF] Tarleton | 280 Development and Evaluation of a SPR-based Immunosensor for Detection of Anti-Trypanosoma cruzi 281 Antibodies in Human Serum[END_REF]. 114

Blood banks in endemic countries require fast and secure screening method for small and medium 115 health facilities, since screening for CD is mandatory in some endemic countries [START_REF] Who | CONTROL OF CHAGAS DISEASE Second report of the WHO Expert Committee World Health[END_REF]. Several 116 countries do not have an active program for CD detection and depend only for the blood bank 117 reports. The most important reason of this fact is the low feasibility to detect Chagas in patients. 118 Since, CD do not produce particular symptoms, there are not incentives from society. Nevertheless, 119 the bug bite is quite notorious and people can suspect that they are infected with T. cruzi when a 120 chinchoma1 appears. In such cases, people can search medical assistance and be subjects of a 121 blood test. 122 Climate change and global warming increase the risk of rising CD burden in some regions. Climate 123 change impacts on vector-borne diseases [START_REF] Sutherst | Global Change and Human Vulnerability to Vector-Borne Diseases Global Change 15 and Human Vulnerability to Vector-Borne Diseases[END_REF] and is undoubtedly detonating variables that make 124 the CD transmission become potentially dangerous, as the WHO points out [START_REF] Githeko | Climate change and vector-borne diseases: a 339 regional analysis[END_REF]. Nevertheless, the 125 incidence of CD can be greatly reduced by residual insecticide-based vector control programs that 126 decrease the populations of the transmitting vectors and by improving housing [START_REF] Coura | Chagas disease: Control, elimination and eradication. Is it possible?[END_REF]. 127

Current detection technologies and their limitations 128

Currently, laboratory methods are employed to diagnose CD. Depending on the patients' phase of 129 infection some are more convenient than others. During the acute phase of CD, a large number of 130 parasites are present in the peripheral blood and can be diagnosed by direct microscopical 131 observation of fresh blood (parasitological test). However, for the chronic phase of CD the 132 diagnosis is not possible, due to the scarce parasitemia. Therefore, the immunodiagnosis is widely 133 used since nearly all T. cruzi-infected individuals in the chronic phase develop antibodies against 134 the complex antigenic mixture of the parasite [START_REF] Who | CONTROL OF CHAGAS DISEASE Second report of the WHO Expert Committee World Health[END_REF]. From a prospective point of view, it is important to discuss about another kind of technology, which 156 could be deployed for Chagas Disease diagnosis in the near future. Over the last decade, Shear-157 Horizontal (SH) Surface Acoustic Wave (SAW) immunosensors (Love-SAW with a guiding layer) 158 have been developed for the diagnosis of various diseases [START_REF] Rocha-Gaso | Surface generated acoustic 347 wave biosensors for the detection of pathogens: a review[END_REF]. Such immunosensors exhibit a 159 high sensitivity and a very low limit of detection (in the order of pg/μl of blood serum). This 160 technology give very relevant results for the detection of antibodies, specific to certain diseases 161 [START_REF] Lee | SAW immunosensors for HBsAb detection[END_REF]. The only drawback of this technology is that a residual frequency or phase shift always 162 remains, which is induced by non-specific mass effects, i.e. a shift which does not correspond to 163 specific antigen-antibody interactions on the sensor surface [START_REF] Lee | SAW immunosensors for HBsAb detection[END_REF]. In order to drastically reduce or 164 avoid cross-reactions with other type of interactions that may lead to false positives, Rayleigh-SAW 165 generation, on the same piezoelectric substrate, seems to be very promising [START_REF] Rocha-Gaso | Lab-on-a-chip based integrated hybrid 350 technologies for biofluids manipulation and characterization[END_REF]. In addition, 166 these waves can be used to generate fast fluid actuation to improve mixing and desorption 167 promoting faster molecular interactions. Indeed, Rayleigh-SAW liquid effects can induce intense 168 recirculation, actuation, heating or atomization, depending on the mechanical power conveyed by 169 these acoustic waves [START_REF] Beyssen | Microfluidic device based on surface acoustic wave[END_REF][START_REF] Roux-Marchand | Rayleigh Surface Acoustic Wave As an 354 Efficient Heating System for Biological Reactions : Investigation of Microdroplet Temperature 355 Uniformity[END_REF]. This recirculation can allow to re-suspend all non-specific species 170 that could settle and lead to non-specific responses. 171

Biosensing research efforts for Chagas diagnosis 172

Biosensors that have been investigated for the diagnosis of CD can be classified into 173 electrochemical -where amperometric [START_REF] Ferreira A. A P | Immunosensor for the diagnosis of Chagas' 357 disease[END_REF][START_REF] Belluzo | Favorably orienting recombinant 359 proteins to develop amperometric biosensors to diagnose Chagas' disease[END_REF][START_REF] Ferreira | Investigation of the interaction between Tc85-11 protein and antibody anti-T. cruzi by AFM and 362 amperometric measurements[END_REF][START_REF] Foguel | Amperometric immunosensor for Chagas' disease using gold CD-R Transducer[END_REF] and impedimetric [START_REF] Erdmann | Development of 44[END_REF] [START_REF] Ferreira A. A P | Immunosensor for the diagnosis of Chagas' 357 disease[END_REF]. It consisted on 178 an amperometric immunosensor. This biosensor required an electrochemical interaction and, 179 therefore, a potensiostat-galvanostat was required to conduct the measurements. Potensiostats are 180 powerful equipment, but they are large and heavy for a final portable biosensing system. Hence, 181 other electronics for biosensors characterization should be developed which provide higher 182 miniaturization and integration capabilities for portable systems. 183

Recently, Luz et al. (2015) presented the first biosensor for the diagnosis of CD based on SPR 184 transducers (6). They obtained the parameter related to the presence of antibodies anti-T. Cruzi 185 found in human serum in approximately 20 min. SPR transducing principle requires an optical 186 source for the laser generation and the integration of this source to the equipment, currently, leads 187 to high volume and heavy apparatus, only suitable for laboratory tests. Moreover, even if optical 188 biosensors can be very sensitive, the cost of SPR equipment is higher than USD $50,000 and for 189 this reason, not many researchers can afford such systems (43). 190 192

Biosensors and their contribution to reduce CD burden 198

An ideal serological test should be easy to perform in a single step, fast, cheap, require no special 199 equipment or refrigeration reagents and should have a sensitivity and specificity of 100%. Such a 200 test does not exist currently for the diagnosis of CD. Hence, new technologies, which combine, 201 robustness, simplicity, portability and rapidity with an effective sensitivity and selectivity could 202 contribute to more efficiently diagnose CD. There are evidences that show that biosensors could 203 meet most of these attributes for this application (6,[START_REF] Ferreira A. A P | Immunosensor for the diagnosis of Chagas' 357 disease[END_REF]. Biosensors could improve the diagnosis 204 and the patients' treatment follow-up, in terms of rapidity, real-time and low cost detection 205 compared to current detection technologies like Polymerase Chain Reaction (PCR) and ELISA. In 206 addition, the use of biosensors offers significant advantages like: small fluid volume manipulation, 207 a high integration capability that facilitates the development of portable devices and ease of use. 208

This should allow their use by non-specialized personnel in non-centralized laboratories [START_REF] Sin | Advances and challenges in biosensor-based diagnosis of 307 infectious diseases[END_REF]. 209

Nevertheless, further research efforts are needed to achieve a biosensing portable device for CD 210

diagnosis. 211

The expected features of biosensors are high selectivity and sensitivity, real-time label-free 212 monitoring, easy to use, reliability, high miniaturization capabilities and low cost. Biosensors based 213 on optical and acoustic wave sensing technologies could meet these requirements in a near future 214 and seem to be very promising tools for this application. Such devices will lead to more sensitive 215 tests at lower reagent concentrations, allowing biosensing system users to: i) reduce the cost of 216 reagents; ii) obtain valuable quantitative information; and iii) extend the measurement range of 217 the assays. 218

Infrastructure requirements 219

To develop a portable biosensor system for the rapid diagnosis of CD, first of all, it is necessary to 220 integrate a transducer with a suitable sensitive bio-chemical layer. Some authors have already 221 achieved this milestone, as stated in Section 4. Additionally, the system requires the integration of: 222 i) an electronic read-out system, for the interrogation and signal acquisition; ii) a microfluidic 223 system, to handle bio-fluids; and iii) a thermal control unit, to keep the temperature stable during 224 the sample analysis. This last point could be avoided if it is proven that the temperature sensitivity 225 of the sensor in use is negligible for the experiments we are conducting or if a differential 226 measurement setup for a temperature compensation is employed [START_REF] Balcerzak | Ultrasonic chemical sensor[END_REF]. Furthermore, it is 227 important to mention, that a fully-automated feature is desirable for the complete system, in order 228 to run the sample analysis as comfortably as possible. 229 Nowadays, some companies offer commercial solutions for integrated biosensing systems that 230 could be employed to diagnose CD. However, most of this systems are still of considerable size, 231 weight and price, which prevents their wide use for field applications in low income communities. 232

Table 2 shows some integrated biosensing platforms currently available in the market and some of 233 their features. As can be appreciated in the table, all these systems require to be operated in a 234 laboratory due to their dimensions. If researchers choose a non-commercial solution, they require 235 to design and develop a system according to their needs. Nevertheless, this might allow them to 236 pursuit a more compact, cost-effective and portable system. 237

Conclusions 239

Since there is not vaccine for CD, currently, the vector control and diagnosis tests are the most 240 effective methods for preventing the disease and apply effective drug treatments. Even if a 241 prophylactic or therapeutic vaccine could be achievable in next years, this would need to be part of 242 integrated efforts that include better diagnostic means, since a vaccine is unlikely to be enough to 243 stop the parasite transmission. Therefore, highly predictive diagnostic tests are required, not only 244 to estimate the real size of CD problem, but also to assess the effectiveness of every action 245 conducted towards a disease burden reduction. 246 Currently, there are three conventional tests to diagnose Chagas in its chronic phase: IHA, IIF and 247 ELISA. All of these tests have sensitivities under 100%. Therefore, the WHO recommends 248 performing at least two of these tests for a conclusive diagnosis, leading to a bottleneck of parasite 249 detection, caused by limited local availability of laboratories in which such tests can be performed.

6

  Several immunodiagnosis tests are available, but mainly three conventional tests are widely used: 136 indirect haemagglutination (IHA), indirect immunofluorescence (IIF) and Enzyme Linked Immuno 137 Assay (ELISA). These tests present several limitations such as: (i) cross-reactivity with other 138 parasites; (ii) not 100% of sensitivity; (iii) the need to be performed in a laboratory; and (iv) a 139 long time is required to obtain the results. IHA test results can be obtained in about two hours, 140 whereas IIF results can be obtained after numerous steps in two hours and ELISA takes several 141 hours to carry out, including prior sensitization of microplates with T. cruzi antigens for about12 142 hours (6). All these tests have to be performed in centralized laboratories; some of them require 143 sophisticated equipment and skilled technicians. Since none of these tests have a sensitivity of 144 100%, the WHO recommends conducting at least two conventional tests for a definitive diagnosis 145 of T. cruzi infection (8). 146 More recently, non-conventional tests, like rapid lateral flow (RLF) tests, are commercially available 147 in the market to detect T. cruzi infection using whole blood, serum or plasma (Sánchez-Camargo et 148 al. 2014). These tests are based in different tests principles: immunochromatography, particle 149 agglutination, immunofiltration or immunodot. They provide fast results (between 5 to 60 min 150 reading times) without the need of electrical equipment and they require low volume samples (5 to 151 150 μl). However, the sensitivities and specificities of such tests are lower than that of conventional 152 tests and they only provide qualitative or semi-quantitative results, which prevents obtaining 153 important test information like genetic lineage of the T. cruzi (32) and the immunoreaction 154 kinetics. 155

++++++

  High selectivity and sensitivity + Improves the time required to yield results + It works well for samples without interfering molecules High sensitivity of 99.5 % Low cost (less than $2 to the end user) No need of an aseptic working area + Fast (real-time) Easy to perform. Not need of trained personnel + In situ simple preparation + High analytical specificity + Reduction of reagents consumption + Reduced analysis time + High reliability + High sensitivity + Integration of multiple processes in a single device + Possible automation Low

  sensors can be found-and 174 optical -where mainly Surface Plasmon Resonance (SPR) transducers (6) are found. Biosensors 175 could provide the benefits presented in Table 1 in comparison with other currently employed 176 techniques for the diagnosis of CD. 177 Pumpin-Ferreira et al., in 2005, reported a biosensor for the diagnosis of CD

Table 1 .

 1 Some methods for the diagnosis of CD.

Table 2 .

 2 Different biosensing systems currently available in the market.

	238
	Product	Company Name	Transducer Technology	Dimensions (cm)	Weight (kg)
	Q-Sense Omega Auto®	Q-sense	Acoustic	70×67×57	83
	Biacore X100®	General Electric	SPR	59.6×56.3×59.3	47
	AWS A20-F20®	AWsensors	Acoustic	77×75×45	60
	OpenPlex®	Horiba	SPRi	49×30.4×48	15.6

Name of the inflammatory injury after a bug bite.

vectors in Brazil based on ecological niche modeling. J Trop Med 2012:705326.

with organic monomolecular layer. Arch Acoust 31:47-52.