Symbolic Automata for Analysing String Manipulating Programs

Mnoho aplikací přijímá, odesílá a zpracovává data v textové podobě. Správné a bezpečné zpracování těchto dat je typicky zajištěno tzv. ošetřením řetězců (string sanitization). Pomocí metod formální verifikace je možné analyzovat takovéto operace s řetězci a prověřit, zda jsou správně navržené či implementované. Naším cílem je vytvořit obecný nástroj pro analýzu systémů jejichž konfigurace lze kódovat pomocí slov z vhodné abecedy, a také jeho specializaci pro analýzu programů pracujících s řetězci. Nejprve jsou popsaný konečné automaty a převodníky a poté různé třídy a podtřídy symbolických převodníků, zejména pak jejich omezení. Na základě těchto informací je pak pro použití v analýze programů navržen nový typ symbolických převodníků. Dále je popsán regulární model checking, speciálně pak jeho variantu založenou na abstrakci automatů, tzv. ARMC, u kterého je známo že dokáže velmi úspěšně překonat problém stavové exploze u automatů a umožňuje nám tzv. dosáhnout pevného bodu v analýze. Poté je navržena vlastní analýza programů psaných v imperativním paradigmatu, a to zejména programů manipulujících s řetězci, založená na principech ARMC. Následuje popis vlastní implementace nástroje s důrazem na jeho praktické vlastnosti. Rovněž jsou popsaný důležité části knihovny AutomataDotNet, na které nástroj staví. Práci je uzavřena diskuzí experimentů s nástrojem provedených na příkladech z knihovny LibStranger. Many software applications receive, send and process data in a text form. Correct and safe processing of these data is usually ensured by so-called string sanitization. With the help of methods of formal verification, we can analyse these string operations and check whether they are correctly designed and implemented. The goal of this work is to create a tool for analysis of systems whose configurations can be encoded as words over a suitable alphabet, as well as its specialization for analysing string manipulating programs. First, we describe finite automata and transducers in general and characterize various classes and sub-classes of symbolic transducers, especially their limitations. Based on this study, a new class of symbolic transducers is proposed for use in the program analysis. Later, we introduce regular model checking, especially its variant based on abstraction over automata, the so called ARMC, which was proved to be able to quite successfully fight the state explosion problem in the size of the automata and allows us to reach a fix-point. We then design an analysis of programs written in imperative languages, especially those that manipulate strings, using the principles of ARMC. Finally, the implementation of the tool is presented, highlighting its practical aspects and discussing relevant parts of AutomataDotNet library it is based on. The work completes debating the experimental evaluation of the tool using test inputs from LibStranger project.