|
|
Symbolic Automata for Analysing String Manipulating Programs
Kotoun, Michal ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
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.
|
|
|
Symbolic Automata for Analysing String Manipulating Programs
Kotoun, Michal ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
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.
|
host ::
RSS.