Symbolické automaty v analýze programů s řetězci
| Autor: | Kotoun, Michal |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
symbolic finite automata
finite automata finite transducer application abstraktní regulární model checking aplikace konečných převodníků symbolic finite transducers konečné převodníky regulární model checking formal verification ASMA formální verifikace abstract regular model checking konečné automaty regular model checking AutomataDotNet symbolické konečné automaty string analysis symbolické konečné převodníky CEGAR LibStranger finite transducers analýza řetězců |
| Druh dokumentu: | masterThesis |
| Popis: | 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. |
| Databáze: | Networked Digital Library of Theses & Dissertations |
| Externí odkaz: |
|