CAREER: Verifying Security and Privacy of Distributed Applications

开发安全的软件系统是一项挑战，因为即使是很小的错误也会破坏系统的安全性。一种减少软件中错误发生率的方法被称为形式验证，其中开发人员构建了一个数学证明，证明软件遵循预期的规范。 然而，现有的正式验证工具不能应用于建立许多应用程序的安全性和隐私。原因是这些应用结合了联合收割机三个具有挑战性的特征和要求：（1）并发性，其中多个计算机系统同时交互，（2）容错性，这意味着系统必须处理故障和崩溃，以及（3）随机性，其中程序生成并使用随机数据来实现安全属性。现有的正式验证工具只支持这些功能的一个子集。 该项目的新奇是一种新的系统形式化验证方法，结合了所有这三个功能，从而能够验证重要应用程序的安全性和隐私性。 该项目的影响是提高安全软件系统的可靠性和正确性。 此外，主要研究人员正在开发新的教学材料的安全性和隐私属性的随机系统的验证。技术方法是基于一种新的方法来推理随机系统称为异步耦合。这种方法允许证明两个随机化程序以等效的方式行为，即使这两个程序在不同的时间和位置生成随机样本。主要研究人员正在开发一种新的逻辑程序验证，结合异步耦合与最近开发的技术推理分布式，容错系统的基础上并发分离逻辑。由此产生的逻辑是可扩展的，在这个意义上，更高层次的技术，证明安全和隐私属性可以编码在逻辑中。这个奖项反映了NSF的法定使命，并已被认为是值得通过评估使用基金会的知识价值和更广泛的影响审查标准的支持。

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.