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

该项目将为旗舰网络基础设施（如激光干涉仪引力波天文台（LIGO）、开放科学网格、极端科学与工程发现环境（XSEDE））及其充满活力的科学社区提供可信计算。该项目的新颖之处在于：1)引入验证感知语言来提供严格的数学证明，证明现有的联邦身份验证实现（CILogon、SciTokens）是正确的；2)使严格的验证成为开发分布式计算科学的一个组成部分。正确实施基于令牌的身份验证协议的问题对于使全球机构、工业合作伙伴和政府机构的研究人员能够安全协作至关重要。例如，SciTokens操作一个复杂的基础设施来管理Internet工程任务组（IETF）标准的短期OAuth令牌，以在分布式计算环境中实现零信任数据访问和作业执行。该项目的影响是减少手工测试可能遗漏的昂贵的生产阶段错误。该项目将促进对可能暴露我国网络基础设施骨干的隐藏漏洞的了解，从而提高研究安全性。该项目汇集了：i)验证感知语言（如Dafny）， ii)网络计算系统中的联合身份验证领域，以及iii)每天使用SciTokens的来自500多个组织（包括国际和美国）的20,000名研究人员的大型科学社区。我们的验证感知SciTokens项目的预期进展将是：a)发现SciTokens代码中的关键错误的连续自动推理（验证）算法，b)基于令牌的身份验证实现是正确的认证证明，以及c)正确应用程序的合成：从Dafny定义的单一规范到各种编程语言（例如，Go, Java， PHP），以广泛地将经过验证的SciTokens集成到不同的系统和网络中。该项目的技术方法是在Dafny中实现SciTokens的关键身份验证功能，该功能使用Hoare逻辑提供SciTokens协议的数学证明，并自动生成正确的代码，例如多种语言的授权范围。初步结果表明，在SciTokens中发现了两类关键的错误：基于时间的错误和访问控制逻辑错误。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.