Evaluation of sat solvers and bit-blasting to challenges numerical bugs in programs

Evaluation of SAT Solvers and Bit-Blasting to challenges numerical bugs in programs

Réf ABG-126867
Stage master 2 / Ingénieur
Durée 6 mois
Salaire net mensuel 630€

13/11/2024

David Defour
Lieu de travail
Perpignan Occitanie France
Champs scientifiques
* Informatique
* Mathématiques
Mots clés
Bit Blasting, SAT Solver, Polynomial evaluation, IEEE754
Date limite de candidature
01/02/2025


Description


Introduction

Numerical problems often involve finding inputs that lead to specific desired outputs. Traditionally, these problems are solved using numerical methods, approximations, or optimization techniques. However, in numerical computation, where the representation of numbers is done in finite precision (i.e., binary), there arises an opportunity to employ combinatorial techniques to search for specific bit patterns in inputs and outputs.

Bit blasting, a technique used in formal verification, translates a problem into a Boolean formula that can be solved by SAT solvers. In recent years, SAT solvers have shown great success in solving complex combinatorial problems. The ability of bit blasting to handle large, complex numerical problems in a bitwise manner can potentially open new avenues for generating inputs that exhibit specific bit patterns.

This thesis aims to explore the feasibility of using bit blasting, in combination with SAT solvers, to solve numerical problems where specific bit patterns are required in both the inputs and the outputs of a given formula. The primary focus will be on polynomial evaluations where the coefficients are fixed, and specific bit patterns are imposed on both the input and output. This exploration could lead to new methods of finding challenging numerical examples and counterexamples in areas such as cryptography, number theory, or formal verification.


2. Problem Statement and Research Objectives

The goal of this research is to investigate whether bit blasting, paired with modern SAT solvers, can be effectively used to find numerical inputs that yield specific bit patterns in their outputs. The objectives of this thesis are:

* Bit Blasting for Polynomial Evaluation: Investigate how polynomial evaluation problems can be represented using bit blasting. Start with simple polynomials and gradually increase the complexity by adding more variables and higher-degree polynomials.
* SAT Solver Integration: Use modern SAT solvers to solve the bit-blasted Boolean formulas and find numerical solutions that exhibit specific bit patterns in their binary representation.
* Performance Evaluation: Evaluate the performance of SAT solvers in terms of time complexity and resource utilization for solving these problems and compare various solvers for this class of problem. Measure the scalability of the approach by varying the bit-width, polynomial degree, and input-output bit pattern constraints.
* Challenging Problem Generation: Investigate whether this approach can be used to generate challenging numerical problems, such as finding inputs that lead to outputs with rare or predefined bit patterns such as hard-to-round cases (i.e. Table Maker’s Dilemma).


3. Literature Review

The literature on SAT solvers and bit-blasting spans several decades, with applications ranging from hardware verification to software model checking. This section will focus on foundational work in SAT solving, recent advancements in bit-blasting techniques, and their use in program verification.

* SAT Solvers and Bit-Blasting:
o Overview of SAT solver algorithms (DPLL, CDCL) and their evolution.
o Examination of bit-blasting as a technique for converting high-level arithmetic and logical operations into SAT problems.
o Insights from SAT competitions and performance benchmarks to understand the current state-of-the-art in SAT solver efficiency.
* Formal Verification with SAT Solvers:
o Applications of SAT solvers in software verification and bug detection.
o Comparative analysis of SAT-based formal methods versus symbolic execution and model checking.
o Case studies where SAT solvers were successfully used in discovering software bugs (e.g., integer overflow detection, buffer overflows, race conditions).
* Challenges and Limitations:
o Known challenges with bit-blasting, including formula size explosion and solver performance degradation in large or complex software systems.
o Discussion of trade-offs between precision and efficiency when using SAT solvers and bit-blasting for bug detection.


4. Methodology

* Experimental Setup:
o Selection of target SAT solvers, including but not limited to Z3, MiniSAT, and CryptoMiniSat.
o Development of an encoding pipeline to convert high-level formulae into bit-level representations suitable for SAT solving.
* Polynomial Representation:
o Start by representing simple polynomials (e.g., linear, quadratic) as Boolean formulas using bit-blasting techniques. Each variable and constant will be represented in binary, and operations like multiplication and addition will be converted into their Boolean equivalents.
* Bit-Blasting Process:
o Solve the Boolean formulas generated by the bit blasting. The solver will output bit vectors that satisfy both the polynomial equation and the bit pattern constraints.
* Performance Evaluation:
o Measure and compare SAT solver performance under various conditions while focusing on time to solution, memory usage, scalability, against satisfiability to unsatisfiability constraints.
* Optimization Techniques:
o Explore optimization methods for reducing the complexity of the SAT problem generated by bit-blasting on this class of problem (i.e. Techniques such as abstraction, formula simplification, and lazy bit-blasting).


5. Expected Contributions

* A clear methodology for representing numerical problems (polynomial evaluation) as Boolean formulas using bit blasting.
* Insights into the effectiveness of SAT solvers for finding numerical solutions that exhibit specific bit patterns.
* A better understanding of the strengths and limitations of using bit blasting and SAT solvers for generating challenging numerical solutions.
* Potential extensions of this approach to other domains, such as cryptography and number theory.


Profil

The candidate should demonstrate skills or, at a minimum, a strong interest in software development, complexity analysis, SAT Solver, and computer arithmetic.


Prise de fonction

01/02/2025
#J-18808-Ljbffr