Security of String Programs via Automata
Školitel: prof. Ing. Tomáš Vojnar, Ph. D.
Instituce: Brno University of Technology, Faculty of Information Technology
Obor: Computer Science and Engineering
O mém projektu
One of the major problems of software development are security vulnerabilities and one of the main sources of these are string manipulating programs such as web applications. Formal verification based on string solving (reasoning about constraints over string variables) has recently shown a great potential to facilitate automated analysis of such programs. The string solving methods based on finite automata seem to have the best potential: automata technology provides a favorable ratio of efficiency, generality, and completness guarantees in reasoning about strings in such applications. The topic of my dissertation will therefore be improvement of the underlying automata methods and their application in verification of software, with a strong focus on real world string manipulating programs. In my master's thesis I have already done the first steps in this direction by combining abstract interpretation approach to verification with an algorithm for testing emptiness of alternating automata. The combination has shown a great potential to facilitate efficient string solving. My research will therefore start by optimizing the implementation, experimenting with design decisions of the approach and searching for other heuristics for effective treatment of automata. We will then work on enriching automata based implementations of string constraint languages so that they could provide expresiveness needed in verification of string manipulating programs. Ultimately, our automata and string constraint solving technology will be integrated in security checking tools for string manipiulating programs and possibly tools for other related verfification problems (e.g. for programs with arrays or pointers).