2 papers
cs.CR2026
GCD: Garbled, Corrected, Demonstrandum -- Fixing and Proving Go's Extended GCD Implementation
Linard Arquint
We verify the 'extendedGCD' implementation in Go's standard library ('crypto/internal/fips140/bigmod'), which plays a crucial role in the generation of RSA key pairs. Even though t…
cs.CR2025
The Secrets Must Not Flow: Scaling Security Verification to Large Codebases (extended version)
Linard Arquint, Samarth Kishor, Jason R. Koenig +3
Existing program verifiers can prove advanced properties about security protocol implementations, but are difficult to scale to large codebases because of the manual effort require…