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

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.