3 ms·

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 proc

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.

anon6362 2y ago
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.
quantumgarbage 2y ago
A seamless, drop-in replacement, for all python users is actually a pretty good feat tbh
nine_k 2y ago
> just another wrapped C library. I suppose you mean "just another top-notch library available in the Python ecosystem"? :)
bolognafairy 2y ago
What part of how this is being conveyed do you disagree with? Specifically. This isn’t a language war.
- neuroelectron 2y ago
  The headline makes it sound like it was written in Python which is a lot more readable than 15,000 lines of C
  - frumplestlatz 2y ago
    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://fstar-lang.org - https://github.com/FStarLang/karamel https://github.com/FStarLang/karamel - https://github.com/hacl-star/hacl-star https://github.com/hacl-star/hacl-star
    - myko 2y ago
      This is fantastic. Somewhere my CS prof is smiling
    - wepple 2y ago
      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?
      - aw1621107 2y ago
        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 https://arxiv.org/pdf/1703.00053
        wepple 2y ago
        Thanks! Looks hefty but I’ll try give it a crack
nxpnsv 2y ago
How is that bad in any way?

anon6362 2y ago

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.

quantumgarbage 2y ago

A seamless, drop-in replacement, for all python users is actually a pretty good feat tbh

nine_k 2y ago

> just another wrapped C library. I suppose you mean "just another top-notch library available in the Python ecosystem"? :)

bolognafairy 2y ago

What part of how this is being conveyed do you disagree with? Specifically. This isn’t a language war.

neuroelectron 2y ago
The headline makes it sound like it was written in Python which is a lot more readable than 15,000 lines of C
- frumplestlatz 2y ago
  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://fstar-lang.org - https://github.com/FStarLang/karamel https://github.com/FStarLang/karamel - https://github.com/hacl-star/hacl-star https://github.com/hacl-star/hacl-star
  - myko 2y ago
    This is fantastic. Somewhere my CS prof is smiling
  - wepple 2y ago
    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?
    - aw1621107 2y ago
      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 https://arxiv.org/pdf/1703.00053
      - wepple 2y ago
        Thanks! Looks hefty but I’ll try give it a crack

nxpnsv 2y ago

How is that bad in any way?