Teaching and researching formal semantics of functional programming languages, while looking for ways of solving complex, practical problems with formal methods in order to create trustworthy tools for the Erlang programmer. Truly enthusiastic about formally verified static analysis and code refactoring.
Something to love about the BEAM is the principle of ‘let it crash’: exceptions are isolated and handled by design. Indeed, various kinds of data checks can be mercifully omitted, but it would be rash to conclude that all input validation is redundant and unnecessary. In 2020, the Erlang Ecosystem Foundation curated an extensive list of secure coding principles to raise programmers’ awareness and assist them in creating secure Erlang systems. But the reality is always messy: Erlang/Elixir projects rarely follow these guidelines, and legacy have been running for years with well-known vulnerabilities. In this talk, we will explain how static analysis can be useful for detecting critical security issues in new or legacy Erlang code bases, mitigating and even eliminating them semi-automatically. In particular, we will present use cases of vulnerabilities found in open-source projects and demonstrate how techniques like data-flow analysis can reveal and cure them.