CAREER: Verifying Security and Privacy of Distributed Applications

职业：验证分布式应用程序的安全性和隐私

• 批准号: 2338317
• 负责人: Joseph Tassarotti
• 金额: $ 60万
• 依托单位: New York University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2024
• 资助国家: 美国
• 起止时间: 2024-05-01 至 2029-04-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2338317&HistoricalAwards=false
• 关键词: CAREER; Verifying; Security; Privacy; Distributed

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.

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