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; http://lattes.cnpq.br/0610645582446597

Dissertação

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

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 ap...

ver descrição completa

Autor principal:	Deveza, Jessé de Souza
Outros Autores:	http://lattes.cnpq.br/0610645582446597
Grau:	Dissertação
Idioma:	por
Publicado em:	Universidade Federal do Amazonas 2025
Assuntos:	CIENCIAS EXATAS E DA TERRA: CIENCIA DA COMPUTACAO Aritmética Intervalar ESBMC-Jimple Programação por Restrições Verificação Formal de Software Verificação de Modelo Limitado Vulnerabilidades
Acesso em linha:	https://tede.ufam.edu.br/handle/tede/10636

id	oai:https:--tede.ufam.edu.br-handle-:tede-10636
recordtype	dspace
spelling	oai:https:--tede.ufam.edu.br-handle-:tede-106362025-01-30T05:05:53Z 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 Rodrigues, Rosiane de Freitas http://lattes.cnpq.br/0610645582446597 http://lattes.cnpq.br/8358219976594707 Mota, Edjard de Souza Massera, José Miguel Aroztegui Lima Filho, Eddie Batista de CIENCIAS EXATAS E DA TERRA: CIENCIA DA COMPUTACAO Aritmética Intervalar ESBMC-Jimple Programação por Restrições Verificação Formal de Software Verificação de Modelo Limitado Vulnerabilidades 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. This research investigates techniques for solving problems formulated to satisfy a set of constraints (Constraint Satisfaction Problems - CSP), modeled as Boolean logical expressions and whose variables can assume real values, representing intervals over which interval arithmetic operations and techniques of constraint programming (Constraint Programming - CP) are applied , for intersection, composition and contraction of intervals. Specifically, the context of formal software verification is used to get variable domain reduction in the preprocessing of programs by formal verification to prove, through Satisfiability Modulo Theories (SMT), the satisfiability or not from the Boolean formula that represents all states of the program. Therefore, it was used. the formal method of bounded model checking (Bounded Model Checking - BMC), which checks in k steps whether a given property is satisfiable or, if not, provides a counterexample. A BMC preprocessing strategy, using programs modeled by CSP/CP and with solutions estimated by an interval contraction algorithmic technique, is presented. Computational experiments were carried out using program benchmarks in C, Java and Kotlin programming languages, and using the ESBMC solver (and ESBMC-Jimple, developed in the SWPERFI UFAM-MOTOROLA PD\&I Project, of which this research is also part) and others. The results indicate that, in many cases, there is a significant reduction in the domain of variables, influencing the reduction of the exponential search space for state verification which, consequently, promotes a reduction in program verification time, showing the suitability of the proposed strategy. Furthermore, the method was also used to detect software vulnerabilities, specifically those that may involve operations with arithmetic intervals, achieving satisfactory results for most of the vulnerability categories used. FAPEAM - Fundação de Amparo à Pesquisa do Estado do Amazonas 2025-01-29T15:28:17Z 2024-03-27 Dissertação DEVEZA, Jessé de Souza. 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. 2024. 62 f. Dissertação (Mestrado em Informática) - Universidade Federal do Amazonas, Manaus (AM), 2024. https://tede.ufam.edu.br/handle/tede/10636 por Acesso Aberto https://creativecommons.org/licenses/by-nc-nd/4.0/ application/pdf Universidade Federal do Amazonas Instituto de Computação Brasil UFAM Programa de Pós-graduação em Informática
institution	TEDE - Universidade Federal do Amazonas
collection	TEDE-UFAM
language	por
topic	CIENCIAS EXATAS E DA TERRA: CIENCIA DA COMPUTACAO Aritmética Intervalar ESBMC-Jimple Programação por Restrições Verificação Formal de Software Verificação de Modelo Limitado Vulnerabilidades
spellingShingle	CIENCIAS EXATAS E DA TERRA: CIENCIA DA COMPUTACAO Aritmética Intervalar ESBMC-Jimple Programação por Restrições Verificação Formal de Software Verificação de Modelo Limitado Vulnerabilidades Deveza, Jessé de Souza 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
topic_facet	CIENCIAS EXATAS E DA TERRA: CIENCIA DA COMPUTACAO Aritmética Intervalar ESBMC-Jimple Programação por Restrições Verificação Formal de Software Verificação de Modelo Limitado Vulnerabilidades
description	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.
author_additional	Rodrigues, Rosiane de Freitas
author_additionalStr	Rodrigues, Rosiane de Freitas
format	Dissertação
author	Deveza, Jessé de Souza
author2	http://lattes.cnpq.br/0610645582446597
author2Str	http://lattes.cnpq.br/0610645582446597
title	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
title_short	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
title_full	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
title_fullStr	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
title_full_unstemmed	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
title_sort	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
publisher	Universidade Federal do Amazonas
publishDate	2025
url	https://tede.ufam.edu.br/handle/tede/10636
_version_	1831970407560773632
score	11.753735

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

Registros relacionados