Security and Privacy of Distributed Software Systems
Navn på bevillingshaver
Simon Oddershede Gregersen
Titel
Postdoctoral Fellow
Institution
New York University
Beløb
DKK 1,020,000
År
2023
Bevillingstype
Internationalisation Fellowships
Hvad?
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.
Hvorfor?
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.
Hvordan?
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.