Grabado: 21/07/2021 Seminario de Seguridad CERIAS en la Universidad de Purdue Un Verificador Formal para el Lenguaje Move de la Blockchain Diem David Dill, Facebook La blockchain Diem, que fue iniciada en 2018 por Facebook, incluye un nuevo lenguaje de programación llamado Move para implementar contratos inteligentes. La corrección de los programas Move es especialmente importante porque la blockchain albergará grandes cantidades de activos, esos activos son gestionados por contratos inteligentes, y porque ha habido un historial de grandes pérdidas en otras blockchains debido a errores en contratos inteligentes. El lenguaje Move está diseñado para ser lo más seguro posible, y viene acompañado de una especificación formal y una herramienta de verificación automática, llamada Move Prover. Un proyecto para especificar y verificar formalmente tantas propiedades importantes de la biblioteca estándar de Move está en marcha. Esta charla tratará sobre los objetivos del proyecto y las ideas más interesantes que hemos tenido hasta el momento de la presentación. La implementación completa de la blockchain, incluyendo el lenguaje Move, la máquina virtual, el Move Prover y varios módulos de Move casi finales están disponibles en
http://github.com/libra \(Visita: www.cerias.purdue.edu\)