Nova ferramenta automatiza a verificação formal de software de sistemas

A verificação formal de sistemas, que prova matematicamente que o código é seguro em todas as circunstâncias, é uma tecnologia relativamente nova. O software está ficando mais complexo e mais difícil de acertar usando técnicas tradicionais de teste de software. Tornar o software correto, seguro e protegido está se tornando ainda mais crítico à medida que aumenta o uso de técnicas generativas de IA, como ChatGPT, para escrever programas automaticamente. Na verdade, haverá ainda mais necessidade de verificação para garantir que os programas gerados automaticamente estejam corretos.

Trabalho recente dirigido pelos professores Ronghui Gu e Jason Nieh apresentou uma nova ferramenta, Spoqque reduz significativamente os esforços complexos que as pessoas devem usar para verificar software do mundo real e torna possível verificar o código dos sistemas C existentes sem modificações.

A verificação formal oferece uma abordagem sistemática e rigorosa à verificação de software e hardware, ajudando a garantir que os sistemas se comportem corretamente e atendam às especificações pretendidas. Com o Spoq, muitos aspectos da verificação formal podem ser automatizados, reduzindo significativamente os esforços de prova manual para verificação. O artigo foi apresentado no 17º Simpósio USENIX sobre Conferência de Design e Implementação de Sistemas Operacionais (OSDI) em 12 de julho de 2023.

O software do sistema constitui a base de software da nossa infraestrutura de computação. O software de sistema moderno é grande, complexo e imperfeito, com vulnerabilidades que podem ser exploradas para comprometer a segurança de um sistema. A verificação formal oferece uma solução potencial para este problema, provando matematicamente que o software do sistema pode fornecer garantias de segurança críticas. Infelizmente, continua a ser demasiado difícil e requer demasiado esforço humano para ser aplicado na prática.

Ferramentas anteriores desenvolvidas pelas equipes de Nieh e Gu introduziram técnicas de verificação para tornar possíveis certas provas que não poderiam ter sido feitas antes. A principal característica do Spoq é que ele automatiza as partes tediosas e demoradas de muitas provas. “O Spoq pode gerar resultados em cerca de uma hora, em comparação com fazê-lo manualmente, o que pode levar meses ou anos para verificar formalmente um sistema”, diz Xupeng Li, principal autor do artigo e Ph.D. estudante com Nieh e Gu.

Nos próximos meses, o laboratório se concentrará em tornar o Spoq de código aberto para que a verificação formal possa ser amplamente implantada para proteger as bases do software de nossa infraestrutura de computação.

O estudo é intitulado “Spoq: Escalando a verificação de sistemas verificáveis ​​por máquina em Coq.”