Por Professor Manuel Barbosa
No dia 20 de outubro, às 14h30, na sala FC6 0.28, Manuel Barbosa dará uma palestra intitulada "A Abordagem Formosa-Crypto a Provas Formais em Criptografia".
Título:
A Abordagem Formosa-Crypto a Provas Formais em Criptografia
Resumo:
Nesta palestra, apresentarei o EasyCrypt e o Jasmin, e a forma como são usados para verificar formalmente implementações criptográficas de alta performance e relacionar a sua segurança com a de especificações de alto nível com segurança demonstrável.
Como casos de uso, utilizarei as normas pós-quânticas do NIST.
Será também discutido brevemente o trabalho em curso e futuro sobre estas ferramentas Formosa Crypto.
Bio:
Manuel Barbosa é docente no Departamento de Ciência de Computadores da Faculdade de Ciências da Universidade do Porto (DCC-FCUP) e investigador no INESC TEC. Os seus interesses de investigação situam-se nas áreas da Criptografia, Segurança da Informação e Verificação Formal. É doutorado em Engenharia Eletrotécnica e Eletrónica pela Newcastle University, onde também concluiu o grau de Mestre, e licenciado em Engenharia Eletrotécnica e de Computadores pela Faculdade de Engenharia da Universidade do Porto. No passado, foi investigador visitante na University of Bristol, École Normale Supérieure, Inria Sophia-Antipolis e Bar-Ilan University. Entre 2023 e 2025, foi investigador no Max Planck Institute for Security and Privacy. Tem mais de 15 anos de experiência no desenvolvimento de implementações criptográficas de elevada confiança, procurando colmatar a distância entre a segurança teórica e a segurança aplicada. Os seus principais interesses incluem segurança demonstrável e a sua relação com a verificação formal de provas criptográficas e de implementações de software criptográfico. É também membro do comité diretivo da Formosa Crypto (formosa-crypto.org), onde são desenvolvidos e promovidos os frameworks de verificação formal EasyCrypt e Jasmin.