Talks@LASIGE

Bitcoin contracts: secure compilation, analysis, and expressiveness

Transmissão através de Videoconferência

Speaker: Massimo Bartoletti (University of Cagliari).

Abstract: Although Bitcoin is mainly used to exchange crypto-currency, its blockchain and consensus mechanism can also be exploited to execute smart contracts, allowing mutually untrusted parties to exchange crypto-assets according to pre-agreed rules. To this purpose, Bitcoin features a non Turing-complete script language, which is used to specify the redeem conditions of transactions. This is a simple language of expressions, without loops or recursion. To write complex smart contracts, one needs to suitably combine transactions: in this approach, executing a contract amounts to appending sequences of transactions in a given order.

A drawback of this approach is that the complexity of writing smart contracts grows quickly in the number of transactions needed to implement it. Reasoning about the correctness of these contracts is even harder: one would have to consider computational adversaries who interact with the blockchain, only being constrained to use PPTIME algorithms. To overcome these issues we have proposed BitML, a high-level DSL for smart contracts with a computationally sound compiler to Bitcoin transactions.

The computational soundness property allows us to reason about contracts at the symbolic level of the BitML semantics. We exploit this possibility to investigate a landmark property of contracts, called liquidity, which ensures that funds never remain frozen within a contract. Liquidity is a relevant issue, as witnessed by a recent attack to the Ethereum Parity Wallet, which has frozen ∼160M USD within the contract, making this sum unredeemable by any user. We develop a static analysis for liquidity of BitML contracts. This is achieved by first devising a finite-state, safe abstraction of infinite-state semantics of BitML, and then model-checking this abstraction.

We conclude by discussing a few open issues: in particular, how to enhance the expressiveness of Bitcoin contracts via minor extensions of the Bitcoin script language, and how to reduce the cost of executing contracts.

Bio: Massimo Bartoletti is Associate Professor at the Department of Mathematics and Computer Science of the University of Cagliari. His research activity concerns the development of tools and techniques for the specification, analysis and verification of software, with a special emphasis on security. Massimo Bartoletti is founder of the laboratory "Blockchain @ Unica" (http://blockchain.unica.it), one of the first academic research groups on blockchain technologies in Italy, director of the node of the Cyber Security National Lab for the University of Cagliari, and core member of the CINI working group on Blockchain. The laboratory is currently investigating several aspects of blockchain technologies, among which Domain-Specific Languages for developing provably secure smart contracts. His research spans over various blockchain platforms, including Bitcoin, Ethereum, Hyperledger Fabric and Algorand. He is principal investigator of several R&D projects on blockchain technologies, editor in chief of the “Smart contracts” section of Frontiers in Blockchains, and member of the scientific board of several workshops on blockchain technologies. Massimo Bartoletti has published over 20 scientific papers on blockchain technologies since 2016.


Zoom

15h00
LASIGE
Logótipo do evento

No dia 04 de abril, pelas 14h30, será gravado um episódio em direto do podcast "A Escala do Clima" de Filipe Duarte Santos (Professor Jubilado de CIÊNCIAS).

Fotografia de coleção de insetos

The course includes several case studies of insect adaptation, and the most recent overview on insect evodevo, plasticity, ecophysiological responses and conservation under global change.

Fotografia de aluna

Uma iniciativa aberta a toda a comunidade académica da ULisboa.

A iniciativa, promovida pela Rede Campus Sustentável (da qual CIÊNCIAS faz parte), é direcionada para o incentivo à colaboração entre as pessoas que pertencem a estruturas existentes ou em fase de constituição.

Título/data/local do evento e fotografia aérea de vias urbanas

Conferência da redeMOV, por Gabriel Costa Valença.

Logótipo CIE

A leading venue for presenting and discussing the latest research, industrial practice and innovations in dependable and secure computing.

Seminário do Centro de Física Teórica e Computacional, por João Neves (CFTC).

Edição anterior da Jobshop Ciências

O maior evento de empregabilidade de CIÊNCIAS, a decorrer nos dias 08 e 09 de abril.

RSS Meetup, por Rodrigo Bruno (IST, ULisboa).

Título do evento

A collaborative initiative supported by five Portuguese research centers, aimed at strengthening and connecting the geometry research community in Portugal.

Equipa da Raiz Vertical Farms

Uma Experiência Única sobre Agricultura Urbana e Energia Renovável.

Título/data/local do evento e fotografia da cidade de Lisboa

The conference aims to bring together students and young researchers working in Mathematics, Statistics, and Applications with a view to fostering discussions and collaborations amongst participants.

Seminário do Instituto de Astrofísica e Ciências do Espaço, por Amidou Sorgho (Instituto de Astrofísica de Andalucía - IAA-CSIC, Spain).

Título/data/local do evento e representação de ser humano

Workshop de Medicina Nuclear, organizado pelo Instituto de Biofísica e Engenharia Biomédica.

Título "Para um ensino humanista das ciências" e logótipos das entidades organizadoras

O evento tem como tema principal "Para um ensino humanista das ciências" e conta com a participação de vários professores de CIÊNCIAS.

Microplásticos em suspensão no oceano

O curso tem como objetivo dar formação sobre a problemática da contaminação por detritos de plástico dos nossos ecossistemas, bem como alertar para os potenciais efeitos deletérios nos organismos - candidaturas até 22 de março.

Banner do Dia de Ciências 2025

A 29 de abril assinalamos o 114.º aniversário de CIÊNCIAS.

Junte-se a nós no Grande Auditório de CIÊNCIAS para uma tarde de celebração que reúne toda a comunidade da Faculdade.

Fotografia de fábrica a emitir poluição para a atmosfera

The course aims at enabling the participants to use different methods to measure the impacts of pollutants on ecosystems.

Logótipo C-Academy

O curso oferece uma base sólida sobre os fundamentos e práticas essenciais para proteger sistemas e dados num mundo cada vez mais digital - candidaturas até 13 de abril.

Banner Dia Aberto de CIÊNCIAS 2025.

Bem-vindos a Ciências ULisboa!

Um concurso de programação dirigido aos alunos do ensino secundário (11.º e 12.º anos), que visa promover a prática e o gosto pela programação.

Fotografia de Chapim-azul

The goal of this course is to provide the participants with the most recent and practical knowledge on the use of Functional Diversity.

Mão a segurar em globo de vidro

Curso acreditado pelo CCPFC para efeitos de progressão na carreira dos professores na dimensão cientifico-pedagógica dos grupos 230, 420, 510, 520 e 560, com candidaturas até 30 de abril.

Título/data/local do evento, logótipos das entidades organizadoras e fotografia de peixe

The event aims to facilitate the exchange of information and knowledge among professionals to advance the understanding, collaboration and capabilities of aquaculture to respond to the impact of climate change in a rapidly changing global environment.

Uma oportunidade única para interagir com a comunidade global de computação científica, com inscrições (preço reduzido) até 02 de maio.

Páginas