BitML is a domain-specific language for Bitcoin smart contracts. The BitML toolchain implements: (i) an IDE for developing BitML contracts, integrated in the DrRacket IDE; (ii) a compiler which translates BitML contracts into standard Bitcoin transaction. The compiler is computationally sound, meaning that computational attacks (i.e., at the level of Bitcoin transactions) can be detected at the symbolic level of the BitML semantics; (iii) a model checker which verifies security properties of BitML contracts, like their liquidity (i.e., funds never remain frozen in a contract), and custom LTL properties. The model checker is based on Maude.
BALZaC (Bitcoin Abstract Language, analyZer and Compiler) is an high-level language allows you to write transaction, verify their correctness, and compile them into actual Bitcoin transactions.
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. The Bitcoin dePonzifier is a classifier of Ponzi schemes based on supervised learning algorithms.
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.View Project
Modern cryptocurrencies exploit decentralised blockchains to record a public and unalterable history of transactions. Besides transactions, further metadata is stored for different, and often undisclosed, purposes. Metadata is mostly generated by protocols and smart contracts, i.e. programs whose correct execution is automatically enforced without relying on a trusted authority. This project investigates tools and techniques for analysing blockchains, their metadata, and smart contracts, focussing on Bitcoin and Ethereum...
We carry out a quantitative research on blockchain technologies for social good, based on the analysis of more than one hundred 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?