Criado primeiro software em nuvem matematicamente seguro

Redação do Site Inovação Tecnológica - 27/05/2021

O sistema garante matematicamente a segurança das máquinas virtuais.
[Imagem: Jason Nieh-Ronghui Gu/Columbia Engineering]

Software matematicamente seguro

Engenheiros da Universidade de Colúmbia, nos EUA, afirmam ter criado o "primeiro sistema de software multiprocessador do mundo real que é matematicamente correto e seguro".

Batizado de SeKVM, é o primeiro sistema formalmente verificado para computação em nuvem.

A verificação formal é o processo de provar matematicamente que o software faz o que se espera dele, que o código do programa funciona como deveria e que não há bugs de segurança ocultos com que se preocupar.

Por exemplo, quando alguém faz uma compra em um site, os dados desse cliente são atualizados automaticamente e armazenados em milhares de máquinas virtuais na nuvem. Qualquer vulnerabilidade, em qualquer uma dessas máquinas virtuais, abre a possibilidade de vazamento de dados e prejuízos.

Assim como os hackers não param, as equipes anti-hacker também têm dado muita atenção à verificação formal, incluindo o trabalho de verificação dos sistemas operacionais com multiprocessador.

"Mas toda essa pesquisa foi conduzida em pequenos sistemas parecidos com brinquedos, que ninguém usa na vida real. Verificar um sistema de multiprocessador comercial, um sistema amplamente utilizado como o Linux, foi considerado mais ou menos impossível," conta Ronghui Gu, membro da equipe.

O processo de verificação formal é feito nos hipervisores, por meio de um mecanismo chamado microverificação.
[Imagem: Shih-Wei Li et al. - 10.1109/SP40001.2021.00049]

Hipervisores

O trabalho de monitoramento e fiscalização dos programas rodando na nuvem ficam a cargo dos chamados "hipervisores", programas usados para executar e gerenciar uma ou mais máquinas virtuais. Assim, a segurança dos dados depende da exatidão e da confiabilidade do hipervisor.

Contudo, apesar de sua importância, os hipervisores são complicados - eles podem incluir um sistema operacional Linux inteiro. Apenas um único elo fraco no código - que é virtualmente impossível de detectar por meio dos testes tradicionais - pode tornar um sistema vulnerável. Mesmo se um hipervisor for escrito 99% corretamente, um hacker ainda pode se infiltrar naquela configuração de 1% em particular e assumir o controle do sistema.

O trabalho da equipe consistiu em aprimorar um hipervisor largamente utilizado, chamado KVM, adicionando-lhe modificações que garantem que as máquinas virtuais são seguras e isoladas uma das outras. E provaram isto matematicamente.

Microverificação

Esta nova versão do hipervisor, batizada de SeKVM (Secure KVM) foi verificada usando MicroV, uma nova estrutura para validar as propriedades de segurança de grandes sistemas. A MicroV parte da hipótese de que pequenas mudanças no sistema podem torná-lo significativamente mais fácil de verificar, uma nova técnica que os pesquisadores chamam de microverificação.

Essa nova técnica em camadas atualiza e corrige um sistema existente e extrai os componentes que reforçam a segurança em um pequeno núcleo, que é então verificado, o que garante a segurança de todo o sistema.

"Nós mostramos que nosso sistema pode salvaguardar e proteger computações e dados privados enviados para a nuvem com garantias matemáticas. Isso nunca foi feito antes," disse o professor Xupeng Li.

"A SeKVM servirá como uma proteção em vários domínios, de sistemas bancários e dispositivos de Internet das Coisas a veículos autônomos e criptomoedas," acrescentou seu colega Shih-Wei Li.

Mais tópicos