LSVerifier: a BMC approach to identify security vulnerabilities in C open-source software projects

Abstract

Esta pesquisa avança o campo da análise de vulnerabilidades de software, destacando o papel crítico das técnicas de validação e verificação formal de software no desenvolvimento de sistemas com alta dependabilidade e confiabilidade. O estudo enfoca nas propriedades de segurança da memória em software C. Introduzimos o LSVerifier, uma ferramenta inovadora que utiliza a técnica de Bounded Model Checking (BMC) para identificar vulnerabilidades de segurança em software de código aberto em C. O LSVerifier destaca-se não apenas por identificar vulnerabilidades, mas também gera um relatório detalhado das potenciais vulnerabilidades detectadas. Nossa avaliação experimental demonstra a eficácia da ferramenta na inspeção de grandes sistemas de software enquanto mantém um uso baixo de memória. Aplicamos o LSVerifier a doze projetos de C de código aberto, detectando com sucesso vulnerabilidades reais de software que foram posteriormente reconhecidas e confirmadas pelos desenvolvedores. Os resultados deste estudo destacam o potencial do LSVerifier como uma ferramenta chave no esforço contínuo para proteger o software de código aberto contra vulnerabilidades.