Towards FATEful Smart Contracts⋆

Abstract

Achieving fair, accountable, transparent, and ethical decentralized finance requires activating enabling properties at the level of smart contracts, the executable scripts at its basis. In this vision paper, a joint efort of the Central Bank of Italy, TU Wien, and the University of Oxford, we leverage the vast amount of experience in this sense from the database community and propose a logic-based reasoning framework that captures smart contracts as a set of rules in DatalogMTL, a temporal language for querying databases. We present the high-level architecture of our framework and explain how the theoretical underpinnings of the reasoning of DatalogMTL convey important properties to the approach.

Keywords

• Smart contracts
• DatalogMTL
• FATE principles

1. Introduction

The Artificial Intelligence and database communities are experiencing a growing infusion of thFeATE (Fairness, Accountability, Transparency, Ethics) principles [ 2 ]. These principles are gaining prominence, drawing attention to the non-functional requirements of everyday AI-assisted and data-driven decisionmaking and catalyzing the discussion around regulatory bodies. Unfortunately, the same level of attention to these high-level concerns is not mirrored in developer circles, and recent studies underscore the scant regard machine learning developers have shown for FATE concerns in machine learning applications [ 3, 4 ].

FATE and DeFi. We see similar patterns emerging when assessing developers’ awareness of FATE concerns within the industrial realm oDfecentralized Finance (DeFi). DeFi entails financial transactions devoid of intermediaries, instead relying on software modules executed on a decentralized public ledger [ 5 ]. At the core of DeFI is the notion ofsmart contracts [ 6 ], which are machine-readable and executable agreements that establish and enforce the binding terms for the parties involved. Supporting FATE. In the AI and data world, social forces have been efective in supporting FATE, for example, by means of third-party audits of the algorithms, either conducted by experts or by everyday users. As recently highlighted by Hong in CACM2[], prominent examples can be found in the fights against the racial bias of face-recognition systems7[], and commercial gender disparities in photo cropping or credit card algorithms8[]. These audits, spurred by social forces and the scientific community, have provided regulators with positive guidance.

In contrast to AI, DeFi boasts a substantial theoretical transparency advantage, thanks to its openaccess code and the ability for anyone to inspect smart contract data on a public ledger. However, enforcing policies in a decentralized context remains an incredibly challenging task. The praiseworthy goal of establishing standards, taxonomies, compliance measures, quality controls, and upholding

CEUR

ceur-ws.org ethical principles 9[] can benefit from robust support from the social forces in the monitoring and enforcement of such policies. However, this must align with the specific technical attributes of these smart contracts. Yet, smart contracts have been criticised within the community due to their overly complex business logic, and limited explainability, resulting in a lack of transparency. Furthermore, they often prove challenging to describe and communicate, rendering them less user-friendly, particularly for non-technical users 1[ 0, 11, 12 ].

A Knowledge Representation and Reasoning (KRR) approach to smart contracts. In the area of deductive AI and ontological reasoning on databases, logic-based approaches built on top of KRR formalisms are gaining increasing attention in industrial settings, with many successful financial applications [ 13, 14, 15 ]. Modern logical languages manage to strike a good balance between expressive power and computational complexity, resulting in compact and eficiently executable formalizations of complex domains, for instance, being able to capture SPARQL under OWL 2 entailment regime1s6[] and so enabling ontological reasoning. Thedeclarative paradigm sustains simplicity, transparency, compactness, and understandability of code, which becomes algorithm-independent and closer to the high-level specifications, policies, and standards. Thewell-defined semantics of KRR languages fosters non-ambiguity, ease of use for non-technical users, and correctness. The intrinssitcep-by-step nature of logical reasoning is conceptually close to notions ofexplainability and thus supports decision transparency.

