|
|
|
|
|
| author: |
Sophie Lathouwers |
| title: |
Formal Verification of Sanitizers |
| keywords: |
sanitizers |
| topics: |
Other
|
| committee: |
Marieke Huisman
,
Maarten Everts
|
| started: |
January 2018 |
| end: |
September 2018 |
Abstract
| Nowadays, most applications are developed to be deployed to the web. These web applications can be accessed by many users, including malicious users who try to attack them. In order to defend against attacks such as SQL injections and XSS, many web applications use sanitizers. Sanitizers will modify a given input so as to remove the presence of dangerous characters. It is, however, very difficult to write correct sanitizers. And reasoning about the correctness of any program tends to be very difficult, especially if the program is quite large. Fortunately, sanitizers are generally small pieces of code due to which it is possible to reason about their correctness. In this research, we present a method to reason about the correctness of sanitizer implementations by comparing them to specifications. This method learns models, symbolic finite transducers, in a black-box manner, which describe the behaviour of the sanitizers. These models are compared to specified models in order to find erroneous behaviour of sanitizer implementations. The learning algorithm and ability to compare models have all been implemented in a tool called SFTLearning. Using SFTLearning, we were able to derive models from real-world sanitizers and reason about their correctness. |
References
-
Thesis
(Digital version available here)
|
Back to University of Twente portal
