Cryptography in SPARK: building the foundation with constant-time bigints

Constant-time big integer libraries are specialized tools designed to execute operations in a time that does not vary with the input values, thereby preventing side-channel attacks like timing attacks. They are foundational in cryptography, where maintaining consistent operation timing and memory access is crucial to ensuring secure key management and protecting sensitive data from exploitation.

In this talk, I will present my partially formally verified implementation of a “bigint” library in SPARK. I will show how it is implemented and how to use it. I will also share my experience writing this library as a newcomer to the Ada/SPARK ecosystem.