Original title: Statická analýza programů pracujících s dynamickou pamětí s využitím separační logiky
Translated title: Static Analysis of Heap-Manipulating programs using Separation Logic
Authors: Brablec, Tomáš ; Rogalewicz, Adam (referee) ; Dacík, Tomáš (advisor)
Document type: Bachelor's theses
Year: 2025
Language: eng
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [eng] [cze]
Tato práce představuje statický analyzátor KTSN zaměřený na verifikaci bezpečnosti práce s pamětí programů v jazyce C. Naše metoda se soustředí na programy, které pracují s lineárními seznamy. Náš analyzátor je schopen verifikovat správnost manipulace s dynamicky alokovanou pamětí a detekovat neplatné dereference ukazatelů (např. use-after-free), úniky paměti a další chyby. Náš přístup je založen na analýze toku dat a využívá separační logiku pro reprezentaci abstraktních stavů paměti. Nástroj je implementovaný ve frameworku Frama-C. Analýza využívá dedikovaný solver Astral pro rozhodování separační logiky založený na překladu do SMT. Nástroj KTSN byl otestován na podmnožině SV-COMP benchmarků zaměřené na lineární seznamy a porovnán s dalšími verifikačními nástroji ve své kategorii. Přestože nedosahuje úrovně nejlepšího nástroje PredatorHP, překonává většinu verifikačních nástrojů v této kategorii, včetně analyzátoru EVA, který je součástí frameworku Frama-C. Naše metoda rovněž vykazuje potenciál pro integraci do analyzátoru EVA, čímž by se výrazně vylepšila analýza lineárních seznamů ve Frama-C. This thesis introduces the KTSN static analyzer that aims to verify the memory safety of C programs. The method focuses on programs that manipulate linked lists. Our tool is able to prove the correctness of handling dynamically allocated memory and detect invalid pointer dereferences such as use-after-free, memory leaks, and other bugs. The approach is based on dataflow analysis, and it uses separation logic to represent abstract memory states. The analysis uses Astral, a dedicated solver for SL based on translation to SMT. KTSN is implemented as a plugin to the Frama-C framework. The tool was tested on the linked lists subset of the SV-COMP benchmarks and compared to other verification tools. While it does not reach the top competitor, PredatorHP, it outperforms most verifiers in this category, including EVA, a value analyzer of Frama-C. Thus, our method shows promise of integration into EVA, greatly improving the analysis of linked lists in Frama-C.
Keywords: Astral; Frama-C; KTSN; separační logika; statická analýza; SV-COMP; verifikace; Astral; Frama-C; KTSN; separation logic; static analysis; SV-COMP; verification

Institution: Brno University of Technology (web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library.
Original record: https://hdl.handle.net/11012/253189

Permalink: http://www.nusl.cz/ntk/nusl-683807


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Bachelor's theses