Název: Statická analýza programů pracujících s dynamickou pamětí s využitím separační logiky
Překlad názvu: Static Analysis of Heap-Manipulating programs using Separation Logic
Autoři: Brablec, Tomáš ; Rogalewicz, Adam (oponent) ; Dacík, Tomáš (vedoucí práce)
Typ dokumentu: Bakalářské práce
Rok: 2025
Jazyk: eng
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [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.
Klíčová slova: Astral; Frama-C; KTSN; separation logic; static analysis; SV-COMP; verification; Astral; Frama-C; KTSN; separační logika; statická analýza; SV-COMP; verifikace

Instituce: Vysoké učení technické v Brně (web)
Informace o dostupnosti dokumentu: Plný text je dostupný v Digitální knihovně VUT.
Původní záznam: https://hdl.handle.net/11012/253189

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-683807


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Vysoké učení technické v Brně
Vysokoškolské kvalifikační práce > Bakalářské práce