Divide, Conquer and Verify: Improving Symbolic Execution Performance
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2023
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866914057599057920 |
|---|---|
| author | Scherb, Christopher Heitz, Luc Bryan Grieder, Hermann Mattmann, Olivier |
| author_facet | Scherb, Christopher Heitz, Luc Bryan Grieder, Hermann Mattmann, Olivier |
| contents | Symbolic Execution is a formal method that can be used to verify the behavior of computer programs and detect software vulnerabilities. Compared to other testing methods such as fuzzing, Symbolic Execution has the advantage of providing formal guarantees about the program. However, despite advances in performance in recent years, Symbolic Execution is too slow to be applied to real-world software. This is primarily caused by the \emph{path explosion problem} as well as by the computational complexity of SMT solving. In this paper, we present a divide-and-conquer approach for symbolic execution by executing individual slices and later combining the side effects. This way, the overall problem size is kept small, reducing the impact of computational complexity on large problems. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2310_03598 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Divide, Conquer and Verify: Improving Symbolic Execution Performance Scherb, Christopher Heitz, Luc Bryan Grieder, Hermann Mattmann, Olivier Cryptography and Security Symbolic Computation Systems and Control Symbolic Execution is a formal method that can be used to verify the behavior of computer programs and detect software vulnerabilities. Compared to other testing methods such as fuzzing, Symbolic Execution has the advantage of providing formal guarantees about the program. However, despite advances in performance in recent years, Symbolic Execution is too slow to be applied to real-world software. This is primarily caused by the \emph{path explosion problem} as well as by the computational complexity of SMT solving. In this paper, we present a divide-and-conquer approach for symbolic execution by executing individual slices and later combining the side effects. This way, the overall problem size is kept small, reducing the impact of computational complexity on large problems. |
| title | Divide, Conquer and Verify: Improving Symbolic Execution Performance |
| topic | Cryptography and Security Symbolic Computation Systems and Control |
| url | https://arxiv.org/abs/2310.03598 |