Thesis topics from Vesal Vojdani

Applied Automated Software Verification

There are many highly sophisticated automated software verifiers, such as those competing at the International Contest on Software Verification, but applying these advanced methods on real-world programs to obtain high signal has proven challenging. To make the software more safe and secure would be how to apply these tools in the real world. I have a couple of ideas in this direction:

BSc:

  1. CoOpeRace: Cooperative Race Detection as a Service. This is a grand idea inspired by the CoVeriTeam Service with a focus on the specifics of comparing race detection results. [One student working on the framework side of this, but topics are possible on how to achieve true cooperation between the tools.]
  2. Evaluating Sound Static Analyzers. It's not so clear what various static analyzers can do. The SAMATE project at NIST aims to evaluate and showcase tools. It would be great to create a simpler and more user-friendly introduction to their work. Try running goblint on their suite, and possibly, generalize the method so that any automated verifier at SV-COMP could run on the SAMATE Ockham evaluation criteria for sound analyzers.
  3. Case Studies on Real-World Security Vulnerability Detection. For a genuinely high-impact thesis, you may try to use Goblint on the Linux kernel or OpenSSL. Consider a version where a known vulnerability has been found and help us get goblint to identify the vulnerability without emitting too many false positives.

MSc:

  1. Analyzing Linux Device Drivers. Analyzing Linux device drivers is particularly interesting but also very challenging. We want to analyze each driver separately, so this requires modelling the environment (creating a so called harness that simulates how the kernel invokes the driver). There is a heavy-weight system for this (klever), but we would prefer a simpler system tailor-made for our analyzer. The goal would be to focus on a subset of simple drivers, such as character drivers, in order to be able to analyze these precisely enough to detect real-world vulnerabilities and verify their patches.

Automaadid, keeled ja translaatorid (AKT)

(The following BSc topics are in Estonian because the course is in Estonian).

BSc:

  • Eetikatestide uurimine ja arendamine
  • AKT keelest LLVM baitkoodi genereerimine
  • CMa simulaatori (VAM) veebiversiooni loomine
  • AKT keelele lisada turvalise andmevoo tüübid
  • Erinevad silmaringimaterjalid AKT või Tarkvara turvalisuse kursuse jaoks: automaatverifitseerijate demode loomine. AKT keele jaoks implementeerida lihtsustatud versioon SV-COMP töövahenditest: