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 propose a secure and efficient implementation of fungible tokens on Bitcoin. Our technique is based on a small extension of the Bitcoin script language, which allows the spending conditions in a transaction to depend on the neighbour transactions. We show that our implementation is computationally sound: that is, adversaries can make tokens diverge from their ideal functionality only with negligible probability.
We develop a formal model of Algorand stateless smart contracts (stateless ASC1.) We exploit our model to prove fundamental properties of the Algorand blockchain, and to establish the security of some archetypal smart contracts. While doing this, we highlight various design patterns supported by Algorand. We perform experiments to validate the coherence of our formal model w.r.t. the actual implementation.
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.
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.