Verifying Information Security for Concurrent Programs
Project Leader: Toby Murray
Staff: Gidon Ernst
Collaborators: Robert Sison (UNSW) Kai Engelhardt (UNSW) Heiko Mantel (TU Darmstadt) Daniel Schoepe (Chalmers University of Technology) Andrei Sabelfeld (Chalmers University of Technology)
Sponsors: Defence Science and Technology Group, US Office of Naval Research
Primary Contact: Toby Murray (email@example.com)
Keywords: computer security; program verification; programming languages
Disciplines: Computing and Information Systems
Software guards our secrets. Indeed, your web browser knows every password you enter online. Modern software is inherently concurrent: your web browser runs many programs at once, at least one for each website you visit. Yet there are no generally applicable methods to conclude that a concurrent program won't leak its secrets. This project will build on recent advances to develop them for the first time. Its success will lead to entirely novel ways to develop new software that is guaranteed to keep its secrets, while allowing insecurity in existing software to be conclusively diagnosed and fix.
We will build program logics that allow one to prove that a concurrent program does not leak its secrets, and to conduct this proof by reasoning over each of the program's individual components (i.e. threads of execution) separately.