15,000 lines of verified cryptography now in Python
a year ago
- #Python
- #HACL
- #cryptography
- Python now includes 15,000 lines of verified cryptographic code from HACL*.
- The transition to HACL* was seamless for users, with no loss of functionality.
- HACL* implemented new features to meet Python's requirements, including additional Blake2 modes and a new SHA3 API.
- The project took 2.5 years and involved contributions from multiple developers.
- Streaming APIs in cryptography are complex and were a key focus for verification.
- Verified code handles various cryptographic algorithms' unique requirements, such as block processing and state management.
- Build issues, like AVX2 compatibility, were addressed through refactoring and abstract struct patterns.
- Memory allocation failures are now properly propagated in the verified code.
- The integration demonstrates the maturity of verified cryptographic code for real-world use.