Qualificação de mestrado do discente Marcos Braga, dia 13/12/2024 as 14:00.

Qualificação de mestrado do discente Marcos Braga, dia 13/12/2024 as 14:00.

Titulo: Uma semântica executável para eBPF

Resumo: O Extended Berkeley Packet Filter (eBPF) é um subsistema Linux que permite executar extensões não confiáveis definidas pelo usuário dentro do kernel. Para proteger o kernel contra código malicioso, o eBPF utiliza técnicas de análise estática simples. Porém, à medida que a linguagem eBPF cresce em popularidade, o seu ecossistema evolui para oferecer suporte a extensões mais complexas. Contudo, as limitações presentes em seu verificador atual, como a sua alta taxa de falsos positivos e falta de suporte a comandos de repetição, tornaram-se um grande empecilho para sua ampla adoção por desenvolvedores de aplicações de rede. Outro ponto a ser ressaltado é que a especificação da linguagem é textual, não havendo um artefato que descreva o significado da linguagem, permitindo assim, o desenvolvimento de novas extensões e ferramentas para análise de código eBPF. Neste sentido, o presente projeto pretende especificou formalmente uma parte da semântica de eBPF usando a linguagem Lean, permitindo assim que desenvolvedores de novas ferramentas de análise estática tenham acesso a uma versão executável da especificação desta linguagem.

Banca: Prof. Dr. Rodrigo Geraldo Ribeiro; Prof. Dr. Leonardo Vieira dos Santos Reis

Data e Hora: Sexta-feira, 13/12/2024, às 14h

Link do Meet: https://meet.google.com/xww-kxha-dca