arXiv subjects

Massimo Bartoletti

Publications and source records attributed to Massimo Bartoletti.

53 records · Page 3Linked to original sources

arXiv2018

Data mining for detecting Bitcoin Ponzi schemes

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.

cs.CR↗

arXiv2017

Timed Session Types

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.

cs.LO↗

arXiv2017

Proceedings 10th Interaction and Concurrency Experience

This volume contains the proceedings of ICE 2017, the 10th Interaction and Concurrency Experience, which was held in Neuchâtel, Switzerland on the 21st and 22nd of June 2017 as a satellite event of DisCoTec'17. The ICE procedure for paper selection allows PC members to interact, anonymously, with authors. During the review phase, each submitted paper is published on a discussion forum whose access is restricted to the authors and to all the PC members not declaring a conflict of interest. The PC members post comments and questions that the authors reply to. For the first time, the 2017 edition of ICE included a double blind reviewing of original research papers, in order to increase fairness and avoid bias in reviewing. The gender balance of accepted papers was also more even than in past years. Each paper was reviewed by three PC members, and altogether five papers were accepted for publication (the workshop also featured five brief announcements which are not part of this volume). We were proud to host three invited talks, by Christian Cachin, Marieke Huismann, and Paweł Sobocinski. The abstracts of these talks are included in this volume together with the regular papers.

cs.LO↗

arXiv2017

A general framework for blockchain analytics

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 have been developed, 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. 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.

cs.CR↗

arXiv2017

An empirical analysis of smart contracts: platforms, applications, and design patterns

Smart contracts are computer programs that can be consistently executed by a network of mutually distrusting nodes, without the arbitration of a trusted authority. Because of their resilience to tampering, smart contracts are appealing in many scenarios, especially in those which require transfers of money to respect certain agreed rules (like in financial services and in games). Over the last few years many platforms for smart contracts have been proposed, and some of them have been actually implemented and used. We study how the notion of smart contract is interpreted in some of these platforms. Focussing on the two most widespread ones, Bitcoin and Ethereum, we quantify the usage of smart contracts in relation to their application domain. We also analyse the most common programming patterns in Ethereum, where the source code of smart contracts is available.

cs.CR↗

arXiv2017

An analysis of Bitcoin OP_RETURN metadata

The Bitcoin protocol allows to save arbitrary data on the blockchain through a special instruction of the scripting language, called OP_RETURN. A growing number of protocols exploit this feature to extend the range of applications of the Bitcoin blockchain beyond transfer of currency. A point of debate in the Bitcoin community is whether loading data through OP_RETURN can negatively affect the performance of the Bitcoin network with respect to its primary goal. This paper is an empirical study of the usage of OP_RETURN over the years. We identify several protocols based on OP_RETURN, which we classify by their application domain. We measure the evolution in time of the usage of each protocol, the distribution of OP_RETURN transactions by application domain, and their space consumption.

cs.CR↗

arXiv2016

Honesty by Typing

We propose a type system for a calculus of contracting processes. Processes can establish sessions by stipulating contracts, and then can interact either by keeping the promises made, or not. Type safety guarantees that a typeable process is honest - that is, it abides by the contracts it has stipulated in all possible contexts, even in presence of dishonest adversaries. Type inference is decidable, and it allows to safely approximate the honesty of processes using either synchronous or asynchronous communication.

cs.PL↗

arXiv2016

Proceedings 9th Interaction and Concurrency Experience

This volume contains the proceedings of ICE 2016, the 9th Interaction and Concurrency Experience, which was held in Heraklion, Greece on the 8th and 9th of June 2016 as a satellite event of DisCoTec 2016. The ICE procedure for paper selection allows PC members to interact, anonymously, with authors. During the review phase, each submitted paper is published on a discussion forum whose access is restricted to the authors and to all the PC members not declaring a conflict of interest. The PC members post comments and questions that the authors reply to. For the first time, the 2016 edition of ICE included a feature targeting review transparency: reviews of accepted papers were made public on the workshop website and workshop participants in particular were able to access them during the workshop. Each paper was reviewed by three PC members, and altogether nine papers were accepted for publication (the workshop also featured three brief announcements which are not part of this volume). We were proud to host two invited talks, by Alexandra Silva and Uwe Nestmann. The abstracts of these two talks are included in this volume together with the regular papers.