The thesis of this vision paper is that a KRR framework for smart contracts that addresses FATE by design is both theoretically and practically viable. For the theory, we show that, by building on the underpinnings of logic-based reasoning, the features important to achieving FATE desiderata can be obtained and rigorously justified. In terms of application, we show that our framework is adaptable to serve as both an interpreted and a compiled execution mode for real-world contracts.

Contributions to industrial advances. In recent industrial EDBT work done by the Central Bank of Italy [ 17 ], they started to investigate the possibility of encoding complex smart contracts in DatalogMTL [ 18, 19 ], a temporal extension of the Datalog language20[] of databases. They obtained promising results, highlighting the potential of a KRR approach in the specific case of a derivative contract. In this work, a joint efort of the Central Bank of Italy, TU Wien, and the University of Oxford, we propose (i) afull-fledged and general framework for smart contracts that sustains FATE concerns (ii) by leveraging the vast amount oefxperience from the database community to achieve enabling properties; (iii) using our framework to study and implementproof of concepts for many smart contracts where FATE is a core desideratum of a central bank. More details can be found in the full version of the paper 1[].

2. Overview of the Framework and Related Work

We use a form of declarative logical object-oriented approach and encode the behaviour of aclass of smart contracts as a set Σ of reasoning rules—or programs—working on a databas e of temporal facts. A temporal fact of is such that it holds in a given time interval, for example, price(123, 2)@[2023-09-01,2023-09-02] defines the price 2 for the asset123 in a two-day interval.

To model the rules ofΣ, we introduceDatalogMTL , a variant of DatalogMTL with features of practical utility. A smart contract is then aninstance of a smart contract class, whose time-dependent status is represented as a database of temporal facts. Instances arestateful objects and the contract execution consists in invocations, akin to method calls, that are carried out by the involved parties. Calls result in updates to the status through the addition of new facts. The semantics of a call is operationally described as the application of the rules oΣf (denoted asΣ() ) to the temporal facts of , extended with call-specific facts.

DatalogMTL rules are sets ofhead←body logic implications where the body is a conjunction of atoms and the head is an atom. As a general guideline, whenever the body of a rule is satisfied by a conjunction of facts in at a point in time , the evaluation of the rule triggers the insertion i n of a new fact for the head atom, holding at. For example, the rule p‘osition(, ) ← buy(, , ), price(, ), = ∗ ’ states that, for every point in time , the position of a trader that buys an amount of an asset of price is obtained as ∗ . So, if contains the price factprice(123, 2) and buy(0241 , 123, 12) , both holding at[2023-09-01,2023-09-02], a new position(0x241F, 24) holding in the same time interval will be added to .

In DatalogMTL , temporal operators can be used to either modify the temporal binding of body atoms to facts of , or to alter the temporal validity of the generated facts. For instance, an expression of the form ♦−[ 0,1 ]position(, ) in the body holds at a point in time , if the trader had at least an open position in the interval[ − 1, ] , while an expression of the form⊞[ 0,1 ]position(, ) in the head, states that the position will be open in the interva[l, + 1] for every . In the following, we show a smart contract class defining a simple financial market: 2∶ ⊞−position(, , ) ← accepted(, ), price(), = ∗ . 1∶ accepted($sender, ) ← # open( ) , ¬marketClosed.

3∶ return(x, g), ⊞−position(, , 0) ← # close(), price(), position($sender, , ), = ∗ − . At a specific point in time in which the market is not closed, a trader tries to open a position by investing an amount (Rule 1 ). The constant$ is a call-level variable that at runtime binds to the invoking updated by multiplying by the current price . The ⊞− operator stands for a new future temporal validity trader. When the transaction is accepted (Rul2e ), the position of the trader on the amount is of the position fact. Finally, when the position is closed (Rul3e ), the final profit is computed based on the current price.

