Pesquisadores da Universidade de Colúmbia criaram um hipervisor seguro baseado em Linux.
O software hipervisor complexo ajuda a executar os computadores em nuvem, mas verificar sua segurança costuma ser considerado quase impossível. Agora, os cientistas da computação da Universidade de Colúmbia desenvolveram o que dizem ser o primeiro hipervisor que pode garantir a computação em nuvem segura.
Os hipervisores organizam servidores em nuvem em máquinas virtuais para fornecer dados e poder de computação pela Internet. Hackers que exploram com sucesso as vulnerabilidades do hipervisor podem obter acesso irrestrito aos dados de milhões de clientes de provedores de computação em nuvem, como a Amazon.
“Basta um único elo fraco no código que é virtualmente impossível de detectar por meio de testes tradicionais para deixar um sistema vulnerável a hackers”, disse Ronghui Gu, um cientista da computação da Escola de Engenharia e Ciências Aplicadas da Universidade de Colúmbia e co-autor do estudo publicado pelos pesquisadores sobre o trabalho.
Em teoria, os cientistas podem verificar formalmente o software para provar matematicamente que seu código “protege a segurança dos dados em 100% das circunstâncias”, conforme Ronghui Gu. No entanto, a maioria dos hipervisores verificados costumam ser muito mais simples do que seus equivalentes comerciais, uma vez que são projetados especificamente para verificação em vez de aplicações práticas. Em contraste, os hipervisores comerciais modernos são peças enormes de software, muitas vezes incluindo um kernel de sistema operacional inteiro, o que pode tornar a verificação deles uma tarefa aparentemente intransponível.
Por exemplo, levou três anos para verificar 6.500 linhas de código com o hipervisor CertiKOS e 10 anos para verificar 9.000 linhas de código com o hipervisor seL4, ambos projetados para verificação. Em comparação, o hipervisor de código aberto KVM amplamente usado, um sistema multiprocessador completo integrado ao Linux, tem mais de 2 milhões de linhas de código.
Agora, os cientistas da computação de Colúmbia desenvolveram uma maneira de verificar os hipervisores de nível comercial. Eles usaram sua nova técnica para desenvolver uma versão segura do KVM chamada SeKVM, que eles sugerem ser o primeiro hipervisor de nível comercial verificado formalmente por máquina.
Os pesquisadores batizaram sua nova técnica de microverificação, que reduz a quantidade de trabalho necessária para verificar um hipervisor. Ele divide um hipervisor em um pequeno núcleo e um conjunto de serviços não confiáveis e, em seguida, prova a segurança do hipervisor verificando apenas o núcleo. O núcleo não tem vulnerabilidades para serem exploradas por um hacker, e esse núcleo medeia todas as interações do hipervisor com as máquinas virtuais, portanto, mesmo que um hacker prejudique uma máquina virtual, não compromete as outras.
Com base na microverificação, os cientistas desenvolveram um software chamado MicroV para verificar grandes hipervisores multiprocessadores de nível comercial. Com a ajuda da MicroV, eles desenvolveram um núcleo seguro para SeKVM com apenas 3.800 linhas de código, que verificaram ao longo de dois anos.
Quando se trata de cargas de trabalho de aplicativos reais, o SeKVM teve um desempenho semelhante ao KVM não modificado, no máximo incorrendo em menos de 10% de sobrecarga de desempenho no hardware nativo. O KVM foi projetado especificamente para ser executado.
Ao mesmo tempo, o SeKVM suportava uma ampla gama de recursos do KVM. “SeKVM é apenas KVM com algumas pequenas alterações”, diz o co-autor do estudo Jason Nieh, cientista da computação da Escola de Engenharia e Ciências Aplicadas da Universidade de Columbia.
“Ele funciona como o KVM normal, herda a funcionalidade do KVM normal, mas, além disso, oferece garantias de segurança que o KVM normal não tem.” No futuro, “continuaremos explorando esse conceito de software de sistemas ciber-resilientes e criaremos proteções em vários domínios, desde sistemas bancários e dispositivos de Internet das Coisas a veículos autônomos e criptomoedas”, conforme Ronghui Gu.
“O SeKVM estabelecerá uma base para futuras inovações na verificação de sistemas e levará a uma nova geração de software de sistemas ciber-resilientes. Em um mundo onde a cibersegurança é uma preocupação crescente, essa resiliência está em alta demanda.”
Este artigo é uma tradução de: https://spectrum.ieee.org/riskfactor/computing/software/safe-hypervisor
