-
Smart Contract Languages: a comparative analysis
Authors:
Massimo Bartoletti,
Lorenzo Benetollo,
Michele Bugliesi,
Silvia Crafa,
Giacomo Dal Sasso,
Roberto Pettinau,
Andrea Pinna,
Mattia Piras,
Sabina Rossi,
Stefano Salis,
Alvise Spanò,
Viacheslav Tkachenko,
Roberto Tonelli,
Roberto Zunino
Abstract:
Decentralized blockchain platforms support the secure exchange of assets among users without relying on trusted third parties. These exchanges are programmed with smart contracts, computer programs directly executed by blockchain nodes. Multiple smart contract languages are available nowadays to developers, each with its own distinctive features, strengths, and weaknesses. In this paper, we examin…
▽ More
Decentralized blockchain platforms support the secure exchange of assets among users without relying on trusted third parties. These exchanges are programmed with smart contracts, computer programs directly executed by blockchain nodes. Multiple smart contract languages are available nowadays to developers, each with its own distinctive features, strengths, and weaknesses. In this paper, we examine the smart contract languages used in six major blockchain platforms: Ethereum, Solana, Cardano, Algorand, Aptos, and Tezos. Starting with a high-level overview of their design choices, we provide a comprehensive assessment that focuses on programming style, security, code readability, and usability, drawing on an original benchmark that encompasses a common set of use cases across all the smart contract languages under examination.
△ Less
Submitted 5 April, 2024;
originally announced April 2024.
-
From Legal Contracts to Legal Calculi: the code-driven normativity
Authors:
Silvia Crafa
Abstract:
Using dedicated software to represent or enact legislation or regulation has the advantage of solving the inherent ambiguity of legal texts and enabling the automation of compliance with legal norms. On the other hand, the so-called code-driven normativity is less flexible than the legal provisions it claims to implement, and transforms the nature of legal protection, potentially reducing the capa…
▽ More
Using dedicated software to represent or enact legislation or regulation has the advantage of solving the inherent ambiguity of legal texts and enabling the automation of compliance with legal norms. On the other hand, the so-called code-driven normativity is less flexible than the legal provisions it claims to implement, and transforms the nature of legal protection, potentially reducing the capability of individual human beings to invoke legal remedies.
In this article we focus on software-based legal contracts; we illustrate the design of a legal calculus whose primitives allow a direct formalisation of contracts' normative elements (i.e., permissions, prohibitions, obligations, asset transfer, judicial enforcement and openness to the external context). We show that interpreting legal contracts as interaction protocols between (untrusted) parties enables the generalisation of formal methods and tools for concurrent systems to the legal setting
△ Less
Submitted 6 September, 2022;
originally announced September 2022.
-
Pacta sunt servanda: legal contracts in Stipula
Authors:
Silvia Crafa,
Cosimo Laneve,
Giovanni Sartor
Abstract:
There is a growing interest in running legal contracts on digital systems, at the same time, it is important to understand to what extent software contracts may capture legal content. We then undertake a foundational study of legal contracts and we distill four main features: agreement, permissions, violations and obligations. We therefore design Stipula, a domain specific language that assists la…
▽ More
There is a growing interest in running legal contracts on digital systems, at the same time, it is important to understand to what extent software contracts may capture legal content. We then undertake a foundational study of legal contracts and we distill four main features: agreement, permissions, violations and obligations. We therefore design Stipula, a domain specific language that assists lawyers in programming legal contracts through specific patterns. The language is based on a small set of abstractions that correspond to common patterns in legal contracts, and that are amenable to be executed either on centralized or on distributed systems. Stipula comes with a formal semantics and an observational equivalence, that provide for a clear account of the contracts' behaviour. The expressive power of the language is illustrated by a set of examples that correspond to template contracts that are often used in practice.
△ Less
Submitted 21 October, 2021;
originally announced October 2021.
-
Solidity 0.5: when typed does not mean type safe
Authors:
Silvia Crafa,
Matteo Di Pirro
Abstract:
The recent release of Solidity 0.5 introduced a new type to prevent Ether transfers to smart contracts that are not supposed to receive money. Unfortunately, the compiler fails in enforcing the guarantees this type intended to convey, hence the type soundness of Solidity 0.5 is no better than that of Solidity 0.4. In this paper we discuss a paradigmatic example showing that vulnerable Solidity pat…
▽ More
The recent release of Solidity 0.5 introduced a new type to prevent Ether transfers to smart contracts that are not supposed to receive money. Unfortunately, the compiler fails in enforcing the guarantees this type intended to convey, hence the type soundness of Solidity 0.5 is no better than that of Solidity 0.4. In this paper we discuss a paradigmatic example showing that vulnerable Solidity patterns based on potentially unsafe callback expressions are still unchecked. We also point out a solution that strongly relies on formal methods to support a type-safer smart contracts programming discipline, while being retro-compatible with legacy Solidity code.
△ Less
Submitted 5 July, 2019;
originally announced July 2019.
-
On the chemistry of typestate-oriented actors
Authors:
Silvia Crafa,
Luca Padovani
Abstract:
Typestate-oriented programming is an extension of the OO paradigm in which objects are modeled not just in terms of interfaces but also in terms of their usage protocols, describing legal sequences of method calls, possibly depending on the object's internal state. We argue that the Actor Model allows typestate-OOP in an inherently distributed setting, whereby objects/actors can be accessed concur…
▽ More
Typestate-oriented programming is an extension of the OO paradigm in which objects are modeled not just in terms of interfaces but also in terms of their usage protocols, describing legal sequences of method calls, possibly depending on the object's internal state. We argue that the Actor Model allows typestate-OOP in an inherently distributed setting, whereby objects/actors can be accessed concurrently by several processes, and local entities cooperate to carry out a communication protocol. In this article we illustrate the approach by means of a number of examples written in Scala Akka. We show that Scala's abstractions support clean and natural typestate-oriented actor programming with the usual asynchronous and non-blocking semantics. We also show that the standard type system of Scala and a typed wrap** of usual (untyped) Akka's ActorRef are enough to provide rich forms of type safety so that well-typed actors respect their intended communication protocols. This approach draws on a solid theoretical background, consisting of a sound behavioral type system for the Join Calculus, that is a foundational calculus of distributed asynchronous processes whose semantics is based on the Chemical Abstract Machine, that unveiled its strong connections with typestate-oriented programming of both concurrent objects and actors.
△ Less
Submitted 11 July, 2016;
originally announced July 2016.
-
Modelling the Evolution of Programming Languages
Authors:
Silvia Crafa
Abstract:
Programming languages are engineered languages that allow to instruct a machine and share algorithmic information; they have a great influence on the society since they underlie almost every information technology artefact, and they are at the core of the current explosion of software technology. The history of programming languages is marked by innovations, diversifications, lateral transfers and…
▽ More
Programming languages are engineered languages that allow to instruct a machine and share algorithmic information; they have a great influence on the society since they underlie almost every information technology artefact, and they are at the core of the current explosion of software technology. The history of programming languages is marked by innovations, diversifications, lateral transfers and social influences; moreover, it represents an intermediate case study between the evolution of human languages and the evolution of technology. In this paper we study the application of the Darwinian explanation to the programming languages evolution by discussing to what extent the evolutionary mechanisms distinctive of biology can be applied to this area. We show that a number of evolutionary building blocks can be recognised in the realm of computer languages, but we also identify critical issues. Far from being crystal clear, this fine-grained study shows to be a useful tool to assess recent results about programming languages phylogenies. Finally, we show that rich evolutionary patterns, such as co-evolution, macro-evolutionary trends, niche construction and exaptation, can be effectively applied to programming languages and provide for interesting explanatory tools.
△ Less
Submitted 15 October, 2015;
originally announced October 2015.
-
Proceedings of the Combined 22th International Workshop on Expressiveness in Concurrency and 12th Workshop on Structural Operational Semantics
Authors:
Silvia Crafa,
Daniel E. Gebler
Abstract:
This volume contains the proceedings of the Combined 22nd International Workshop on Expressiveness in Concurrency and the 12th Workshop on Structural Operational Semantics (EXPRESS/SOS 2015) which was held on 31 August 2015 in Madrid, Spain, as an affiliated workshop of CONCUR 2015, the 26th International Conference on Concurrency Theory. The EXPRESS workshops aim at bringing together researchers…
▽ More
This volume contains the proceedings of the Combined 22nd International Workshop on Expressiveness in Concurrency and the 12th Workshop on Structural Operational Semantics (EXPRESS/SOS 2015) which was held on 31 August 2015 in Madrid, Spain, as an affiliated workshop of CONCUR 2015, the 26th International Conference on Concurrency Theory. The EXPRESS workshops aim at bringing together researchers interested in the expressiveness of various formal systems and semantic notions, particularly in the field of concurrency. Their focus has traditionally been on the comparison between programming concepts (such as concurrent, functional, imperative, logic and object-oriented programming) and between mathematical models of computation (such as process algebras, Petri nets, event structures, modal logics, and rewrite systems) on the basis of their relative expressive power. The EXPRESS workshop series has run successfully since 1994 and over the years this focus has become broadly construed. The SOS workshops aim at being a forum for researchers, students and practitioners interested in new developments, and directions for future investigation, in the field of structural operational semantics. One of the specific goals of the SOS workshop series is to establish synergies between the concurrency and programming language communities working on the theory and practice of SOS. Since 2012, the EXPRESS and SOS communities have organized an annual combined EXPRESS/SOS workshop on the expressiveness of mathematical models of computation and the formal semantics of systems and programming concepts.
△ Less
Submitted 25 August, 2015;
originally announced August 2015.
-
The role of concurrency in an evolutionary view of programming abstractions
Authors:
Silvia Crafa
Abstract:
In this paper we examine how concurrency has been embodied in mainstream programming languages. In particular, we rely on the evolutionary talking borrowed from biology to discuss major historical landmarks and crucial concepts that shaped the development of programming languages. We examine the general development process, occasionally deepening into some language, trying to uncover evolutionary…
▽ More
In this paper we examine how concurrency has been embodied in mainstream programming languages. In particular, we rely on the evolutionary talking borrowed from biology to discuss major historical landmarks and crucial concepts that shaped the development of programming languages. We examine the general development process, occasionally deepening into some language, trying to uncover evolutionary lineages related to specific programming traits. We mainly focus on concurrency, discussing the different abstraction levels involved in present-day concurrent programming and emphasizing the fact that they correspond to different levels of explanation. We then comment on the role of theoretical research on the quest for suitable programming abstractions, recalling the importance of changing the working framework and the way of looking every so often. This paper is not meant to be a survey of modern mainstream programming languages: it would be very incomplete in that sense. It aims instead at pointing out a number of remarks and connect them under an evolutionary perspective, in order to grasp a unifying, but not simplistic, view of the programming languages development process.
△ Less
Submitted 28 July, 2015;
originally announced July 2015.
-
Actors vs Shared Memory: two models at work on Big Data application frameworks
Authors:
Silvia Crafa,
Luca Tronchin
Abstract:
This work aims at analyzing how two different concurrency models, namely the shared memory model and the actor model, can influence the development of applications that manage huge masses of data, distinctive of Big Data applications. The paper compares the two models by analyzing a couple of concrete projects based on the MapReduce and Bulk Synchronous Parallel algorithmic schemes. Both projects…
▽ More
This work aims at analyzing how two different concurrency models, namely the shared memory model and the actor model, can influence the development of applications that manage huge masses of data, distinctive of Big Data applications. The paper compares the two models by analyzing a couple of concrete projects based on the MapReduce and Bulk Synchronous Parallel algorithmic schemes. Both projects are doubly implemented on two concrete platforms: Akka Cluster and Managed X10. The result is both a conceptual comparison of models in the Big Data Analytics scenario, and an experimental analysis based on concrete executions on a cluster platform.
△ Less
Submitted 12 May, 2015;
originally announced May 2015.
-
Proceedings Combined 21st International Workshop on Expressiveness in Concurrency and 11th Workshop on Structural Operational Semantics
Authors:
Johannes Borgström,
Silvia Crafa
Abstract:
This volume contains the proceedings of the Combined 21st International Workshop on Expressiveness in Concurrency and the 11th Workshop on Structural Operational Semantics (EXPRESS/SOS 2014) which was held on 1st September 2014 in Rome, Italy, as an affiliated workshop of CONCUR 2014, the 25th International Conference on Concurrency Theory.
The EXPRESS workshops aim at bringing together resear…
▽ More
This volume contains the proceedings of the Combined 21st International Workshop on Expressiveness in Concurrency and the 11th Workshop on Structural Operational Semantics (EXPRESS/SOS 2014) which was held on 1st September 2014 in Rome, Italy, as an affiliated workshop of CONCUR 2014, the 25th International Conference on Concurrency Theory.
The EXPRESS workshops aim at bringing together researchers interested in the expressiveness of various formal systems and semantic notions, particularly in the field of concurrency. Their focus has traditionally been on the comparison between programming concepts (such as concurrent, functional, imperative, logic and object-oriented programming) and between mathematical models of computation (such as process algebras, Petri nets, event structures, modal logics, and rewrite systems) on the basis of their relative expressive power. The EXPRESS workshop series has run successfully since 1994 and over the years this focus has become broadly construed.
The SOS workshops aim at being a forum for researchers, students and practitioners interested in new developments, and directions for future investigation, in the field of structural operational semantics. One of the specific goals of the SOS workshop series is to establish synergies between the concurrency and programming language communities working on the theory and practice of SOS. Reports on applications of SOS to other fields are also most welcome, including: modelling and analysis of biological systems, security of computer systems programming, modelling and analysis of embedded systems, specification of middle-ware and coordination languages, programming language semantics and implementation, static analysis software and hardware verification, and semantics for domain-specific languages and model-based engineering.
△ Less
Submitted 6 August, 2014;
originally announced August 2014.
-
Semantics of (Resilient) X10
Authors:
Silvia Crafa,
David Cunningham,
Vijay Saraswat,
Avraham Shinnar,
Olivier Tardieu
Abstract:
We present a formal small-step structural operational semantics for a large fragment of X10, unifying past work. The fragment covers multiple places, mutable objects on the heap, sequencing, \code{try/catch}, \code{async}, \code{finish}, and \code{at} constructs. This model accurately captures the behavior of a large class of concurrent, multi-place X10 programs. Further, we introduce a formal mod…
▽ More
We present a formal small-step structural operational semantics for a large fragment of X10, unifying past work. The fragment covers multiple places, mutable objects on the heap, sequencing, \code{try/catch}, \code{async}, \code{finish}, and \code{at} constructs. This model accurately captures the behavior of a large class of concurrent, multi-place X10 programs. Further, we introduce a formal model of resilience in X10. During execution of an X10 program, a place may fail for many reasons. Resilient X10 permits the program to continue executing, losing the data at the failed place, and most of the control state, and repairing the global control state in such a way that key semantic principles hold, the Invariant Happens Before Principle, and the Failure Masking Principle. These principles permit an X10 programmer to write clean code that continues to work in the presence of place failure. The given semantics have additionally been mechanized in Coq.
△ Less
Submitted 13 December, 2013;
originally announced December 2013.
-
Causality in concurrent systems
Authors:
Silvia Crafa,
Federica Russo
Abstract:
Concurrent systems identify systems, either software, hardware or even biological systems, that are characterized by sets of independent actions that can be executed in any order or simultaneously. Computer scientists resort to a causal terminology to describe and analyse the relations between the actions in these systems. However, a thorough discussion about the meaning of causality in such a con…
▽ More
Concurrent systems identify systems, either software, hardware or even biological systems, that are characterized by sets of independent actions that can be executed in any order or simultaneously. Computer scientists resort to a causal terminology to describe and analyse the relations between the actions in these systems. However, a thorough discussion about the meaning of causality in such a context has not been developed yet. This paper aims to fill the gap. First, the paper analyses the notion of causation in concurrent systems and attempts to build bridges with the existing philosophical literature, highlighting similarities and divergences between them. Second, the paper analyses the use of counterfactual reasoning in ex-post analysis in concurrent systems (i.e. execution trace analysis).
△ Less
Submitted 6 March, 2013;
originally announced March 2013.
-
Behavioural Types for Actor Systems
Authors:
Silvia Crafa
Abstract:
Recent mainstream programming languages such as Erlang or Scala have renewed the interest on the Actor model of concurrency. However, the literature on the static analysis of actor systems is still lacking of mature formal methods. In this paper we present a minimal actor calculus that takes as primitive the basic constructs of Scala's Actors API. More precisely, actors can send asynchronous messa…
▽ More
Recent mainstream programming languages such as Erlang or Scala have renewed the interest on the Actor model of concurrency. However, the literature on the static analysis of actor systems is still lacking of mature formal methods. In this paper we present a minimal actor calculus that takes as primitive the basic constructs of Scala's Actors API. More precisely, actors can send asynchronous messages, process received messages according to a pattern matching mechanism, and dynamically create new actors, whose scope can be extruded by passing actor names as message parameters. Drawing inspiration from the linear types and session type theories developed for process calculi, we put forward a behavioural type system that addresses the key issues of an actor calculus. We then study a safety property dealing with the determinism of finite actor com- munication. More precisely, we show that well typed and balanced actor systems are (i) deadlock-free and (ii) any message will eventually be handled by the target actor, and dually no actor will indefinitely wait for an expected message
△ Less
Submitted 8 June, 2012;
originally announced June 2012.
-
A Logic for True Concurrency
Authors:
Paolo Baldan,
Silvia Crafa
Abstract:
We propose a logic for true concurrency whose formulae predicate about events in computations and their causal dependencies. The induced logical equivalence is hereditary history preserving bisimilarity, and fragments of the logic can be identified which correspond to other true concurrent behavioural equivalences in the literature: step, pomset and history preserving bisimilarity. Standard Hennes…
▽ More
We propose a logic for true concurrency whose formulae predicate about events in computations and their causal dependencies. The induced logical equivalence is hereditary history preserving bisimilarity, and fragments of the logic can be identified which correspond to other true concurrent behavioural equivalences in the literature: step, pomset and history preserving bisimilarity. Standard Hennessy-Milner logic, and thus (interleaving) bisimilarity, is also recovered as a fragment. We also propose an extension of the logic with fixpoint operators, thus allowing to describe causal and concurrency properties of infinite computations. We believe that this work contributes to a rational presentation of the true concurrent spectrum and to a deeper understanding of the relations between the involved behavioural equivalences.
△ Less
Submitted 17 January, 2014; v1 submitted 18 October, 2011;
originally announced October 2011.
