Sound Static Analysis

You are maybe already familiar with static analyzers, such as SpotBugs (formerly FindBugs), but these popular analyzers tend to focus on bug patterns. Sound static analysis is a slightly different beast. It is far more interesting because the results are as reliable as mathematical proofs! The NIST report on Dramatically Reducing Software Vulnerabilities emphasizes the need for sound analysis and explains the distinction neatly: "Heuristic analysis is faster than sound analysis, but lacks assurance that comes from a chain of logical reasoning".

Learning to develop and effectively apply sound static analyzers is much more difficult than just writing bug patterns. This is, however, a skill that is increasingly sought after. All the big silicon valley companies are growing their static analysis teams. The following is an example of the requirements for a Static Analysis Engineering job at Facebook. In order effectively develop an analyzer, one needs to master both typed functional programming (OCaml) as well as the semantics of the target language (C/C++).

These skills are not just important for Facebook; these are critical skills to improve software quality in Estonia as well. There are scholarships available to students willing to invest the time necessary to master static analysis engineering.

Together with the Technical University of Munich, we develop a sound static analyzer, Goblint, which is architecturally very similar to Facebook's analyzer. We have started a new analyzer, Põder, which is written in Scala and analyzes JVM bytecode. By working on the following topics, you will learn to develop and apply sound static analyzers.

Towards Security Analysis with Goblint

Goblint is a general static analysis framework. The analysis engine is capable of simulating program execution. On top of this, one can implement specific analyses that check specific properties. The goal of this thesis is to focus on the Juliet test suite. This work requires being able to run our analyzers on these benchmark suites and identify failing test cases. You will then work with us to implement the necessary analysis to achieve better results on these benchmarks. It suffices to focus on a single class of security vulnerabilities and implement a well-known analysis.

Competing with Goblint at the SV-COMP verification contest

The SV-COMP verification contest is a competition between static analyzers. The goal of this thesis is to get Goblint to compete there with decent results! This will require you to understand their rules and the understand their exchange format for witnesses. You will then need to program Goblint to output witnesses. Generating counter-example witnesses for Goblint can be very difficult, but your task is not to win the contest. To begin with, we just need to produce syntactically correct witnesses.

Interactive Static Assertion Checking for JVM bytecode

One of the problems with sound analysis is that it assumes worst possible behavior from unknown events. In reality, there are often informal assumptions on how systems are used, so the developer needs to interact with the analyzer. The first step towards sound interactive analysis is to implement on-demand assertion checking in the Põder framework. You will first just flag warnings on locations that the static analyzer fails to prove the assertion, and then, you will work towards inferring preconditions for the correctness of these assertions. The goal is to invent novel ways of allowing interaction with the application developer to rule out warnings via meaningful annotations rather than suppressing false alarms.