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

Um workshop com o objetivo de reunir académicos que abordam a história da ecologia - e a evolução da própria disciplina - a partir de uma variedade de perspetivas.

Cardume

Seminário no âmbito do Doutoramento em Ciências do Mar, por Inês Pereira.

Cartaz do evento

Palestra por Francisco Lobo (CIÊNCIAS ULisboa / Instituto de Astrofísica e Ciências do Espaço), no âmbito do Encontro com a Astronomia.

Pormenor de mecanismo de relógio

Concerto no âmbito do programa Música na Universidade de Lisboa.

Orquestra

Concerto no âmbito do programa Música na Universidade de Lisboa.

Banner Ser Cientista

A 10.ª edição do Ser Cientista realiza-se entre 21 e 25 de julho - vem investigar connosco!

Título e data da iniciativa

A iniciativa conta com a participação do MARE - Centro de Ciências do Mar e do Ambiente e do LASIGE Computer Science and Engineering Research Centre.

Aluna a utilizar um computador portátil

A Escola Doutoral Unite! Widening visa apoiar diretamente estudantes de doutoramento que realizem investigação numa das quatro áreas estratégicas selecionadas pelo projeto - as candidaturas decorrem até 26 de julho.

Pormenor de lâmpada

Candidaturas a decorrer de 01 a 30 de setembro.

Microplásticos no ocerano

O curso procura 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, utilizando uma abordagem de ensino científico, com um discurso adequado a formandos sem formação científica - candidaturas até 03 de agosto.

Logótipo do evento, sobre fotografia dos Açores

Um simpósio internacional que reúne investigadores especializados em várias disciplinas (taxonomia, ecologia da vegetação, biogeografia, filogeografia, paleoecologia ou conservação da biodiversidade), focados na flora e vegetação terrestre e marinha da região da Macaronésia (Açores, Madeira, Selvagens, Canárias e Cabo Verde).

Quatro investigadores num laboratório

O curso visa capacitar investigadores, docentes e técnicos para integrar os princípios da economia circular em ambientes laboratoriais académicos - candidaturas até 16 de setembro.

Composição de imagens relativas à área das ciências forenses

O curso visa dotar os formandos com os conhecimento necessários à integração de equipas profissionais multidisciplinares nas áreas Médico-Legais e Forenses, em Laboratórios ou Serviços Médico-Legais e Forenses - candidaturas até 27 de julho.

Três investigadores num laboratório

O curso visa capacitar profissionais para aplicar os princípios da economia circular em ambientes laboratoriais industriais, promovendo práticas sustentáveis e eficientes - candidaturas até 17 de setembro.

Logótipo do evento

Um evento promovido pelo Departamento de Física da Faculdade de Ciências da ULisboa, com um duplo objetivo: valorizar a diversidade e excelência da formação dos doutorados e promover um espaço de diálogo direto entre empresas e estudantes.

Cientista a trabalhar com tubos de ensaio

Os participantes neste curso irão adquirir os conhecimentos essenciais à integração de equipas profissionais multidisciplinares na área das Análises Clínicas/Patologia Clínica, em laboratórios privados, públicos, hospitalares ou do Estado - candidaturas até 27 de julho.

Saída de campo (Geologia)

O curso, com candidaturas até 20 de julho, convida os professores do Ensino Básico e Secundário a explorar a Geologia a partir das rochas que afloram nas imediações da sua escola.

Gotas de água

O curso visa capacitar os formandos para a aplicação dos índices de qualidade ecológica utilizados na avaliação da qualidade ambiental em sistemas de transição, no âmbito da Diretiva Quadro da Água (DQA) - candidaturas até 31 de agosto.

Astronauta, banhado pela luz solar, no meio de uma floresta

Candidaturas até 30 de julho - um evento único, que reunirá estudantes de mestrado e doutoramento com investigadores e líderes da indústria de toda a Europa para uma experiência inesquecível.

Lupa e caneta sobre página com texto e gráfico

O curso visa dar formação inicial a estudantes de pós-graduação sobre o processo de escrita, submissão e publicação de trabalhos científicos, focando principalmente a publicação de artigos científicos em revistas internacionais com revisão por pares.

Iconografia relacionada com a temática do curso

O curso fornece uma exploração aprofundada de isótopos estáveis como uma ferramenta valiosa em Ecologia, usando assinaturas isotópicas para rastrear processos ecológicos e revelando insights sobre o ciclo de nutrientes e água, interações de espécies e condições ambientais em diversos ecossistemas e comunidades.

Composição de três imagens relativas à área da deteção remota

2.ª edição do curso, com candidaturas até 18 de outubro.

O evento pretende reunir investigadores que trabalhem sobre temas ligados à indústria e sobre património técnico e industrial, para uma reflexão prospetiva sobre o património industrial e atuais vias de colaboração no seu estudo, salvaguarda e preservação.

Computador portátil a projetar imagem de sequência biológica

O curso visa a aquisição de conhecimentos sobre as ferramentas bioinformáticas disponíveis para efetuar análises de sequências de DNA e proteínas, bem como a autonomia e espírito crítico na utilização dessas ferramentas. Procura igualmente desenvolver competências na utilização de software de bioinformática disponível gratuitamente na Internet e na interpretação do significado biológico dos resultados.

Bola de cristal colocada no solo

O curso tem como objetivo apresentar aos participantes um estado da arte atualizado sobre a diversidade da biota do solo e os papéis funcionais desempenhados pelos organismos do solo nos principais processos ecológicos.

Páginas