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

该项目将为旗舰网络基础设施(例如激光干涉仪引力波天文台(LIGO)、开放科学网格、极端科学和工程发现环境(XSEDE))及其充满活力的科学界提供可信计算。该项目的创新之处在于：1)引入支持验证的语言，提供严格的数学证明，证明现有的联邦认证实现(CILogon，SciTokens)是正确的；2)使严格的验证成为发展分布式计算科学不可或缺的一部分。正确实施基于令牌的身份验证协议的问题对于使全球机构、行业合作伙伴和政府机构的研究人员能够安全协作至关重要。例如，SciTokens运营一个复杂的基础设施来管理互联网工程任务组(IETF)标准的短期OAuth令牌，以实现分布式计算环境中的零信任数据访问和作业执行。该项目的影响是减少人工测试可能遗漏的代价高昂的生产阶段错误。该项目将促进对可能暴露我国网络基础设施骨干的隐藏错误的了解，从而提高研究安全性。该项目汇集了：i)Dafny等具有验证意识的语言，ii)网络计算系统中的联合身份验证领域，以及iii)一个由来自500个组织(包括国际和美国)的20,000名研究人员组成的大型科学社区。他们每天都在使用本网站。我们的支持验证的SciTokens项目的预期进展将是：a)连续自动推理(验证)算法，它发现SciTokens代码中的关键错误；b)基于令牌的认证实现的认证证明是正确的；以及c)正确应用的合成：从Dafny中定义的单一规范到多种编程语言(例如，GO、Java、PHP)，以将经过广泛验证的SciTokens集成到不同的系统和网络中。该项目的技术方法是在Dafny实现Science Tokens的关键认证功能，该功能使用Hoare逻辑来提供Science Tokens协议的数学证明，并自动生成正确的代码，例如，授权范围，有多种语言版本。初步结果显示，在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.