Upcoming paper: BitML: a calculus for Bitcoin smart contracts

posted Jul 23, 2018, 9:58 PM by Massimo Bartoletti

Upcoming paper (to be presented at ACM CCS 2018)

Massimo Bartoletti and Roberto Zunino

Abstract. We introduce BitML, a domain-specific language for specifying contracts that regulate transfers of bitcoins among participants, without relying on trusted intermediaries. We define a symbolic and a computational model for reasoning about BitML security. In the symbolic model, participants act according to the semantics of BitML, while in the computational model they exchange bitstrings, and read/append transactions on the Bitcoin blockchain. A compiler is provided to translate contracts into standard Bitcoin transactions. Participants can execute a contract by appending these transactions on the Bitcoin blockchain, according to their strategies. We prove the correctness of our compiler, showing that computational attacks to compiled contracts are also observable in the symbolic model.

Upcoming paper: Progress-preserving Refinements of CTA

posted Jun 8, 2018, 1:44 AM by Massimo Bartoletti   [ updated Jul 23, 2018, 10:01 PM ]

Upcoming paper (to be presented at CONCUR 2018)

Massimo Bartoletti, Laura Bocchi, Maurizio Murgia

Abstract. We develop a theory of refinement for timed asynchronous systems, in the setting of Communicating Timed Automata (CTA). Our refinement applies point-wise to the components of a system of CTA, and only affecting their time constraints — in this way, we achieve compositionality and decidability. We then establish a decidable condition under which our refinement preserves behavioural properties of systems, such as their global and local progress. Our theory provides guidelines on how to implement timed protocols using the real-time primitives of programming languages. We validate our theory throughseries of experiments, supported by an open-source tool which implements our verification techniques.

Seminar: Transcompiling and Analysing Firewalls

posted Jun 6, 2018, 2:04 AM by Massimo Bartoletti   [ updated Jun 6, 2018, 2:05 AM ]

Upcoming Seminar

Transcompiling and Analysing Firewalls

June 11, 17.00 (Aula F)
Palazzo delle Scienze - Cagliari

Letterio Galletta

IMT Lucca (IT)

Abstract. Configuring and maintaining a firewall configuration is notoriously hard. On the one hand, network administrators have to know in detail the policy meaning, as well as the internals of the firewall systems and of their languages. On the other hand, policies are written in low-level, platform-specific languages where firewall rules are inspected and enforced along non trivial control flow paths. Further difficulties arise from Network Address Translation (NAT), an indispensable mechanism in IPv4 networking for performing port redirection and translation of addresses.

Upcoming paper: Data mining for detecting Bitcoin Ponzi schemes

posted Jun 6, 2018, 2:02 AM by Massimo Bartoletti

Upcoming paper (to be presented at the Crypto Valley Conference 2018)

Massimo Bartoletti, Barbara Pes, Sergio Serusi

Abstract. Soon after its introduction in 2009, Bitcoin has been adopted by cyber-criminals, which rely on its pseudonymity to implement virtually untraceable scams. One of the typical scams that operate on Bitcoin are the so-called Ponzi schemes. These are fraudulent investments which repay users with the funds invested by new users that join the scheme, and implode when it is no longer possible to find new investments. Despite being illegal in many countries, Ponzi schemes are now proliferating on Bitcoin, and they keep alluring new victims, who are plundered of millions of dollars.

We apply data mining techniques to detect Bitcoin addresses related to Ponzi schemes. Our starting point is a dataset of features of real-world Ponzi schemes, that we construct by analysing, on the Bitcoin blockchain, the transactions used to perform the scams. We use this dataset to experiment with various machine learning algorithms, and we assess their effectiveness through standard validation protocols and performance metrics. The best of the classifiers we have experimented can identify most of the Ponzi schemes in the dataset, with a low number of false positives.

1st Scientific School on Blockchain and Distributed Ledger Technologies

posted Mar 15, 2018, 6:45 AM by Massimo Bartoletti   [ updated Apr 16, 2018, 6:40 AM ]

1st Scientific School on Blockchain and Distributed Ledger Technologies
Pula, Sardinia, Italy
12-15 June 2018

Crypto economics is a new discipline born after the rise of virtual currencies and distributed ledger technologies, and is rapidly developing in a unique intersection between computing, cryptography, law, economics, and game theory. The school aims at disseminating knowledge about the foundations and the applications of these technologies to researchers, PhD students, scholars and technologists in industry and academia, not excluding under- or new graduates with strong technical drive and a sufficient background.


The school will be hosted at the Technology Park of Sardinia in Pula (Sardinia, Italy).
Travel and accommodation information are available on the school website.


The registration and attendance is FREE of charge. However, as we may not be able to accommodate all the applicants, the attendees will be selected by the scientific committee on a CV best-match basis. This implies that candidates showing the attitude to receive the most value from the lectures will be given higher priority. The school plans for a maximum of 38 attendees with a quota of 12 seats reserved to scholars coming from CRS4, University of Cagliari and from SMEs located in Sardinia. Should this quota remain unfilled, the remainder seats will be redistributed to waitlisted participants.


