Verified Authentication for NSF Large Facilities

This project will enable trusted computing for flagship cyberinfrastructures (e.g., Laser Interferometer Gravitational-Wave Observatory (LIGO), Open Science Grid) and their vibrant scientific communities that use SciTokens. The expected advances Verified Authentication 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 is correct. We are exploring the use of functional/array based languages for concise and mathematically correct descriptions of complex authorization scopes.