News


Upcoming paper: A formal model of Bitcoin transactions

posted Dec 5, 2017, 7:03 AM by Massimo Bartoletti

Upcoming paper (to be presented at Financial Cryptography 2018)

Nicola Atzei, Massimo Bartoletti, Stefano Lande, Roberto Zunino

Abstract.
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

Abstract.
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.

Seminars series: cryptocurrencies and smart contracts 2017

posted Apr 18, 2017, 3:16 AM by Massimo Bartoletti

The preliminary programme of this series of seminars is available here.

Seminar: Behavioural type-checking of time-sensitive protocols

posted Apr 18, 2017, 2:57 AM by Massimo Bartoletti   [ updated Apr 18, 2017, 3:31 AM ]

Upcoming Seminar

Behavioural type-checking of time-sensitive protocols

April 21, 15.00 (Aula F)
Palazzo delle Scienze - Cagliari


Laura Bocchi

University of Kent (UK)

Abstract. In recent work we have extended multiparty session types (MPST) with a model of time borrowed from Communicating Time Automata (CTA). This allowed us to establish a sound and complete correspondence between timed MPST and a subclass of CTA that satisfies progress. On the basis of this correspondence, we can decide properties on CTA that are undecidable in the general case, such as safety (absence of orphan messages and communication mismatches), progress, non-zenoness and eventual reception of messages sent. I will present decidable conditions for these properties, and   give a concrete procedure to build *when possible* global timed MPST from (arbitrary) collections of timed automata, with the guarantee that the resulting global specification is a well-behaved composition.

Resources

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

posted Mar 24, 2017, 1:49 PM by Massimo Bartoletti

Upcoming paper (to be presented at WTSC 2017)
Massimo Bartoletti and Livio Pompianu

Abstract. 
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.

Upcoming paper: An analysis of Bitcoin OP_RETURN metadata

posted Mar 24, 2017, 1:44 PM by Massimo Bartoletti

Upcoming paper (to be presented at BITCOIN 2017)
Massimo Bartoletti and Livio Pompianu

Abstract.
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.

Upcoming paper: Constant-deposit multiparty lotteries on Bitcoin

posted Mar 24, 2017, 1:42 PM by Massimo Bartoletti   [ updated Mar 24, 2017, 1:45 PM ]

Upcoming paper (to be presented at BITCOIN 2017)
Massimo Bartoletti and Roberto Zunino

Abstract. An active research trend is to exploit the consensus mechanism of cryptocurrencies to secure the execution of distributed applications. In particular, some recent works have proposed fair lotteries which work on Bitcoin. These protocols, however, require a deposit from each player which grows quadratically with the number of players. We propose a fair lottery on Bitcoin which only requires a constant deposit.

Upcoming paper: A survey of attacks on Ethereum smart contracts

posted Mar 24, 2017, 1:38 PM by Massimo Bartoletti

Upcoming paper (to be presented at POST 2017)
Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli

Abstract. Smart contracts are computer programs that can be correctly executed by a network of mutually distrusting nodes, without the need of an external trusted authority. Since smart contracts handle and transfer assets of considerable value, besides their correct execution it is also crucial that their implementation is secure against attacks which aim at stealing or tampering the assets. We study this problem in Ethereum, the most well-known and used framework for smart contracts so far. We analyse the security vulnerabilities of Ethereum smart contracts, providing a taxonomy of common programming pitfalls which may lead to vulnerabilities. We show a series of attacks which exploit these vulnerabilities, allowing an adversary to steal money or cause other damage.

The detailed code of attacks is available here.

1-10 of 89