Técnicas de contração de domínio de variáveis em verificação formal e detecção de vulnerabilidades de software usando programação por restrições e aritmética intervala - Deveza, Jessé de Souza (2024)
Nesta pesquisa são investigadas técnicas para resolução de problemas formulados para satisfazer um conjunto de restrições (Constraint Satisfaction Problems - CSP), modelados como expressões lógicas booleanas e cujas variáveis podem assumir valores reais, representando intervalos sobre os quais se aplica operações de aritmética intervalar e técnicas de programação por restrições (Constraint Programming - CP), para interseção, composição e contração de intervalos. Especificamente, o contexto de verificação formal de software é utilizado para a aplicação de redução do domínio de variáveis no pré-processamento de programas que usam verificação formal para provar por meio das teorias de módulo da satisfatibilidade (Satisfiability Modulo Theories - SMT) a satisfabilidade ou não da fórmula booleana que representa todos os estados do programa. Foi utilizado, portanto, o método formal de verificação de modelo limitado (Bounded Model Checking - BMC), que verifica em k passos se determinada propriedade é satisfatível ou, caso contrário, provê um contra-exemplo. Uma estratégia de pré-processamento BMC usando os programas modelados por CSP/CP e com soluções estimadas por uma técnica algorítmica de contração de intervalos é apresentada. Experimentos computacionais foram realizados usando benchmarks de programas em linguagem de programação C, Java e Kotlin, e utilizando o verificador ESBMC (e ESBMC-Jimple, desenvolvido no Projeto de PD&I SWPERFI UFAM-MOTOROLA, do qual esta pesquisa também faz parte) e outros. Os resultados indicam que, em muitos casos, há redução significativa do domínio das variáveis, influenciando na redução do espaço de busca exponencial da verificação de estados que, consequentemente, promove a diminuição do tempo de verificação dos programas, mostrando a adequabilidade da estratégia proposta. Além disso, o método também foi empregado na detecção de vulnerabilidades de softwares, especificamente naquelas que podem envolver operações com intervalos aritméticos, alcançando resultados satisfatórios para a maioria das categorias de vulnerabilidades utilizadas.