Melhorando a Verificação de Software com Análise de Intervalo

Bugs de software podem causar vários problemas, desde chatices pequenas até questões sérias de segurança. Para sistemas que são vitais para a segurança, esses bugs podem resultar em perdas financeiras significativas. Por exemplo, uma grande companhia aérea enfrentou uma perda de bilhões de dólares devido a uma série de bugs em seus sistemas. Essa situação destaca a necessidade de um software confiável que atenda aos padrões de qualidade. Métodos de teste tradicionais nem sempre são suficientes. Métodos formais que verificam o software por meio de processos estruturados podem ajudar a garantir a qualidade do software.

A verificação de modelos é um método formal que examina um modelo para verificar se ele atende a uma Propriedade de Segurança. A Verificação de Modelo Limitada (BMC) é uma abordagem popular usada na indústria de software. Empresas como Amazon e ARM já usaram BMC para suas tarefas de Verificação de Software. O BMC ajuda os desenvolvedores a identificar bugs de forma eficaz. No entanto, o BMC tem suas limitações, incluindo Explosão do espaço de estados e incompletude, que podem atrapalhar sua eficácia em aplicações do mundo real.

A Análise de Intervalos é outra técnica usada na verificação de software para identificar vulnerabilidades. Ela funciona calculando intervalos para valores de variáveis em um programa. Isso pode ajudar a melhorar a eficiência do BMC, eliminando caminhos de programa inatingíveis e provando algumas afirmações de forma consistente. Porém, aplicar a análise de intervalos tem um custo em termos de recursos computacionais.

Este artigo apresenta uma análise da relação entre análise de intervalos e BMC. Nosso objetivo é avaliar se as vantagens obtidas através da análise de intervalos justificam os custos computacionais adicionais. Vamos analisar os benefícios da análise de intervalos usando benchmarks específicos, incluindo programas do firmware de gerenciamento de energia da Intel e entradas da categoria ReachSafety em uma competição de verificação de software. Nossos resultados mostram que a análise de intervalos desempenha um papel crítico em relação a benchmarks únicos.

#A Necessidade de Verificação de Software

Bugs de software podem afetar sistemas de várias maneiras. Para sistemas críticos de segurança, as consequências podem ser severas. Esses bugs podem causar falhas que levam a riscos à segurança e perdas financeiras. Portanto, garantir a qualidade do software é essencial. Métodos formais oferecem uma forma estruturada de verificar o software. Eles oferecem melhor segurança do que métodos de teste tradicionais.

O BMC é um desses métodos formais. Ele explora sistematicamente um programa para verificar se ele atende a uma propriedade de segurança. Embora o BMC tenha ganhado popularidade na indústria, ele tem desvantagens significativas. A explosão do espaço de estados refere-se ao crescimento rápido do número de estados que precisam ser examinados, tornando o processo de verificação cada vez mais complexo. Além disso, o BMC não consegue produzir uma prova de segurança para cenários não limitados, o que limita seu uso em aplicações do mundo real.

A análise de intervalos é um método que pode ajudar a superar alguns desses desafios. Ela calcula o intervalo possível de valores para as variáveis de um programa. Ao fazer isso, pode eliminar certos caminhos que não precisam ser inspecionados, o que pode melhorar a eficiência do processo de verificação.

#Verificação de Modelo Limitada (BMC)

O BMC é uma abordagem de verificação que investiga um sistema em relação a uma propriedade de segurança. Ele gera fórmulas para verificar se há contraexemplos (documentos que mostram que o sistema poderia violar a propriedade de segurança) dentro de um comprimento especificado. Esse método é benéfico porque permite que pesquisadores e desenvolvedores limitem o número de estados que precisam explorar, ajudando a gerenciar o problema da explosão do estado.

No entanto, o BMC tem suas limitações. Ele não pode provar segurança para rastreamentos não limitados, já que só pode verificar contraexemplos até um certo comprimento. Isso significa que, se houver um problema que requer explorar estados além dos limites especificados, o BMC pode não ser capaz de identificá-lo.

#Análise de Intervalos

A análise de intervalos envolve calcular os valores mínimo e máximo possíveis para todas as variáveis dentro de um programa. Isso ajuda a definir o intervalo de valores que cada variável pode assumir em qualquer ponto. Ao entender esses intervalos, torna-se possível determinar se certos caminhos do programa podem ser ignorados durante o processo de verificação.

Por exemplo, se o intervalo calculado para uma variável mostra que ela não pode assumir um valor específico, então o caminho correspondente do programa pode ser ignorado. Isso reduz bastante a complexidade da verificação.

A análise de intervalos pode ser realizada de várias maneiras, incluindo métodos estáticos e dinâmicos. Neste trabalho, focamos na análise de intervalos estática, que computa intervalos sem executar o programa.

A análise de intervalos fornece um meio para refinar o processo do BMC. Ao remover caminhos inatingíveis e afirmando que certas condições se mantêm para todos os valores possíveis, pode melhorar significativamente a eficácia dos métodos de verificação.

