News
Upcoming paper: Verifying liquidity of Bitcoin contracts
Upcoming paper (to be presented at Principles of Security and Trust, 2019) Massimo Bartoletti and Roberto Zunino Abstract. A landmark security property of smart contracts is
liquidity: in a non-liquid contract, it may happen that some
funds remain frozen. The relevance of this issue is witnessed
by a recent liquidity attack to the Ethereum Parity Wallet,
which has frozen 160M USD within the contract, making this sum
unredeemable by any user. We address the problem of verifying
liquidity of Bitcoin contracts. Focussing on BitML, a contracts
DSL with a computationally sound compiler to Bitcoin, we
study various notions of liquidity. Our main result is that
liquidity of BitML contracts is decidable, in all the proposed
variants. To prove this, we first transform the infinite-state
semantics of BitML into a finite-state one, which focusses on
the behaviour of any given set of contracts, abstracting the
moves of the context. With respect to the chosen contracts,
this abstraction in sound and complete. Our decision procedure
for liquidity is then based on model-checking the finite space
of states of the abstraction. The computational soundness of
the BitML compiler allows to lift this result from the
symbolic to the computational level: if our decision procedure
establishes that a contract is liquid, then it will be such
also under a computational adversary, and vice versa.
|
Upcoming paper: A journey into Bitcoin metadata
Upcoming paper (to appear on Journal of Grid Computing) Massimo Bartoletti, Bryn Bellomy, Livio Pompianu Abstract. Besides recording transfers of currency, the Bitcoin blockchain is being used to save metadata — i.e. arbitrary pieces of data which do not affect transfers of bitcoins. This can be done by using different techniques, and for different purposes. For instance, a growing number of protocols embed metadata in the blockchain to certify and transfer the ownership of a variety of assets beyond cryptocurrency. A point of debate in the Bitcoin community is hether metadata negatively impact on the effectiveness of Bitcoin with respect to its primary function. This paper is a systematic analysis of the usage of Bitcoin metadata over the years. We discuss all the known techniques to embed metadata in the Bitcoin blockchain; we then extract metadata, and analyse them from different angles. |
Upcoming paper: Blockchain for social good: a quantitative analysis
Upcoming paper (to be presented at GOODTECHS 2018) Blockchain for social good: a quantitative analysis Massimo Bartoletti, Tiziana Cimoli, Livio Pompianu and Sergio Serusi Abstract. The advent of blockchain technologies has given a boost to social good projects, which are trying to exploit various characteristic features of blockchains: the quick and inexpensive transfer of cryptocurrency, the transparency of transactions, the ability to tokenize any kind of assets, and the increase in trustworthiness due to decentralization. However, the swift pace of innovation in blockchain technologies, and the hype that has surrounded their “disruptive potential”, make it difficult to understand whether these technologies are applied correctly, and what one should expect when trying to apply them to social good projects. This paper addresses these issues, by systematically analysing a collection of 95 blockchain-enabled social good projects. Focussing on measurable and objective aspects, we try to answer various relevant questions: which features of blockchains are most commonly used? Do projects have success in fund raising? Are they making appropriate choices on the blockchain architecture? How many projects are released to the public, and how many are eventually abandoned? |
Upcoming paper: BitML: a calculus for Bitcoin smart contracts
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
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
Upcoming Seminar Transcompiling and Analysing Firewalls June 11, 17.00 (Aula F) 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
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
1st Scientific School on Blockchain and Distributed Ledger Technologies
Pula, Sardinia, Italy 12-15 June 2018 http://blockchain2018.crs4.it 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. SCHOOL VENUE 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. SCHOOL FEES 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. SCHOOL DATES 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 PROGRAM
SCIENTIFIC COMMITTEE
|
Upcoming paper: SoK: unraveling Bitcoin smart contracts
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
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. |
1-10 of 98