Execution modes. From a practical perspective, our framework implementΣs() by enabling three execution alternatives, each ofering specific properties, as reported in Figure 1: (i) on-reasoner execution: the rules are applied natively by a reasoning system supporting DatalogMTL oDratalogMTL such as Temporal Vadalog [ 21 ] or MeTeoR [ 22 ]; (ii) on-chain execution: the DatalogMTL programs are verifiably translated into the language of a target system, for instancSeo,lidity [ 23 ] or Bitcoin Script [ 24 ] and executed within the target systems; (iiio)f-chain execution , the rules are applied with an on-reasoner execution with persistent efects on a blockchain and cryptographically verifiable computation.

The expert intention is substantiated as a natural language (NL) contract or directly encoded in a DatalogMTL program Σ, and the use of large language models (LLM) can bridge the gap between the natural language specification of the contract and the encoding of its DatalogM TLversion [ 25 ].

In the on-reasoner execution mode, to evaluateΣ, reasoners use variants of thechase procedure [26] specialized for the temporal extensions2[ 7 ]. They ofer a good degree of explainability of the produced facts as a side efect of the inference process of the chase. Also, they are suited to be used fsoirmulation and runtime verification purposes as step-by-step debugging can be emulated by incrementally adding facts to and monitoring the results entailed by the application oΣf. On the other hand, the execution relies on a trusted centralized system.

Conversely, on-chain execution ofers a trustless paradigm, only requiring that the user acknowledges the translation of theDatalogMTL code into the target language, which can be verified through opensourced translators. This trustlessness is underpinned by the validation properties ensured by the distributed consensus protocol embraced by the blockchain, guaranteeing the integrity of the mined blocks. What is more, on-chain execution is characterized by ittismeliness, as results are promptly included in the first mined block.

