Sempre que você compra algo na Amazon, os dados do cliente são atualizados automaticamente e armazenados em milhares de máquinas virtuais na nuvem. Para empresas como a Amazon, garantir a segurança dos dados de seus milhões de clientes é essencial. Isso é verdadeiro para organizações grandes e pequenas. Mas, até agora, não houve nenhuma maneira de garantir que um sistema de software esteja protegido contra bugs, hackers e vulnerabilidades.
Os pesquisadores da Columbia Engineering podem ter resolvido esse problema de segurança. Eles desenvolveram o SeKVM, o primeiro sistema que garante - por meio de provas matemáticas - a segurança das máquinas virtuais na nuvem. Em um novo artigo a ser apresentado em 26 de maio de 2021, no 42º Simpósio IEEE sobre Segurança e Privacidade, os pesquisadores esperam estabelecer as bases para futuras inovações na verificação de software de sistema, levando a uma nova geração de software de sistema ciber-resiliente.
SeKVM é o primeiro sistema formalmente verificado para computação em nuvem. A verificação formal é uma etapa crítica, pois é o processo de provar que o software é matematicamente correto, que o código do programa funciona como deveria e não há bugs de segurança ocultos com que se preocupar.
“Esta é a primeira vez que um sistema de software multiprocessador do mundo real se mostra matematicamente correto e seguro”, disse Jason Nieh, professor de ciência da computação e codiretor do Software Systems Laboratory. “Isso significa que os dados dos usuários são gerenciados corretamente pelo software executado na nuvem e estão protegidos contra bugs de segurança e hackers.”
A construção de software de sistema correto e seguro tem sido um dos grandes desafios da computação. | Nieh trabalhou em diferentes aspectos dos sistemas de software desde que ingressou na Columbia Engineering em 1999. Quando Ronghui Gu, o professor assistente de ciência da computação da família Tang e especialista em verificação formal, ingressou no departamento de ciência da computação em 2018, ele e Nieh decidiram colaborar na exploração de verificação formal de sistemas de software.
Sua pesquisa atraiu grande interesse: ambos os pesquisadores ganharam um Prêmio de Pesquisa da Amazon, várias bolsas da National Science Foundation, bem como um contrato multimilionário da Defense Advanced Research Projects Agency (DARPA) para promover o desenvolvimento do projeto SeKVM. Além disso, Nieh recebeu uma bolsa Guggenheim por este trabalho.
Nos últimos XNUMX anos, deu-se muita atenção à verificação formal, incluindo o trabalho de verificação de sistemas operacionais com multiprocessador. “Mas toda essa pesquisa foi conduzida em pequenos sistemas parecidos com brinquedos que ninguém usa na vida real”, disse Gu. “A verificação de um sistema de commodity multiprocessador, um sistema amplamente utilizado como o Linux, foi considerada mais ou menos impossível.”
O crescimento exponencial da computação em nuvem permitiu que empresas e usuários movessem seus dados e computação fora do local para máquinas virtuais em execução em hosts na nuvem. Provedores de computação em nuvem, como a Amazon, implantam hipervisores para oferecer suporte a essas máquinas virtuais
Um hipervisor é a peça chave do software que torna possível a computação em nuvem. A segurança dos dados da máquina virtual depende da exatidão e confiabilidade do hipervisor. Apesar de sua importância, os hipervisores são complicados - eles podem incluir um sistema operacional Linux inteiro. Apenas um único link fraco no código - virtualmente impossível de detectar por meio de testes tradicionais - pode tornar um sistema vulnerável a hackers. Mesmo se um hipervisor for escrito 99% corretamente, um hacker ainda pode se infiltrar naquela configuração de 1% específica e assumir o controle do sistema.
O trabalho de Nieh e Gu é o primeiro a verificar um sistema de commodity, especificamente o hipervisor KVM amplamente usado, que é usado para executar máquinas virtuais por provedores de nuvem como a Amazon. Eles provaram que o SeKVM, que é o KVM com algumas pequenas alterações, é seguro e garante que os computadores virtuais fiquem isolados uns dos outros.
“Nós mostramos que nosso sistema pode proteger e proteger dados privados e computação carregada para a nuvem com garantias matemáticas”, disse Xupeng Li, Ph.D. de Gu aluno e co-autor principal do artigo. “Isso nunca foi feito antes.”
O SeKVM foi verificado usando MicroV, uma nova estrutura para verificar as propriedades de segurança de grandes sistemas. Baseia-se na 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 verificação MICR. Essa nova técnica de camadas atualiza um sistema existente e extrai os componentes que reforçam a segurança em um pequeno núcleo que é verificado e garante a segurança de todo o sistema.
As mudanças necessárias para adaptar um sistema grande são bastante modestas - os pesquisadores demonstraram que, se o pequeno núcleo do sistema maior estiver intacto, o sistema está seguro e nenhum dado privado será vazado. Foi assim que conseguiram verificar um grande sistema como o KVM, que antes se pensava ser impossível.
“Pense em uma casa - uma rachadura na parede de gesso não significa que a integridade da casa esteja em risco”, explicou Nieh. “Ainda é estruturalmente sólido e o sistema estrutural principal é bom.”
Shih-Wei Li, Ph.D. de Nieh O aluno e co-autor principal do estudo, acrescentou: “O SeKVM servirá como uma salvaguarda em vários domínios, desde sistemas bancários e dispositivos de Internet das Coisas a veículos autônomos e criptomoedas”.
Como o primeiro hipervisor de commodity verificado, o SeKVM pode mudar a forma como os serviços em nuvem devem ser projetados, desenvolvidos, implantados e confiáveis. Em um mundo onde cíber segurança é uma preocupação crescente, essa resiliência é altamente solicitada. As principais empresas de nuvem já estão explorando como podem aproveitar o SeKVM para atender a essa demanda.