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

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

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.