Prospective participants should apply through the school web page by April 30, 2018
Notification of accepted applicants will be posted by May 15, 2018
School dates June 12-15, 2018

  • Silvio Micali (MIT). Algorand: a truly distributed ledger
  • Paolo Tasca (UCL). TBA
  • Rainer Böhme (Univ. Innsbruck). Incentives Matter: On the Economics and Governance of Blockchain-based Systems
  • Stefano Bistarelli (Univ. Perugia). From mining to multisigned transactions: discovering how Bitcoin works
  • Massimo Simbula. Bitcoin revolution a legal perspective
  • Michele Nati (Digital Catapult). Reputation and personal data in the blockchain age
  • Federico Tenga (Chainside). Bitcoin Scalability, payment channels and lightning networks
  • Michele Marchesi (Univ. Cagliari). Software engineering methodologies for blockchain development
  • Davide Carboni (CRS4). Introduction to Ethereum and smart contracts
  • Mauro Pili (Paymeabit). Web3: a platform for decentralized apps
  • Massimo Bartoletti, Livio Pompianu,Alessandro Sebastian Podda, Nicola Atzei (Univ. Cagliari). Hands on lab on Bitcoin
  • Mauro Pili, Andrea Pinna, Marco Ortu, Simona Ibba (Univ. Cagliari). Hands on lab on Ethereum

  • Massimo Bartoletti, University of Cagliari
  • Davide Carboni, CRS4 Pula (chair)
  • Salvatore Carta, University of Cagliari
  • Rocco De Nicola, IMT Lucca
  • William Knottenbelt, Imperial College of London
  • Michele Marchesi, University of Cagliari
  • Francesco Piras, Associazione Bitcoin Sardegna

Upcoming paper: SoK: unraveling Bitcoin smart contracts

posted Mar 1, 2018, 2:34 PM by Massimo Bartoletti

Upcoming paper (to be presented at POST 2018)

Nicola Atzei, Massimo Bartoletti, Tiziana Cimoli, Stefano Lande, Roberto Zunino

Abstract. Albeit the primary usage of Bitcoin is to exchange currency, its blockchain and consensus mechanism can also be exploited to securely execute some forms of smart contracts. These are agreements among mutually distrusting parties, which can be automatically enforced without resorting to a trusted intermediary. Over the last few years a variety of smart contracts for Bitcoin have been proposed, both by the academic community and by that of developers. However, the heterogeneity in their treatment, the informal (often incomplete or imprecise) descriptions, and the use of poorly documented Bitcoin features, pose obstacles to the research.

In this paper we present a comprehensive survey of smart contracts on Bitcoin, in a uniform framework. Our treatment is based on a new formal specification language for smart contracts, which also helps us to highlight some subtleties in existing informal descriptions, making a step towards automatic verification. We discuss some obstacles to the diffusion of smart contracts on Bitcoin, and we identify the most promising open research challenges.

Upcoming paper: A formal model of Bitcoin transactions

posted Dec 5, 2017, 7:03 AM by Massimo Bartoletti   [ updated Mar 1, 2018, 2:35 PM ]

Upcoming paper (to be presented at Financial Cryptography 2018)

Nicola Atzei, Massimo Bartoletti, Stefano Lande, Roberto Zunino

We propose a formal model of Bitcoin transactions, which is sufficiently abstract to enable formal reasoning, and at the same time is concrete enough to serve as an alternative documentation to Bitcoin. We use our model to formally prove some well-formedness properties of the Bitcoin blockchain, for instance that each transaction can only be spent once. We release an open-source tool through which programmers can write transactions in our abstract model, and compile them into standard Bitcoin transactions.

Upcoming paper: A general framework for blockchain analytics

posted Oct 23, 2017, 9:13 AM by Massimo Bartoletti

Upcoming paper (to be presented at SERIAL 2017)
Massimo Bartoletti, Andrea Bracciali, Stefano Lande, Livio Pompianu

Abstract. Modern cryptocurrencies exploit decentralised blockchains to record a public and unalterable history of transactions. Besides transactions, further information is stored for different, and often undisclosed, purposes, making the blockchains a rich and increasingly growing source of valuable information, in part of difficult interpretation. Many data analytics studies have been carried out, mostly based on specifically designed and ad-hoc engineered approaches. We propose a general-purpose framework, seamlessly supporting data analytics on both Bitcoin and Ethereum — currently the two most prominent cryptocurrencies. Such a framework allows us to integrate relevant blockchain data with data from other sources, and to organise them in a database, either SQL or NoSQL. Our framework is released as an open-source Scala library, a mainstream Java-like programming language. We illustrate the distinguishing features of our approach on a set of significant use cases, which allow us to empirically compare ours to other competing proposals, and evaluate the impact of the database choice on scalability.

Upcoming paper: Timed Session Types

posted Oct 23, 2017, 9:09 AM by Massimo Bartoletti

Upcoming paper (to appear in LMCS)
Massimo Bartoletti, Tiziana Cimoli, Maurizio Murgia

Timed session types formalise timed communication protocols between two participants at the endpoints of a session. They feature a decidable compliance relation, which generalises to the timed setting the progress-based compliance between untimed session types. We show a sound and complete technique to decide when a timed session type admits a compliant one. Then, we show how to construct the most precise session type compliant with a given one, according to the subtyping preorder induced by compliance. Decidability of subtyping follows from these results.

Seminar: On the Security of the Blockchain Bix Protocol and Certificates

posted Oct 6, 2017, 8:25 AM by Sebastian P.   [ updated Oct 6, 2017, 8:26 AM ]

Upcoming Seminar

 On the Security of the Blockchain Bix Protocol and Certificates

October 5, 15.00 (Aula F)
Palazzo delle Scienze - Cagliari

Riccardo Longo

University of Trento (IT)

Abstract: The BIX protocol is a blockchain-based protocol that allows distribution of certificates linking a subject with his public key, hence providing a service similar to that of a PKI but without the need of a CA. In this seminar I will present an analysis of the security of the BIX protocol in a formal way. First, I will identify formal security assumptions which are well-suited to this protocol. Second, I will present some attack scenarios against the BIX protocol. Finally, I will provide a formal security proof that these attacks are not feasible under our previously established assumptions.

1-10 of 95