Description

Sanitizers are programs that remove unwanted characters from a given input. They are often used in order to prevent injection attacks such as SQL injection and XSS. It is therefore very important that we can check if the sanitizer is correctly implemented.

To do this, one can use an active learning algorithm which learns the behavior of a program by observing the input and output to a system. There exists an algorithm that derives automata, specifically Symbolic Finite Transducers, from sanitizers. This automaton describes how the sanitizer transforms the input into the corresponding output. In order to check whether this learned model, which represents the sanitizer, is correct, we compare the learned model to a specification (also in the form of a Symbolic Finite Transducer).

However, writing such specifications takes quite some time. Therefore, we propose to automatically generate specifications (based on some user input). In this project, we would like you to investigate what types of specifications can be automatically generated and implement the generation of these specifications.

Tasks:

1. Understand the SFT learning algorithm
2. Investigate what types of specifications can be automatically generated
3. Make a program that automatically generates the specifications

References

1. Final paper (Digital version available here)