Pesquisadores da Universidade de Col\u00fambia criaram um hipervisor seguro baseado em Linux.<\/p>\n
\u00a0<\/p>\n
O software hipervisor complexo ajuda a executar os computadores em nuvem, mas verificar sua seguran\u00e7a costuma ser considerado quase imposs\u00edvel. Agora, os cientistas da computa\u00e7\u00e3o da Universidade de Col\u00fambia desenvolveram o que dizem ser o primeiro hipervisor que pode garantir a computa\u00e7\u00e3o em nuvem segura.<\/p>\n
\u00a0<\/p>\n
Os hipervisores organizam servidores em nuvem em m\u00e1quinas virtuais para fornecer dados e poder de computa\u00e7\u00e3o pela Internet. Hackers que exploram com sucesso as vulnerabilidades do hipervisor podem obter acesso irrestrito aos dados de milh\u00f5es de clientes de provedores de computa\u00e7\u00e3o em nuvem, como a Amazon.<\/p>\n
\u00a0<\/p>\n
“Basta um \u00fanico elo fraco no c\u00f3digo que \u00e9 virtualmente imposs\u00edvel de detectar por meio de testes tradicionais para deixar um sistema vulner\u00e1vel a hackers”, disse Ronghui Gu, um cientista da computa\u00e7\u00e3o da Escola de Engenharia e Ci\u00eancias Aplicadas da Universidade de Col\u00fambia e co-autor do estudo publicado pelos pesquisadores sobre o trabalho.<\/p>\n
\u00a0<\/p>\n
Em teoria, os cientistas podem verificar formalmente o software para provar matematicamente que seu c\u00f3digo “protege a seguran\u00e7a dos dados em 100% das circunst\u00e2ncias”, conforme Ronghui Gu. No entanto, a maioria dos hipervisores verificados costumam ser muito mais simples do que seus equivalentes comerciais, uma vez que s\u00e3o projetados especificamente para verifica\u00e7\u00e3o em vez de aplica\u00e7\u00f5es pr\u00e1ticas. Em contraste, os hipervisores comerciais modernos s\u00e3o pe\u00e7as enormes de software, muitas vezes incluindo um kernel de sistema operacional inteiro, o que pode tornar a verifica\u00e7\u00e3o deles uma tarefa aparentemente intranspon\u00edvel.<\/p>\n
\u00a0<\/p>\n
Por exemplo, levou tr\u00eas anos para verificar 6.500 linhas de c\u00f3digo com o hipervisor CertiKOS e 10 anos para verificar 9.000 linhas de c\u00f3digo com o hipervisor seL4, ambos projetados para verifica\u00e7\u00e3o. Em compara\u00e7\u00e3o, o hipervisor de c\u00f3digo aberto KVM amplamente usado, um sistema multiprocessador completo integrado ao Linux, tem mais de 2 milh\u00f5es de linhas de c\u00f3digo.<\/p>\n
\u00a0<\/p>\n
Agora, os cientistas da computa\u00e7\u00e3o de Col\u00fambia desenvolveram uma maneira de verificar os hipervisores de n\u00edvel comercial. Eles usaram sua nova t\u00e9cnica para desenvolver uma vers\u00e3o segura do KVM chamada SeKVM, que eles sugerem ser o primeiro hipervisor de n\u00edvel comercial verificado formalmente por m\u00e1quina.<\/p>\n
\u00a0<\/p>\n
Os pesquisadores batizaram sua nova t\u00e9cnica de microverifica\u00e7\u00e3o, que reduz a quantidade de trabalho necess\u00e1ria para verificar um hipervisor. Ele divide um hipervisor em um pequeno n\u00facleo e um conjunto de servi\u00e7os n\u00e3o confi\u00e1veis \u200b\u200be, em seguida, prova a seguran\u00e7a do hipervisor verificando apenas o n\u00facleo. O n\u00facleo n\u00e3o tem vulnerabilidades para serem exploradas por um hacker, e esse n\u00facleo medeia todas as intera\u00e7\u00f5es do hipervisor com as m\u00e1quinas virtuais, portanto, mesmo que um hacker prejudique uma m\u00e1quina virtual, n\u00e3o compromete as outras.<\/p>\n
\u00a0<\/p>\n
Com base na microverifica\u00e7\u00e3o, os cientistas desenvolveram um software chamado MicroV para verificar grandes hipervisores multiprocessadores de n\u00edvel comercial. Com a ajuda da MicroV, eles desenvolveram um n\u00facleo seguro para SeKVM com apenas 3.800 linhas de c\u00f3digo, que verificaram ao longo de dois anos.<\/p>\n
\u00a0<\/p>\n
Quando se trata de cargas de trabalho de aplicativos reais, o SeKVM teve um desempenho semelhante ao KVM n\u00e3o modificado, no m\u00e1ximo incorrendo em menos de 10% de sobrecarga de desempenho no hardware nativo. O KVM foi projetado especificamente para ser executado.<\/p>\n
\u00a0<\/p>\n
Ao mesmo tempo, o SeKVM suportava uma ampla gama de recursos do KVM. “SeKVM \u00e9 apenas KVM com algumas pequenas altera\u00e7\u00f5es”, diz o co-autor do estudo Jason Nieh, cientista da computa\u00e7\u00e3o da Escola de Engenharia e Ci\u00eancias Aplicadas da Universidade de Columbia.<\/p>\n
\u00a0<\/p>\n
“Ele funciona como o KVM normal, herda a funcionalidade do KVM normal, mas, al\u00e9m disso, oferece garantias de seguran\u00e7a que o KVM normal n\u00e3o tem.” No futuro, “continuaremos explorando esse conceito de software de sistemas ciber-resilientes e criaremos prote\u00e7\u00f5es em v\u00e1rios dom\u00ednios, desde sistemas banc\u00e1rios e dispositivos de Internet das Coisas a ve\u00edculos aut\u00f4nomos e criptomoedas”, conforme Ronghui Gu.<\/p>\n
\u00a0<\/p>\n
“O SeKVM estabelecer\u00e1 uma base para futuras inova\u00e7\u00f5es na verifica\u00e7\u00e3o de sistemas e levar\u00e1 a uma nova gera\u00e7\u00e3o de software de sistemas ciber-resilientes. Em um mundo onde a ciberseguran\u00e7a \u00e9 uma preocupa\u00e7\u00e3o crescente, essa resili\u00eancia est\u00e1 em alta demanda.”<\/p>\n
\u00a0<\/p>\n