TY - THES TI - Symbolické automaty v analýze programů s řetězci TT - Symbolic Automata for Analysing String Manipulating Programs AU - Kotoun, Michal AB - 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.  AB - 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. UR - http://hdl.handle.net/11012/194969 UR - http://www.nusl.cz/ntk/nusl-433553 A2 - Vojnar, Tomáš A2 - Rogalewicz, Adam LA - eng KW - symbolic finite automata KW - finite automata KW - finite transducer application KW - abstraktní regulární model checking KW - aplikace konečných převodníků KW - symbolic finite transducers KW - konečné převodníky KW - regulární model checking KW - formal verification KW - ASMA KW - formální verifikace KW - abstract regular model checking KW - konečné automaty KW - regular model checking KW - AutomataDotNet KW - symbolické konečné automaty KW - string analysis KW - symbolické konečné převodníky KW - CEGAR KW - LibStranger KW - finite transducers KW - analýza řetězců PY - 2020 PB - Vysoké učení technické v Brně‎, Antonínská 548/1, 601 90 Brno, http://www.vutbr.cz/ ER -