cs.PL↗

arXiv2015

Combining behavioural types with security analysis

Today's software systems are highly distributed and interconnected, and they increasingly rely on communication to achieve their goals; due to their societal importance, security and trustworthiness are crucial aspects for the correctness of these systems. Behavioural types, which extend data types by describing also the structured behaviour of programs, are a widely studied approach to the enforcement of correctness properties in communicating systems. This paper offers a unified overview of proposals based on behavioural types which are aimed at the analysis of security properties.

cs.PL↗

arXiv2015

The LTS WorkBench

Labelled Transition Systems (LTSs) are a fundamental semantic model in many areas of informatics, especially concurrency theory. Yet, reasoning on LTSs and relations between their states can be difficult and elusive: very simple process algebra terms can give rise to a large (possibly infinite) number of intricate transitions and interactions. To ease this kind of study, we present LTSwb, a flexible and extensible LTS toolbox: this tutorial paper discusses its design and functionalities.

cs.LO↗

arXiv2014

A note on two notions of compliance

We establish a relation between two models of contracts: binary session types, and a model based on event structures and game-theoretic notions. In particular, we show that compliance in session types corresponds to the existence of certain winning strategies in game-based contracts.

cs.PL↗

arXiv2013

Contract agreements via logic

We relate two contract models: one based on event structures and game theory, and the other one based on logic. In particular, we show that the notions of agreement and winning strategies in the game-theoretic model are related to that of provability in the logical model.

cs.LO↗

arXiv2013

Lending Petri nets and contracts

Choreography-based approaches to service composition typically assume that, after a set of services has been found which correctly play the roles prescribed by the choreography, each service respects his role. Honest services are not protected against adversaries. We propose a model for contracts based on a extension of Petri nets, which allows services to protect themselves while still realizing the choreography. We relate this model with Propositional Contract Logic, by showing a translation of formulae into our Petri nets which preserves the logical notion of agreement, and allows for compositional verification.

cs.LO↗

arXiv2013

An event-based model for contracts

We introduce a basic model for contracts. Our model extends event structures with a new relation, which faithfully captures the circular dependencies among contract clauses. We establish whether an agreement exists which respects all the contracts at hand (i.e. all the dependencies can be resolved), and we detect the obligations of each participant. The main technical contribution is a correspondence between our model and a fragment of the contract logic PCL. More precisely, we show that the reachable events are exactly those which correspond to provable atoms in the logic. Despite of this strong correspondence, our model improves previous work on PCL by exhibiting a finer-grained notion of culpability, which takes into account the legitimate orderings of events.

cs.LO↗

arXiv2012

On the realizability of contracts in dishonest systems

We develop a theory of contracting systems, where behavioural contracts may be violated by dishonest participants after they have been agreed upon - unlike in traditional approaches based on behavioural types. We consider the contracts of \cite{CastagnaPadovaniGesbert09toplas}, and we embed them in a calculus that allows distributed participants to advertise contracts, reach agreements, query the fulfilment of contracts, and realise them (or choose not to). Our contract theory makes explicit who is culpable at each step of a computation. A participant is honest in a given context S when she is not culpable in each possible interaction with S. Our main result is a sufficient criterion for classifying a participant as honest in all possible contexts.

cs.PL↗

arXiv2011

Contracts in distributed systems

We present a parametric calculus for contract-based computing in distributed systems. By abstracting from the actual contract language, our calculus generalises both the contracts-as-processes and contracts-as-formulae paradigms. The calculus features primitives for advertising contracts, for reaching agreements, and for querying the fulfilment of contracts. Coordination among principals happens via multi-party sessions, which are created once agreements are reached. We present two instances of our calculus, by modelling contracts as (i) processes in a variant of CCS, and (ii) as formulae in a logic. With the help of a few examples, we discuss the primitives of our calculus, as well as some possible variants.

cs.PL↗

arXiv2010

Primitives for Contract-based Synchronization

We investigate how contracts can be used to regulate the interaction between processes. To do that, we study a variant of the concurrent constraints calculus presented in [1], featuring primitives for multi-party synchronization via contracts. We proceed in two directions. First, we exploit our primitives to model some contract-based interactions. Then, we discuss how several models for concurrency can be expressed through our primitives. In particular, we encode the pi-calculus and graph rewriting.

cs.PL↗