CAREER: Verifying Security and Privacy of Distributed Applications

Developing secure software systems is challenging because even small bugs can undermine the security of a system. One approach to reduce the incidence of bugs in software is known as formal verification, in which a developer constructs a mathematical proof that the software follows an intended specification. Yet existing tools for formal verification cannot be applied to establish the security and privacy of many applications. The reason is that these applications combine three challenging features and requirements: (1) concurrency, in which multiple computer systems interact at once, (2) fault-tolerance, meaning that systems must handle failures and crashes, and (3) randomization, in which programs generate and use random data to achieve security properties. Existing tools for formal verification only support a subset of these features. The project's novelty is a new approach to formal verification of systems that combines all three of these features, thereby enabling the verification of security and privacy properties of important applications. The project's impacts are in improving the reliability and correctness of secure software systems. In addition, the primary investigator is developing new teaching materials on verification of security and privacy properties of randomized systems. The technical approach is based on a new method for reasoning about randomized systems called asynchronous couplings. This method allows one to prove that two randomized programs behave in equivalent ways, even when the two programs generate random samples at different times and locations. The primary investigator is developing a new logic for program verification that combines asynchronous couplings with recently developed techniques for reasoning about distributed, fault-tolerant systems based on concurrent separation logic. The resulting logic is extensible, in the sense that higher-level techniques for proving security and privacy properties can be encoded in the logic. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.