However, on-chain execution comes with a high cost and is ill-suited for complex applications. In contrast, of-chain execution is widely regarded as a practical and eficient alternative, and there is a large body of related work such as state-channels28[], Plasma [29], and Zero-Knowledge Rollups [30]. In particular, specific protocols have been proposed, that help attest the integrity of of-chain computation (i.e., verifiable computation ), such as ZK-SNARK [31] and ZK-STARK [32]. Towards this direction, the construction of specialized virtual machines compiling succinct ZK proofs foDratalogMTL executions is envisaged here, but beyond the scope of this vision paper and a matter of future work. Termination and Complexity. Fact entailment in DatalogMTL is a decidable task, in particular PSPACE in data complexity [ 18 ]; therefore we haveguaranteed termination andguaranteed computational complexity. Moreover, the rules modelling real-world smart contracts need to allow for the derivation of facts into present and future time points, while the propagation towards the past is almost never required. Under this condition, the setΣ belongs to the forward-propagating fragment, namely, DatalogMTLFP [ 18 ], for which afinite representation of infinite models is always possible [ 19 ]. It is important to point out that in DatalogMTL the use of arithmetic and recursion can, in general, lead to undecidabili3t3y][ and a comprehensive study of arithmetic in DatalogMTL has not been provided yet. However, our framework conditions the activations of the rules on the specific smart contract functions being called, which reduces the cases of potentially harmful recursion.

3. The Framework in Action

In this section, we show the usefulness of our framework with a smart contract of industrial relevance. ERC-20. The ERC-20 [34] is a well-known and widely adopted Token Standard that implements an API for tokens within smart contracts. The followingDatalogMTL smart contract implements a simple ERC-20 contract with a fixed supply .

1∶ ⊞ totalSupply(), ⊞−balanceOf ($sender, ) ← # init(). 2∶ ⊞−balanceOf ($sender, 0) ← ¬balanceOf ($sender, ), # create(). 3∶ ⊞−balanceOf ($sender, − ) , ⊞−balanceOf (to, + ) ← balanceOf ($sender, ), balanceOf (to, ), ≥ , # transfer(to, ).

Atoms with predicates#init, create, and #transfer are calledtrigger atoms and represent contract functions, while atoms withbalanceOf and totalSupply are status atoms and they persist across state 1 initializes the smart contract state by adding the fac⊞tstotalSupply() and ⊞−balanceOf ($sender, ) . transitions. Other atoms aretransient and they are discarded at the end of each function evaluation. Rule Note that using the⊞− operator allows to overwrite the balance in case of a transfer. Ru2le allows the sender to initialize a balance, if not already done earlier. Ru3le implements the “transfer” function from the sender address$sender to the recipient addressto of amount . Atoms of the form balanceOf ( address, ) in the body are used to query the balance of address (a common pattern in logic procomplete the transfer, and the head of the rule uses th⊞−e to update the balances accordingly. We gramming), the condition ≥ imposes that there is enough balance from the sender account to omitted allowances and thetransferFrom and approve functions.

Compilation to Solidity. In [ 1 ] we outlined an approach to compileDatalogMTL programs into Solidity code that implements the same contract. Intuitively, rules with trigger atoms in the body are translated into functions, and status atoms are translated into contract state variables and data structures. Figure2 shows an example of how we can translate the ERC-2D0atalogMTL program into Solidity.

Formal Verification. Our framework can enable formal verification of smart contracts written in DatalogMTL . An example of how formal properties can be verified is by additional program rules that formalizeinvariants in the DatalogMTL language. These are formalized using rules of the form ⊥ ← 1, … , , meaning that, if all expression s 1, … , are true (that is, the invariant does not hold), then the function call that triggered that rule must be reverted. These rules are compiled inatsosert instructions and can be seen as a runtime verification technique that rejects all transactions that violate the invariants, as in 3[ 5 ]. For example, in the ERC-20 smart contract, we might add some invariant conditions that must be true at any time during the lifetime of the smart contract, such as: • The sum of user balances is equal tototalSupply [36] (the operatormsum is an aggregation operator that computes the sum, see 3[ 7, 27 ])

actualTotalSupply(msum(⟨()⟩) ← balanceOf (_, ).

⊥ ← actualTotalSupply( 1), totalSupply( 2), 1! = 2. • The sums of sender and receiver balances before and after the transfer are equa3l8[]: ⊥ ←♦−[ 1,1 ]#transfer (), address(), ♦−[ 1,1 ]balanceOf ($sender, ), ♦−[ 1,1 ]balanceOf (, ),

balanceOf ($sender, ′), balanceOf ($sender, ′), + = ′ + ′.

4. Conclusion

This preliminary work proposes a framework for expressing and evaluating smart contracts, focusing on improving the explainability and transparency of traditional smart contract development. We achieve this by building on decades of research in KRR, particularly in declarative logic-based programming, leveraging the expressive power of DatalogMTL. Inspired by a recent application of such formalism for modelling smart contracts 3[ 9, 17 ], we generalize those approaches and develop a foundational framework which supports the formalization and evaluation of arbitrary smart contracts. While in this paper we focused more on the vision and its industrial applications in the financial sector, we can already foresee many research avenues as future works. First, we aim to develop novel techniques (e.g., zeroknowledge techniques for of-chain execution) and implementations for realizing each execution mode. Next, it would be interesting to investigate the impact of developing smart contracts iDnatalogMTL , in terms of ease of use, explainability, and code quality. Finally, we want to devise and apply formal verification techniques for DatalogMTL smart contracts. language models via ontological reasoning, in: International Joint Conference on Rules and Reasoning, Springer, 2023, pp. 86–94. [26] D. Maier, A. O. Mendelzon, Y. Sagiv, Testing implications of data dependencies, ACM Transactions on Database Systems 4 (1979) 455–468. [27] L. Bellomarini, M. Nissl, E. Sallinger, Monotonic aggregation for temporal datalog, in: RuleML+RR (Supplement), volume 2956 of CEUR Workshop Proceedings, CEUR-WS.org, 2021. [28] A. Miller, I. Bentov, S. Bakshi, R. Kumaresan, P. McCorry, Sprites and state channels: Payment networks that go faster than lightning, in: Financial Cryptography, volume 11598 Lofecture Notes in Computer Science, Springer, 2019, pp. 508–526. [29] M. Harishankar, D. Akestoridis, S. V. Iyer, A. Laszka, C. Joe-Wong, P. Tague, Plasma go: A scalable sidechain protocol for flexible payment mechanisms in blockchain-based marketplaces, CoRR abs/2003.06197 (2020). [30] Ethereum.org, Zero-knowledge rollups,https://shorturl.at/wIYZ4, 2023. Last accessed on 2022-1128. [31] T. Chen, H. Lu, T. Kunpittaya, A. Luo, A review of zk-snarks, CoRR abs/2202.06877 (2022). [32] E. Ben-Sasson, I. Bentov, Y. Horesh, M. Riabzev, Scalable, transparent, and post-quantum secure computational integrity, IACR Cryptol. ePrint Arch. (2018) 46. [33] B. C. Grau, I. Horrocks, M. Kaminski, E. V. Kostylev, B. Motik, Limit datalog: A declarative query language for data analysis, SIGMOD Rec. 48 (2019) 6–17. [34] Ethereum Improvement Proposals, ERC-20: Token Standard, 2015. URLh:ttps://eips.ethereum.org/

EIPS/eip-20. [35] A. Li, J. A. Choi, F. Long, Securing smart contract with runtime validation, in: PLDI, ACM, 2020, pp. 438–453. [36] Á. Hajdu, D. Jovanović, solc-verify: A modular verifier for solidity smart contracts, in: Verified Software. Theories, Tools, and Experiments: 11th International Conference, VSTTE 2019, New York City, NY, USA, July 13–14, 2019, Revised Selected Papers 11, Springer, 2020, pp. 161–179. [37] A. Shkapsky, M. Yang, C. Zaniolo, Optimizing recursive queries with monotonic aggregates in deals, in: ICDE, 2015, pp. 867–878. [38] L. Alt, C. Reitwießner, Smt-based verification of solidity smart contracts, in: ISoLA (4), volume 11247 of Lecture Notes in Computer Science, Springer, 2018, pp. 376–388. [39] M. Nissl, E. Sallinger, Modelling smart contracts with datalogmtl, in: EDBT/ICDT Workshops, volume 3135 of CEUR Workshop Proceedings, CEUR-WS.org, 2022.

References

[1] L. Bellomarini , M. Favorito , E. Laurenza, M. Nissl , E. Sallinger, Toward fateful smart contracts , in: DLT, CEUR Workshop Proceedings, CEUR-WS.org, 2024 .

[2] J. I. Hong , Teaching the fate community about privacy , Commun. ACM 66 ( 2023 ) 10 - 11 .

[3] Á. A. Cabrera , E. Fu , D. Bertucci , K. Holstein , A. Talwalkar , J. I. Hong , A. Perer , Zeno: An interactive framework for behavioral evaluation of machine learning , in: CHI, ACM , 2023 , pp. 419 : 1 - 419 : 14 .

[4] T. Li , Y. Agarwal , J. I. Hong , Coconut: An IDE plugin for developing privacy-friendly apps , Proc. ACM Interact. Mob. Wearable Ubiquitous Technol . 2 ( 2018 ) 178 : 1 - 178 : 35 .

[5] E. Napoletano , B. Curry , What is defi? understanding decentralized finance , http://bitly.ws/xd7Y, 2021 . Last accessed on 2022- 11 -28.

[6] I. Swaps , D. Association , Legal guidelines for smart derivatives contracts: the isda master agreement , 2019 .

[7] P. E. Naeini , J. Dheenadhayalan , Y. Agarwal , L. F. Cranor , An informative security and privacy ”nutrition” label for internet of things devices , IEEE Secur. Priv . 20 ( 2022 ) 31 - 39 .

[8] J. Buolamwini , T. Gebru, Gender shades: Intersectional accuracy disparities in commercial gender classification , in: FAT , volume 81 of Proceedings of Machine Learning Research, PMLR , 2018 , pp. 77 - 91 .

[9] Bank of Italy, Public consultation on the working document relating to phase one of the research project on smart contracts ,https://bit.ly/3xQKRL8, 2023 . [Online; accessed 3-May-2024].

[10] G. Ciatto , R. Calegari , S. Mariani , E. Denti , A. Omicini , From the blockchain to logic programming and back: Research perspectives , in: WOA, 2018 , pp. 69 - 74 .

[11] M. Li , J. Weng , A. Yang , J. Weng , Y. Zhang, Towards interpreting smart contract against contract fraud: A practical and automatic realization , Cryptology ePrint Archive , Paper 2020 /574, 2020 . URL: https://eprint.iacr.org/ 2020 /574, https://eprint.iacr.org/ 2020 /574.

[12] E. Regnath , S. Steinhorst , Smaconat: Smart contracts in natural language , in: 2018 Forum on Specification and Design Languages (FDL) , 2018 , pp. 5 - 16 . doi: 10 .1109/FDL. 2018 . 8524068 .

[13] A. Hogan , E. Blomqvist, M. Cochez , C. d'Amato, G. de Melo, C. Gutierrez , J. E. L. Gayo , S. Kirrane , S. Neumaier , A. Polleres , R. Navigli , A. N. Ngomo , S. M. Rashid , A. Rula , L. Schmelzeisen , J. F. Sequeda , S. Staab , A. Zimmermann , Knowledge graphs , CoRR abs/ 2003 .02320 ( 2020 ).

[14] T. Baldazzi , L. Bellomarini , E. Sallinger, Reasoning over financial scenarios with the vadalog system, in: EDBT, OpenProceedings .org, 2023 , pp. 782 - 791 .

[15] L. Bellomarini , D. Fakhoury , G. Gottlob , E. Sallinger, Knowledge graphs and enterprise AI: the promise of an enabling technology , in: ICDE, IEEE, 2019 , pp. 26 - 37 .

[16] G. Gottlob , A. Pieris , Beyond SPARQL under OWL 2 QL entailment regime: Rules to the rescue , in: IJCAI , 2015 , pp. 2999 - 3007 .

[17] A. Colombo , L. Bellomarini , S. Ceri , E. Laurenza, Smart derivative contracts in datalogmtl , in: EDBT, OpenProceedings.org, 2023 , pp. 773 - 781 .

[18] P. A. Walega , B. C. Grau , M. Kaminski , E. V. Kostylev , Datalogmtl: Computational complexity and expressive power, in: IJCAI, ijcai .org, 2019 , pp. 1886 - 1892 .

[19] L. Bellomarini , M. Nissl , E. Sallinger, Query evaluation in datalogmtl - taming infinite query results , CoRR abs/2109 .10691 ( 2021 ).

[20] S. Ceri , G. Gottlob , L. Tanca, What you always wanted to know about datalog (and never dared to ask) , TKDE 1 ( 1989 ) 146 - 166 .

[21] L. Bellomarini , L. Blasi , M. Nissl , E. Sallinger, The temporal vadalog system , in: RuleML+RR , volume 13752 of Lecture Notes in Computer Science, Springer, 2022 , pp. 130 - 145 .

[22] D. Wang , P. Hu , P. A. Walega , B. C. Grau , Meteor: Practical reasoning in datalog with metric temporal operators , in: AAAI, AAAI Press, 2022 , pp. 5906 - 5913 .

[23] T. S. Authors , Solidity documentation,https://docs.soliditylang. org/en/v0.8 .21,/ 2023 . [Online; accessed 12-Oct-2023].

[24] B. Wiki , Script, https://en.bitcoin.it/wiki/Script, 2023 . [Online; accessed 12-Oct-2023].

[25] T. Baldazzi , L. Bellomarini , S. Ceri , A. Colombo , A. Gentili , E. Sallinger, Fine-tuning large enterprise