Development of Domain-Specific Languages for smart contracts
Security analysis of smart contracts and blockchain-based applications
Blockchain-based monetary fraud analysis and detection
Custom data analysis on blockchain (de-anonymisation, attack patterns, ...)
Design and development of blockchain-based applications (on Bitcoin, Ethereum, ...)
Business consultancy on blockchain technologies and cyber-security
We present a toolchain for developing and verifying smart contracts that can be executed on Bitcoin. The toolchain is based on BitML, a recent domain-specific language for smart contracts with a computationally sound embedding into Bitcoin. Our toolchain automatically verifies relevant properties of contracts, among which liquidity, ensuring that funds do not remain frozen within a contract forever. A compiler is provided to translate BitML contracts into sets of standard Bitcoin transactions: executing a contract corresponds to appending these transactions to the blockchain. We assess our toolchain through a benchmark of representative contracts.
One of the key features of modern blockchain platforms is the possibility of executing smart contracts, i.e. computer programs that transfer digital assets between users, according to pre-agreed rules. Crucially, the execution of smart contracts must be correct even in the presence of (a minority of) adversaries in the peer-to-peer network that maintains the blockchain. To enforce this property without a trusted authority, the nodes follow a consensus protocol, which determines which node can extend the blockchain at each moment. To this aim, nodes first collect a set of transactions from the network, representing the actions on the smart contracts required by users. Then, to compute the new state of the smart contracts, they put these transactions in sequence (in an arbitrary order), and execute them serially. Once this block of transactions is appended to the blockchain, the other nodes of the network validate it, by re-executing the transactions in the same order. The serial execution of transactions does not take advantage of the multi-core architecture of modern processors, so contributing to limit the throughput of blockchains. In this paper we devise a static analysis technique for parallelizing the execution of transactions, in a formal setting based on Ethereum, the most widespread platform for smart contracts.
Journal of Grid Computing, 2019
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 whether 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.
Financial Cryptography and Data Security, 2018.
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.
Principles of Security and Trust, 2017
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.
Crypto Valley Conference on Blockchain Technology, 2018
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.