0
0
Como nossos dados pessoais são cada vez mais usados em muitos aplicativos, desde publicidade, finanças e cuidados de saúde, a proteção de informações confidenciais tornou-se um recurso essencial para arquiteturas de computação.
Os aplicativos que processam esses dados devem confiar no software do sistema em que confiam, como sistemas operacionais e hipervisores, mas esse software do sistema é complexo e muitas vezes tem vulnerabilidades que podem arriscar a confidencialidade e a integridade dos dados.
Nos últimos dois anos, pesquisadores da Columbia Engineering têm trabalhado com a Arm, uma empresa de design de IP e software de semicondutores, para resolver essas vulnerabilidades. A equipe revelou as principais tecnologias de verificação para a Arm Confidential Compute Architecture (Arm CCA), um novo recurso da arquitetura Armv9-A. O artigo, apresentado no 16o Simpósio USENIX sobre Projeto e Implementação de Sistemas Operacionais, demonstra a primeira verificação formal de um protótipo de firmware Arm CCA.
A Arm CCA depende do firmware para gerenciar o hardware para fazer cumprir suas garantias de segurança, por isso é essencial que o firmware esteja correto e seguro. Embora muitos sistemas anteriores dependam do firmware, nenhum deles pode garantir que o firmware não tenha bugs.
A verificação formal é uma metodologia relativamente nova que agora está sendo usada para garantir a correção do software/hardware. Em vez de testar, a verificação formal usa modelos matemáticos para provar que o software e o hardware estão absolutamente corretos e, portanto, fornece o mais alto nível de garantia de correção.
“Nós provamos, pela primeira vez, que o firmware está correto e seguro, resultando na primeira demonstração de uma arquitetura de computação confidencial apoiada por firmware formalmente verificado”, disse o principal autor do estudo, Xupeng Li, estudante de doutorado da Ronghui Gu, Professor Assistente de Ciência da Computação da Família Tang, e Jason Nieh, professor de ciência da computação e codiretor do Laboratório de Sistemas
Embora existam muitas abordagens para verificar a correção de programas simples, elas não são adequadas para algo tão complexo quanto o firmware CCA, então os pesquisadores tiveram que desenvolver novas técnicas de verificação para tornar possível a verificação do firmware do Arm CCA. Por exemplo, o firmware CCA foi projetado para escalabilidade e desempenho, por isso permite uma operação altamente simultânea e mistura C e código de montagem. A operação simultânea é possível usando métodos de sincronização de grãos finos e código com corridas de dados.
É um princípio de design da Arm CCA que o software não confiável deve manter o controle do gerenciamento de recursos de hardware, portanto, um desafio fundamental é provar que o sistema ainda está seguro, mesmo que o software não confiável possa tirar os recursos de hardware, conforme quiser. Abordagens anteriores não conseguiram verificar programas com tais propriedades. Esta nova técnica de verificação é poderosa o suficiente para verificar o firmware concorrente com C e código de montagem.
“Os bugs são realmente difíceis de encontrar através de técnicas clássicas de teste de software”, disse Xuheng Li, coautor do trabalho. “Portanto, mostramos a importância e o valor de nossas técnicas formais de verificação, sendo o resultado final a primeira demonstração de uma arquitetura de computação confidencial apoiada por firmware verificado.”
A equipe está muito animada com as novas tecnologias de verificação que podem ser usadas para provar a correção das implementações de firmware subjacentes ao Arm CCA. As CPUs do braço já estão implantadas em bilhões de dispositivos em todo o mundo. À medida que o Arm CCA se torna mais comumente usado para proteger os dados privados do usuário, especialmente em serviços em nuvem e além, as técnicas de verificação demonstradas neste artigo fornecerão uma melhoria significativa na proteção e segurança de dados.
Um dos desafios com metodologias formais aplicadas ao software é a necessidade de adaptar provas quando o software é atualizado. Os pesquisadores estão trabalhando em novas tecnologias para ajudá-los a verificar de forma incremental e rápida as atualizações do firmware do Arm CCA e garantir que o firmware mais recente disponível seja sempre verificado.
Gu e Nieh acrescentaram: “Vemos o poder e o potencial da verificação formal do nosso trabalho, e estamos convencidos de que a verificação formal é uma técnica essencial que, em um futuro próximo, suplantará os testes de software no uso atual.”
FONTE: HELPNET SECURITY