Security and Privacy of Distributed Software Systems

Navn på bevillingshaver

Simon Oddershede Gregersen


Postdoctoral Fellow


New York University


DKK 1,020,000




Internationalisation Fellowships


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.


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.


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.

Tilbage til oversigtssiden