Protegendo a Arm
Confidential Computing Architecture
23 violações de propriedade adicionais identificadas no Realm Management Monitor, o firmware privilegiado na raiz de confiança da Arm Confidential Computing Architecture do Armv9, além daquelas já detectadas pelo CBMC.
23
Violações de propriedade adicionais que somente o ESBMC detectou no firmware RMM da Arm
Armv9
A CCA está sendo implantada por todo o ecossistema Armv9
SAS 2024
Publicado no Static Analysis Symposium (Wu et al., 451–462)
Arm CoE
Cofinanciado via Arm Centre of Excellence na University of Manchester
Desafio
A Confidential Computing Architecture (CCA) da Arm provê isolamento de memória imposto por hardware e está sendo implantada por todo o ecossistema Armv9. O Realm Management Monitor (RMM) é o componente de firmware privilegiado em seu núcleo; ele impõe isolamento entre os mundos de memória Realm, Secure, Root e Non-secure, e é a raiz de confiança de toda a CCA.
Qualquer violação de propriedade no RMM poderia comprometer as garantias de confidencialidade das cargas de trabalho em nuvem rodando em hardware habilitado para CCA. Engenheiros da Arm haviam gerado automaticamente harnesses de verificação a partir da especificação legível por máquina do RMM e já estavam implantando o CBMC (o C Bounded Model Checker de Daniel Kroening e Michael Tautschnig) contra esses harnesses em seu CI/CD, confirmando e corrigindo várias violações ao longo do caminho. A questão em aberto que os colaboradores da Arm queriam responder era se um model checker de ponta diferente poderia revelar mais violações no mesmo código.
Abordagem
Trabalhando com engenheiros da Arm, incluindo os coautores Shale Xiong e Gareth Stockwell, aplicamos o ESBMC aos harnesses de verificação do RMM contra as propriedades de segurança e proteção definidas na especificação do RMM. Primeiro reproduzimos as violações que o CBMC havia reportado anteriormente (e que os engenheiros da Arm já haviam confirmado), e então rodamos o ESBMC contra a mesma base de código em busca de achados adicionais.
Durante a comparação, também identificamos um pequeno número de casos em que o CBMC e o ESBMC produziam veredictos inconsistentes. Reportamos esses casos à equipe do CBMC, que confirmou um bug subjacente no modelo de memória (diffblue/cbmc#8161). O trabalho foi publicado no SAS 2024 e os artefatos de verificação foram depositados no Zenodo para reprodutibilidade.
Resultados
23 violações de propriedade adicionais identificadas na implementação do RMM que o ESBMC foi capaz de detectar além daquelas já reportadas pelo CBMC na mesma base de código.
Veredictos inconsistentes entre o CBMC e o ESBMC foram documentados e reportados ao upstream, levando a uma correção confirmada no modelo de memória do CBMC.
A coautoria da Arm no trabalho publicado, juntamente com o cofinanciamento via Arm Centre of Excellence na University of Manchester, confirma que esta foi uma colaboração do mundo real sobre firmware em vias de produção, e não um estudo de benchmark sintético.
Os achados fortaleceram a linha de base de garantia da implementação do RMM tal como publicada.
Referências
- Tong Wu, Shale Xiong, Edoardo Manino, Gareth Stockwell, Lucas C. Cordeiro. Verifying Components of Arm® Confidential Computing Architecture with ESBMC. SAS 2024: 451–462. ssvlab.github.io/lucasccordeiro/papers/sas2024.pdf
Nota. A colaboração descrita nesta página é um engajamento de pesquisa acadêmica publicado (SAS 2024) coautorado com engenheiros da Arm e parcialmente financiado via Arm Centre of Excellence na University of Manchester. O CBMC é uma ferramenta independente de terceiros, criada por Daniel Kroening e Michael Tautschnig; a inconsistência descrita acima foi reportada ao upstream e confirmada pelos mantenedores do CBMC. Achados reportados como "violações de propriedade" são violações de asserção ou de especificação identificadas pelo model checker no código RMM publicado; o artigo não os caracteriza como vulnerabilidades de segurança exploráveis.