FMitF: Track II: Bringing Verification-Aware Languages and Federated Authentication to Enable Secure Computing for Scientific Communities

FMITF：轨道 II：引入验证感知语言和联合身份验证，为科学界提供安全计算

• 批准号: 2319190
• 负责人: Phuong Cao
• 金额: $ 10万
• 依托单位: University of Illinois at Urbana-Champaign
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-08-01 至 2025-01-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2319190&HistoricalAwards=false
• 关键词: FMitF; Track; II; Bringing; Verification

This project will enable trusted computing for flagship cyberinfrastructures (e.g., Laser Interferometer Gravitational-Wave Observatory (LIGO), Open Science Grid, Extreme Science and Engineering Discovery Environment (XSEDE)) and their vibrant scientific communities. The project’s novelties are to: 1) bring verification-aware languages to provide rigorous mathematical proofs that existing federated authentication implementations (CILogon, SciTokens) are correct, and 2) make rigorous verification an integral part of developing distributed computational science. The problem of correctly implementing token-based authentication protocols is critical to enable researchers across global institutions, industrial partners, and government agencies to collaborate safely. For example, SciTokens operates a sophisticated infrastructure to manage Internet Engineering Task Force (IETF)-standard, short-lived OAuth tokens to enable zero-trust data access and job execution in distributed computing environments. The project’s impact is to reduce costly production-stage bugs that may be missed by manual testing. The project will advance the knowledge of hidden bugs that could expose the backbone of our nation’s cyberinfrastructures, thereby advancing research security.This project brings together: i) verification-aware languages such as Dafny, ii) the field of federated authentication in networked computing systems, and iii) a large scientific community of 20,000 researchers from 500+ organizations (both international and from the U.S.) who use SciTokens daily. The expected advances of our Verification-aware SciTokens project will be: a) continuous automated reasoning (verification) algorithm that uncovers critical bugs in SciTokens code, b) certification proof that a token-based authentication implementation is correct, and c) synthesis of correct applications: from a single specification defined in Dafny into a variety of programming languages (e.g., Go, Java, PHP) to broadly integrate Verified SciTokens into different systems and networks.The project's technical approach is implementing critical authentication functions of SciTokens in Dafny, which provides the mathematical proof of SciTokens’s protocol using Hoare logic and automatically generates correct code, e.g., authorization scopes, in multiple languages. Preliminary results show that two critical bug classes have been discovered in SciTokens: timing-based and access control logic bugs.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.

该项目将为旗舰网络基础设施（例如激光干涉仪重力波动台（LIGO），开放科学网格，极端科学与工程发现环境（XSEDE）及其充满活力的科学社区提供信任的计算。该项目的新颖性是：1）携带验证意识的语言，以提供严格的数学证据，证明现有的联合身份验证实现（Cilogon，Scitokens）是正确的，而2）将严格的验证成为开发分布式计算科学不可或缺的一部分。正确实施基于令牌的身份验证协议的问题对于使全球机构，工业合作伙伴和政府机构的研究人员能够安全合作至关重要。例如，Scitokens操作一个复杂的基础架构来管理Internet工程工作组（IETF）标准，短暂的OAuth代币，以在分布式计算环境中启用零信任数据访问和工作执行。该项目的影响是减少可能通过手动测试遗漏的昂贵的生产阶段错误。该项目将促进可能暴露国家网络基础架构的骨干的隐藏错误的知识，从而提高研究安全性。本项目汇集了：i）验证 - 意识到的语言，例如达夫尼，ii）ii）在网络计算系统中的联合身份验证领域，以及iii的20,000个研究者（均来自500多个组织）的大型科学界（来自500多个组织）（来自国际范围）。我们的验证知识项目的预期进步将是：a）持续自动推理（验证）算法，该算法会发现scitokens代码中关键的错误，b）认证证明，基于令牌的身份验证实施是正确的，以及c）正确的应用程序的合成：从dafny中定义为dafny over opermage（E. e. e。将经过验证的Scitokens集成到不同的系统和网络中。该项目的技术方法是在DAFNY中实施Scitokens的关键身份验证功能，该功能使用Hoare Logic提供了Scitokens协议的数学证明，并自动生成正确的代码，例如，以多种语言为单位。初步结果表明，在Scitokens：基于计时和访问控制逻辑错误中已经发现了两个关键的错误类别。该奖项反映了NSF的法定任务，并使用基金会的知识分子优点和更广泛的影响评估标准，通过评估被认为是珍贵的支持。