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

Abstract

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.