Reading the article, they took a verified C library generated from F* from Microsoft, vendored the code in CPython and wrote a C extension.
And during the process they discovered that the original library did not handle allocation failures?
What is the big deal about Python here? It's just another wrapped C library.
A seamless, drop-in replacement, for all python users is actually a pretty good feat tbh
In general, it's good practice to use best components available, regardless of source. Cryptographic components especially shouldn't be DIY.
It would be cool if Ruby did something similar for stdlib/openssl, but it could be also be done in a gem too.
How is that bad in any way?
> just another wrapped C library.
I suppose you mean "just another top-notch library available in the Python ecosystem"? :)
What part of how this is being conveyed do you disagree with? Specifically.
This isn’t a language war.
The headline makes it sound like it was written in Python which is a lot more readable than 15,000 lines of C
The 15k lines of C are generated. The implementations are written in (and formally verified using) F*, and then the C is generated from the F* code using KaRaMeL.
One should be able to trust the proofs of correctness and never look at (or maintain) the generated C directly.
- https://fstar-lang.org
- https://github.com/FStarLang/karamel
- https://github.com/hacl-star/hacl-star
I’m not a verification expert - do we know or assume that the F* to C compiler preserves the verified code completely? And doesn’t introduce issues?
This paper [0] linked in the KaRaMeL repo claims to provide the proof you're looking for:
> Verified Low-Level Programming Embedded in F∗
> We present Low∗, a language for low-level programming and verification, and its application to high-assurance optimized cryptographic libraries. Low∗ is a shallow embedding of a small, sequential, well-behaved subset of C in F∗, a dependently-typed variant of ML aimed at program verification. Departing from ML, Low∗ does not involve any garbage collection or implicit heap allocation; instead, it has a structured memory model à la CompCert, and it provides the control required for writing efficient low-level security-critical code.
> By virtue of typing, any Low∗ program is memory safe. In addition, the programmer can make full use of the verification power of F∗ to write high-level specifications and verify the functional correctness of Low∗ code using a combination of SMT automation and sophisticated manual proofs. At extraction time, specifications and proofs are erased, and the remaining code enjoys a predictable translation to C. We prove that this translation preserves semantics and side-channel resistance.
[0]: https://arxiv.org/pdf/1703.00053
This is fantastic. Somewhere my CS prof is smiling