Gravado: 21/07/2021 Seminário de Segurança CERIAS na Universidade Purdue Um Verificador Formal para a Linguagem Move da Blockchain Diem David Dill, Facebook A blockchain Diem, que foi iniciada em 2018 pelo Facebook, inclui uma nova linguagem de programação chamada Move para implementar contratos inteligentes. A correção dos programas Move é especialmente importante porque a blockchain hospedará grandes quantidades de ativos, esses ativos são gerenciados por contratos inteligentes e porque há um histórico de grandes perdas em outras blockchains devido a bugs em contratos inteligentes. A linguagem Move foi projetada para ser o mais segura possível e é acompanhada por uma especificação formal e uma ferramenta de verificação automática, chamada Move Prover. Um projeto para especificar e verificar formalmente o maior número possível de propriedades importantes da biblioteca padrão Move está agora bem avançado. Esta palestra será sobre os objetivos do projeto e as percepções mais interessantes que tivemos até o momento da apresentação. Toda a implementação da blockchain, incluindo a linguagem Move, a máquina virtual, o Move Prover e vários módulos Move quase finais estão disponíveis em
http://github.com/libra \(Visite: www.cerias.purdue.edu\)