Smart contracts are programs that automatically execute on blockchains when some conditions are verified. They encode the legally relevant events needed to satisfy the terms of an agreement and are usually defined by using procedural languages, even if some recent proposals investigated the possibility of using logic formalisms. However, existing logic-based initiatives are rather limited since they only enable the formal checking of properties of a single smart contract, totally neglecting its possible interactions with other smart contracts running on the same blockchain. This paper proposes a framework, called SCRea, that works on a set of smart contracts specified as Linear Temporal Logic (LTL) formulas. SCRea enables to reason about smart contracts considered individually or by considering them as running cooperatively or competitively on the same blockchain.
Distributed Ledger Technologies (DLT) [
Smart contracts in blockchains are typically programmed in a procedural language specific of the host
DLT platform, such as Solidity[
We try to fill this gap by focusing on the application of linear temporal logic on finite traces (LTL )
[
We also studied the applicability of SCRea for the identification of conflict situations at runtime by dealing with one execution trace. In the domain of smart contracts, the term trace denotes a sequence of events executed by a blockchain or a sequence of function or event invocations issued by one or more smart contracts. The availability of information at runtime helps dynamic verification techniques to mitigate one of the main obstacles in the analysis of smart contracts: the need to model a complex blockchain execution environment.
The rest of the paper is organized as follows. In Section 2 we introduce some preliminary definitions. The encoding of smart contracts in linear temporal logic is discussed in Section 3 while Section 4 reports about reasoning problems that are enabled by our encoding. The SCRea framework is described in Section 5 and Section 6 will conclude the paper.
Linear temporal logic, denoted by LTL, is a modal logic introduced in the 1970s [
Syntax. Let’s be a set of propositional variables. An LTL formula is built on variables in using boolean connectives ∧, ∨, ¬ as well as a number of time operators of two categories: future and past temporal operators. For our purposes we will focus on a specific fragment of LTL which includes the future operator X (next) and the past operators Y (previous), H (always in the past), P (in the past), S (since). Moreover, we assume that the negation is atomic in in the sense that it is applied directly only to propositional variables. More formally, the formula is constructed according to the following grammar, where is any variable in : ::= | ¬ | ( ∧ ) | ( ∨ ) | ( ) | ( ) | ( ) | ( ) | ( ) Semantics. A finite trace defined on the variables in is a sequence = 0, 1, ... − 1 that associates with each ∈ {0, 1, ...− 1} a state ⊆ consisting of all propositional variables that are assumed to be true in the time instant . The length of (its number of time instants) is denoted by ( ). Given a finite trace , we define that an LTL formula evaluate true in at the time instant ∈ {0, 1, ...( )-1} inductively as follows: ∙ , | = if and only if ∈ ; ∙ , | = ¬ if and only if ∈/ ; ∙ , | = ( 1 ∧ 2) if and only if , | = 1 and , | = 2; ∙ , | = ( 1 ∨ 2) if and only if , | = 1 or , | = 2; ∙ , | = ( ′) if and only if < ( ) − 1 and , + 1| = ′; ∙ , | = ( ′) if and only if > 0 and , − 1| = ′; ∙ , | = ( ′) if and only if for each such that 0 ≤ ≤ it’s true that , | = ′; ∙ , | = ( ′) if and only if exists such that 0 ≤ ≤ and , | = ′; the condition/action occurs the condition/action does not occurs the conditions/actions 1 and 2 occurs the conditions/actions 1 or 2 occurs in the next step the condition/action ′ must apply/be executed in the previous step the condition/action ′ must be valid/have been executed in the past there must be an instant in which the condition/action ′ was valid/was performed in the past the condition/action ′ has been verified/has always been performed in the past there is an instant in which 2 has been verified/ executed, and from that moment the condition/action 1 has always been verified/executed ∙ , | = ( 1 2) if and only if exists such that 0 ≤ ≤ and , | = 2 and for any k such that ≤ ≤ it’s true that , | = 1.
When , -1 |= we say that is a model of and is satisfiable.
Our goal is to use the fragment of linear time logic on finite traces with past operators described in the Section 2 to reason on smart contracts. From this perspective, the time operators are interpreted as reported in Table 1. In our encoding, each smart contract is a pair ⟨, ⟩, where: (i) are the preconditions, i.e. an LTL formula using past operators only; (ii) is the efect, i.e. a propositional formula or an LTL formula using future operators only. Since are the preconditions that activate the smart contract and the efect of its execution, the smart contract will be expressed by the LTL formula = ( → ), i.e., every time the preconditions occurs then the smart contract must be executed and, thus, its efect must be visible. In the smart contracts domain, a trace denotes a sequence of events executed by a blockchain platform or a sequence of function or event invocations issued by one or more smart contracts. If a trace satisfies a smart contract ⟨, ⟩ it means that it satisfies the LTL formula = ( → ) encoding it.
Example 1. Let’s consider a simple smart contract within the sharing economy context to access multimedia contents. The contract consists of the following clause: if a user requests a content for which he has previously paid, that content must be transferred to him. The propositional variables encoding events are: (he user requests the content), (the user pays for the content) and (the content is transmitted to the user). The precondition of the smart contract is = ∧ (), that is when the user requires a content it must be checked that he already payed for it. The efect is the transmission of the content to the user which is considered to be made in the time instant immediately following the request: = (). The smart contract will then be codified by the following formula: = ((∧ ()) → ()).
Using LTL to encode smart contracts allows to reason over (group of) smart contracts by exploiting its reasoning capabilities. In this section we will discuss several reasoning problems on smart contracts.
In this section we discuss three reasoning problems that can be defined if considering a single smart contract.
Model checking. A major issue when dealing with a smart contract is model verification or model
checking. The goal is to verify if a given trace , encoding the events registered by a blockchain, is a
model of a given smart contract ⟨, ⟩ encoded by the formula LTL = ( → ). This corresponds
to check whether the smart contract has been executed (i.e., the efects of its execution are visible on the
blockchain) every time its preconditions have been satisfyied. Checking if a trace is a model of a smart
contract can be done in polynomial time w.r.t the length of the formula [
Example 2. Let’s consider the smart contract discussed in Example 1 consisting in the LTL formula = (( ∧ ()) → ()) and the trace 1 = {}, {}, {}. It’s easy to see that 1 is a model of . Instead, the trace 2 = {, } is not a model of since the precondition of the smart contract is satisfied but the content is not transmitted to the user.
Satisfiability. Satisfiability is the problem of establishing whether a smart contract ⟨, ⟩ encoded by the LTL formula = ( → ) admits a satisfying trace in which it has been executed at least once. This corresponds to check whether the LTL formula () ∧ ( → ) admits a model. Example 3. The smart contract discussed in Example 1 is satisfiable, and examples of traces that satisfy it are: 1={}, {}, {} 2={, }, {} 3={}, {}, {}, {}, {}. Satisfiability at runtime. Satisfiability at runtime is the problem of verifying whether a smart contract ⟨, ⟩ (encoded by the LTL formula = ( → )) is satisfiable given a partial trace . In particular, it is the problem of verifying whether there exists a completion = of (obtained by adding to a subtrace consisting of a certain number of states) such that the trace obtained is a model of the formula () ∧ ( → ).
Example 4. Consider again the smart contract discussed in Example 1 and the partial trace = {}, {}. This smart contract can be satisfied at runtime starting from , and examples of completions of are: 1={}, {}, {} 2={}, {}, {}, {}, {}
The previous section considered reasoning problems defined on individual smart contracts. It is also interesting in the context of blockchains to consider problems defined on a set of smart contracts, which are supposed to operate and interact in the same blockchain infrastructure.
Model checking. Given a set of smart contracts {⟨1, 1⟩, ⟨2, 2⟩, ..., ⟨, ⟩} encoded by the LTL formulas 1 = (1 → 1), 2 = (2 → 2),... , = ( → ), the goal is to verify if a given trace is a model of 1, 2, ..., . To this end, we can use the same approach used for the model checking of a single smart contract, but defining appropriately the LTL formula encoding the set. In particular, since no smart contracts must be violated by the trace, we can consider the formula = 1 ∧ 2 ∧ ... ∧ .
Example 5. Consider the smart contract consisting of the following clause: if a user shares a content that has been previously transmitted to him, thus violating contractual terms, that user will be deleted from the system. The propositional variables used for the encoding are: ℎ (the user shares the content), (the content is transmitted to the user) and (the user is deleted from the system). The precondition of the smart contract is = ℎ ∧ (). The efect is the deletion of the user from the system which is considered to be made in the time instant immediately following the sharing = ( ). The smart contract is encoded by the following formula: 2 = ((ℎ ∧ ()) → ( )). If we consider that 2 and the smart contract discussed in Example 1 (consisting of the LTL formula 1 = (( ∧ ()) → ())) are running on the same blockchain; we can perform model checking by considering the LTL formula = 1 ∧ 2. Let’s consider the following trace: = smart contracts formalized by it. {}, {}, {}, {}, {, ℎ}, { }. It is easy to verify that satisfies and it’s compliant with the two Consistency of a set of smart contracts. If we consider a set of smart contracts running on the same blockchain, another relevant problem is to verify their consistency, i.e. if it is possible that all smart contracts can sooner or later be executed or if they are incompatible with each other, meaning that the execution of one of them makes another smart contract never executable. The goal is to check if there is a trace in which all the smart contracts in the set have been executed at least ⋀︀ once. Let’s consider a set of smart contracts {⟨1, 1⟩, ..., ⟨, ⟩} encoded by the LTL formulas 1=(1 → 1), . . . , =( → ). Then, the LTL formula for consistency checking is ∈{1,...,}(( → ) ∧ ()), that is, the conjunction of the formulas encoding the individual smart contracts plus the check that the preconditions of each smart contract have been satisfied at least once = (using the () subformulas). ℎ} { }.
Consider the set of smart contracts discussed in Example 5.
This set of smart contracts is consistent, in fact we found a trace satisfying this set.
Let: ′1′=(( ∧ ())→() and ′2′=((ℎ ∧ ()) sistency of the set is:
→ (ℎ ∧ ()).
( ).
The LTL formula allowing to check the con= ( ′1′) ∧ ( ′2′) ∧ ( ∧ ()) ∧
A trace that satisfies is the following: = {}, {}, {}, {}, {,
Consider the two smart contracts within the sharing economy environment ⟨1=( ∧ (¬)), 1=⟩ and ⟨2= ( ∧ (¬)), 2=). The smart contract ⟨1, 1⟩ establishes that if the owner of a content ask for its deletion () and previously such content has not been declared not deletable ((¬)), the content is deleted from the system. Instead, the smart contract ⟨2, 2⟩ states that if a content is requested to be made permanent in the system ( ) and has not been previously deleted ((¬)) then it is marked as not deletable. It is easy to see that this set of smart contracts is not consistent since the execution of one smart contract prevents the precondition of the other to be ever satisfied.
Consistency at runtime. Consistency at runtime is the problem of checking if a set of smart contracts {⟨1, 1⟩, ..., ⟨, ⟩} can be satisfied starting from a partial trace , that is to verify whether there exists a completion = of (obtained by adding to a subtrace ) such that all smart contracts in the set are executed at least once. To solve such a problem the encoding of the set of smart contracts in LTL is the same as discussed for the standard consistency checking. However, the partial trace must be completed by adding indicator variables to register the satisfaction of preconditions. Example 8. Consider again the set of smart contracts discussed in Example 6 and the partial trace ={}, {}. The completion of corresponds to the addition of the indicator variable 1 in the last state, i.e., ={}{, 1}. The set of smart contracts is consistent at runtime starting from , and examples of completions of are: 1={}, {, 1}, {, ℎ, 2}, { } 2={}, {, 1}, {}, {, , ℎ, 1, 2}, {, }
In this section we introduce the Smart Contracts Reasoner (SCRea) that works on smart contracts
encoded in LTL and exploits boolean satisfiability for solving the reasoning tasks introduced in the
previous section. The proposed reasoner is based on a SAT (boolean satisfiability) rewrite technique
that recalls the approach followed by (incremental) model checking methods for bounded LTL [
The first component is the Parser which constructs the parse tree ( ) associated with the input
formula . Starting from the parse tree, the SAT rewriting technique rewrites into an equivalent
propositional formula Φ, which is satisfiable if, and only if, can be satisfied by a model of maximum
length . To verify if Φ, is satisfiable, the reasoner can use any existing SAT solver (e.g., Glucose
[
Given an LTL formula representing one or a set of smart contracts, for its SAT encoding a crucial role is played by the parse tree of a formula ( ) = (, , ) that is a tree (, ) with a node labeling function : → {∧, ∨, , , , , } ∪ {, ¬| ∈ } inductively defined as follows: ∙ For any literal ∈ {, ¬} with ∈ , () = ({}, ∅, ) and () = . ∙ If ( )=(, , ), with ∈ {1, 2}, it is an analysis tree having as root the vertex ∈ and if ∈ ∧, ∨ is a boolean connective or = then ( 1 2) = ({} ∪ 1 ∪ 2, {(, 1), (, 2)} ∪ 1 ∪ 2, ) is the analysis tree which has as roots the new node , with 1 and 2 as its two children, and where is such that () = and its restriction on coincides with . ∙ If ( ′)=( ′, ′, ′) is an analysis tree having the root ′ and if ∈ {, , , } is a time operator, then (( ′))=({} ∪ ′, {(, ′)} ∪ ′, ) is the tree rooted in the new node whose only child is ′ and where is such that ()= and its restriction on ′ coincides with .
To explain the encoding approach used by the reasoner to construct Φ, , let us first note that, given a trace , each node ∈ of the parse tree ( ) = (, , ) can easily be equipped with a set (, ) of all time instants in which the sub-formula associated with vertex holds in . In particular, such sets can be computed by structural induction on the parse tree according to the semantics of the diferent temporal operators. Then, the basic idea we use to construct the formula Φ, is to imitate the construction of the sets (, ). Formally, we first define the variables [0], ..., [ − 1] that will be used to encode the last time instant of the model. Intuitively, Φ, will be defined in such a way that there exists an index ∈ {0, ..., − 1}, such that [] evaluates true (respectively, false) whenever ≥ (respectively, < ). The instant indicates the last time instant of a model of – more formally, whenever Φ, is satisfiable, there exists a model of of length ≤ . Then, we associate the variables [0], ..., [ − 1] to each node of ( ). Intuitively, [] is meant to check if the formula encoded in the parse tree rooted at node is satisfied at instant . In the following expressions, we use two additional variables [− 1] and [], whose value will actually be a constant that will be fixed depending on the type of node .
Then, the SAT encoding is the formula Φ,
= ⋀︀∈ (Φ ∧ [-1] ∧ [-1]) ∧ ⋀︀=− 02([] → [ + 1]) ∧ ⋀︀=− 02([] → ⋀︀([] ↔ [ + 1])) and, for all ∈ , Φ = [0] ↔ Φ0 ⋀︀=− 11(¬[-1] → ([] ↔ Φ)), where: ∙ if () ∈ {, ¬}, then Φ = ⋀︀′∈, (′)≡¬ () ¬′[] ∧ ⋀︀′∈, (′)≡ () ′[]; ∙ if ()=∧ or ()=∨, then Φ=1[] ()2[], where 1 and 2 are the right/left children of ; ∙ if ()=, then Φ=′[ + 1] ∧ ¬[], where ′ is the child of and [] is the constant false; ∙ if ()= , then Φ=′[ − 1], where ′ is the child of and [− 1] is the constant false; ∙ if ()= , then Φ=′[] ∨ [ − 1], where ′ is the child of and [− 1] is the constant false; ∙ if ()=, then Φ=′[] ∧ [ − 1], where ′ is the child of and [− 1] is the constant true; ∙ if ()=, then Φ=(2[] ∧ 1[]) ∨ (1[] ∧ [ − 1]), where 1 and 2 are the left and right children of and [− 1] is the constant false.
We note, for the sake of completeness, that Φ, is rewritten (in polynomial time) in conjunctive normal form, before being passed to the solver. Moreover, by construction, it is possible to establish that Φ, is satisfiable if, and only if, can be satisfied by a model with ( ) ≤ . When SCRea finds a model for a SAT formula Φ, , the decoder module is responsible for the building of the trace that satisfies the smart contract . In particular, starting from it is possible to construct the trace satisfying by implementing the following steps: (i) If [] ∈ and there is no [] ∈ with < then the decoder constructs a trace with states; (ii) For every such that () = and every such that [] ∈ then the decoder adds to [].
In this section we will discuss how the reasoner can be applied to solve reasoning problems at runtime. To work at runtime it is necessary to slightly modify the architecture of SCRea. In particular, the Encoder module must also receive in input the partial trace which contains the events recorded on the blockchain up to the current time instant. In this case, the parameter concerns the additional number of states (i.e., sets of events) that can happen after those already present in . Moreover, if SCRea is meant to work on a set of smart contracts must be preprocessed to add indicator variables. In this paper we proposed a framework, based on the encoding of smart contracts in Linear Temporal Logic on finite traces, that enables various reasoning tasks on a single and on a set of smart contracts running on the same blockchain. The proposed framework, called SCRea, is the first tool developed with the aim of checking the consistency of a set of smart contracts that are supposed to cooperate in same blockchain infrastructure and it is able to work at runtime on a running blockchain system. As a first line for future research, we are planning to implement our framework on an existing blockchain infrastructure to test its efectiveness on a real system. As a limitation of the proposed framework we want to point out that LTL is based on a propositional logic and, thus, has some limitations in expressiveness. Therefor, a second line for future research regards the extension of the proposed framework with a more powerful logic such as first-order temporal logic that will increase SCRea’s expressive power.