Formal Methods based on Abstract Interpretation and Symbolic – Execution for Vulnerability Detection Tools

This course introduces formal methods for building and evaluating vulnerability detection tools, bridging concepts from abstract interpretation (AI) and symbolic execution (SE). It covers foundational theory, including program semantics, soundness, and completeness, to understand issues of static analyzers and concepts like false positives and negatives in security. The course explores abstract interpretation and symbolic execution and examines practical, state-of-the-art tools based on taint-tracking, like Pysa (AI-based) and Pysta (SE-based), focusing on how they
identify vulnerabilities, handle data flow (sources and sinks), and mitigate the common problem of false results. Exercises include the understanding of common security vulnerabilities such as XSS for web applications and how they can be identified by the techniques described by the theory of the course.