#Desafios na Aplicação da Análise de Intervalos ao BMC

Embora a análise de intervalos ofereça benefícios substanciais, ela também traz desafios. O principal problema é que calcular intervalos com precisão pode exigir recursos computacionais significativos. Isso pode contrabalançar as vantagens obtidas com a análise de intervalos. Portanto, é preciso encontrar um equilíbrio cuidadoso entre o custo computacional da análise de intervalos e os ganhos de eficiência no BMC.

Alguns dos desafios de aplicar efetivamente a análise de intervalos incluem:

• Determinar em qual estágio no BMC a análise de intervalos deve ser introduzida para obter o máximo benefício.
• Medir o impacto geral de intervalos mais apertados nos resultados da verificação.
• Comparar diferentes maneiras de representar intervalos para inteiros de máquina, o que pode afetar os resultados da verificação.

Para enfrentar esses desafios, investigamos vários aspectos da análise de intervalos e do BMC nas seções seguintes.

#Contribuições deste Trabalho

Este trabalho apresenta várias contribuições principais voltadas para melhorar os processos de verificação de software.

• Implementamos a análise de intervalos dentro do ESBMC, um verificador de modelo de software proeminente no mercado.
• Avaliamos os efeitos de diferentes técnicas de análise de intervalos no desempenho geral do BMC na verificação de software.
• Quantificamos os benefícios de introduzir intervalos no programa e seu impacto no tempo de resolução e uso de memória.
• Avaliamos a combinação de análise de intervalos e BMC em um conjunto de programas em C da categoria ReachSafety.
• Ilustramos as melhorias que resultam da aplicação da análise de intervalos em cenários do mundo real, como o firmware de gerenciamento de potência da Intel.

#Configuração Experimental

Para explorar a relação entre a análise de intervalos e o BMC, montamos experimentos usando benchmarks específicos. Os benchmarks incluem programas da Competição Internacional de Verificação de Software (SV-COMP) e do firmware de gerenciamento de potência da Intel.

Nosso objetivo é avaliar como a análise de intervalos afeta o desempenho do ESBMC como uma ferramenta de verificação de software. Limitamos os recursos computacionais para garantir que nossas descobertas possam ser interpretadas com precisão.

Comparamos duas configurações dentro do ESBMC:

• Base: Esta configuração não usa cálculos de intervalos.
• Intervalos: Esta configuração utiliza a análise de intervalos e otimizações relacionadas.

Examinamos como cada configuração se sai nos benchmarks, focando em métricas como o número de benchmarks resolvidos, tempo de CPU consumido e memória utilizada.

#Resultados e Discussão

Os experimentos mostram que a análise de intervalos pode melhorar o desempenho do ESBMC. Os resultados mostram um aumento geral no número de benchmarks resolvidos quando a análise de intervalos é aplicada. As melhorias mais significativas vêm da capacidade da análise de intervalos de provar a segurança de benchmarks adicionais, em vez de descobrir violações em benchmarks inseguros.

No entanto, a adição da análise de intervalos vem com um custo, aumentando a carga computacional. Embora aumente levemente os tempos de CPU, os benefícios de resolver mais benchmarks podem superar o consumo adicional de recursos.

#Resultados Únicos por Categoria

Os experimentos também destacam categorias específicas onde a análise de intervalos teve um efeito notável. Por exemplo, programas que manipulam variáveis baseadas em eventos ou contêm loops infinitos mostram melhorias devido à introdução da análise de intervalos.

Ao lidar com sistemas de eventos, calcular intervalos reduz o número de caminhos que o BMC deve examinar. Da mesma forma, a análise de intervalos ajuda em programas com loops infinitos, permitindo um raciocínio mais eficiente através de algoritmos de k-indução.

Os resultados indicam que a análise de intervalos pode ser particularmente benéfica para benchmarks com uma estrutura complexa ou um alto número de variáveis.

#Conclusão

Este trabalho demonstra com sucesso que implementar a análise de intervalos dentro de uma estrutura BMC pode melhorar o processo de verificação de software. Ao calcular os intervalos das variáveis, a análise de intervalos simplifica o processo de verificação, permitindo que ferramentas como o ESBMC lidem de forma eficaz com programas maiores e mais complexos.

No geral, o uso da análise de intervalos leva a invariantes mais fortes, aprimorando ainda mais as capacidades do BMC e dos algoritmos de k-indução. Embora a análise de intervalos aumente os custos computacionais em alguns casos, seus benefícios sugerem que ela deve ser considerada uma parte importante do kit de ferramentas de verificação de software.

Trabalhos futuros nessa área vão focar em ampliar o escopo da análise de intervalos para incluir tipos adicionais de afirmações e aplicar essa análise à execução simbólica. Tais avanços poderiam aprimorar ainda mais a compreensão do comportamento do software e melhorar os processos de verificação.

Em resumo, a análise de intervalos oferece uma abordagem promissora para enfrentar os desafios encontrados na verificação de software, levando a sistemas mais seguros e confiáveis.