Security and Privacy of Distributed Software Systems
Name of applicant
Simon Oddershede Gregersen
Title
Postdoctoral Fellow
Institution
New York University
Amount
DKK 1,020,000
Year
2023
Type of grant
Internationalisation Fellowships
What?
To ensure that software systems are secure and privacy-preserving, it is appealing to mathematically prove their correctness. However, existing tools for verification of such properties cannot be used to verify many modern systems of interest as they are distributed and perform randomized operations. This project will develop a new framework that will allow us to formally verify such systems.
Why?
Software is intertwined with all aspects of our lives, and security and privacy breaches pose enormous costs and risks. Developing secure software is a substantial challenge: small errors can undermine security, with exploits targeting everything from protocol vulnerabilities down to floating point rounding errors, and testing is inadequate for guaranteeing the absence of such errors.
How?
This project will develop mathematical tools that can be used to formally verify that software systems are secure and privacy-preserving by constructing mathematical proofs that the system is always well-behaved. In particular, we will develop a new so-called separation logic that supports probabilistic reasoning about distributed systems as needed to verify modern software systems.