Criado primeiro software em nuvem resistente a hackers

Informtica

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

Software matematicamente seguro

Engenheiros da Universidade de Colmbia, 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 computao em nuvem.

A verificao formal o processo de provar matematicamente que o software faz o que se espera dele, que o cdigo do programa funciona como deveria e que no h bugs de segurana ocultos com que se preocupar.

Por exemplo, quando algum faz uma compra em um site, os dados desse cliente so atualizados automaticamente e armazenados em milhares de mquinas virtuais na nuvem. Qualquer vulnerabilidade, em qualquer uma dessas mquinas virtuais, abre a possibilidade de vazamento de dados e prejuzos.

Assim como os hackers no param, as equipes anti-hacker tambm tm dado muita ateno verificao formal, incluindo o trabalho de verificao dos sistemas operacionais com multiprocessador.

“Mas toda essa pesquisa foi conduzida em pequenos sistemas parecidos com brinquedos, que ningum usa na vida real. Verificar um sistema de multiprocessador comercial, um sistema amplamente utilizado como o Linux, foi considerado mais ou menos impossvel,” conta Ronghui Gu, membro da equipe.

O processo de verificao formal feito nos hipervisores, por meio de um mecanismo chamado microverificao.
[Imagem: Shih-Wei Li et al. – 10.1109/SP40001.2021.00049]

Hipervisores

O trabalho de monitoramento e fiscalizao dos programas rodando na nuvem ficam a cargo dos chamados “hipervisores”, programas usados para executar e gerenciar uma ou mais mquinas virtuais. Assim, a segurana dos dados depende da exatido e da confiabilidade do hipervisor.

Contudo, apesar de sua importncia, os hipervisores so complicados – eles podem incluir um sistema operacional Linux inteiro. Apenas um nico elo fraco no cdigo – que virtualmente impossvel de detectar por meio dos testes tradicionais – pode tornar um sistema vulnervel. Mesmo se um hipervisor for escrito 99% corretamente, um hacker ainda pode se infiltrar naquela configurao 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 modificaes que garantem que as mquinas virtuais so seguras e isoladas uma das outras. E provaram isto matematicamente.

Microverificao

Esta nova verso do hipervisor, batizada de SeKVM (Secure KVM) foi verificada usando MicroV, uma nova estrutura para validar as propriedades de segurana de grandes sistemas. A MicroV parte da hiptese de que pequenas mudanas no sistema podem torn-lo significativamente mais fcil de verificar, uma nova tcnica que os pesquisadores chamam de microverificao.

Essa nova tcnica em camadas atualiza e corrige um sistema existente e extrai os componentes que reforam a segurana em um pequeno ncleo, que ento verificado, o que garante a segurana de todo o sistema.

“Ns mostramos que nosso sistema pode salvaguardar e proteger computaes e dados privados enviados para a nuvem com garantias matemticas. Isso nunca foi feito antes,” disse o professor Xupeng Li.

“A SeKVM servir como uma proteo em vrios domnios, de sistemas bancrios e dispositivos de Internet das Coisas a veculos autnomos e criptomoedas,” acrescentou seu colega Shih-Wei Li.

Outras notcias sobre: