The Reducing Software Vulnerability Project (RSVP@Tartu)
How much more needless suffering before we take software quality seriously?
- Rocket exploding because preconditions were unspecified? ✓
- Complete internet security collapse due to a missing array bounds check? ✓
- Global ransomware epidemic due to buggy input validation? ✓
With the rising threats of state-sponsored hacking, the consequences are even more severe. A key message of the 2016 Federal Cybersecurity R&D Strategic Plan is the need to reverse the adversaries' asymmetric advantage: It is currently easier for a malicious actor to exploit a software vulnerability than for the software vendor to develop and deploy patches to all vulnerable systems. Our only hope is to avoid vulnerabilities in the first place. The call is out for a dramatic reduction in software vulnerabilities. We are responding to this call---what about you?
Assuming you want to prevent the next wave ransomware attacks, how can you help? The National Institute of Standards and Technology (NIST) have answered this question in their report "Dramatically Reducing Software Vulnerabilities" Of the five approaches they highlight, our main focus is on formal methods. These include all software analysis approaches based on mathematics and logic.
Research that dramatically reduces software vulnerabilities
| Goblint | Alvor | JVM Security Analyzer | ||
|---|---|---|---|---|
| A static analysis tool for multi-threaded C based on the theory of abstract interpretation. | A static validator of SQL statements embedded in Java based on abstract GLR parsing. | We are currently developing a security analyzer for JVM bytecode. |
Courses that dramatically reduce software vulnerabilities
You can learn the foundations of formal methods in our formal methods course. We also promote microservice architecture and domain-specific frameworks within our functional programming courses.
| 
| 
| ||
| Formal Methods with Isabelle/HOL | Functional Programming | PL Seminar: Static Analysis |
|---|