Beyond Testing: Improving Safety and Security through Static Analysis - Pascal Kesseli

Pascal started his research in static analysis at the University of Oxford in 2013, where he explored automated generation of provably correct programs and refactorings in Java and C/C++. Since then Pascal has worked for a variety of companies creating developer tools which focus on improving the safety and security of programs, as well as entirely automating tedious tasks away for developers.
Bugs and security vulnerabilities in computer programs stretch as far back as the field itself. Software errors cause billions of dollars in damage every year, and in critical environments they even put national security and people's lives at risk. Most developers are familiar with testing and fuzzing techniques to try and mitigate these issues but are of course also aware of these approaches' limitations.
In this talk we go one step beyond testing and take a deep dive into the state of the art of model checking and static analysis for C and C++. We explore how these tools work and how they can identify high-impact bugs and security vulnerabilities early, and even outright prove the safety and correctness of critical systems. The talk also includes practical demos of open-source tools used by companies like Microsoft, Meta and Amazon, and how these tools can be leveraged by any project or company with elevated security and safety requirements.
#cpp #cbmc #zurich