3 ms·

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

by bolognafairy 1y ago

neuroelectron 1y 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 1y 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 1y ago
    This is fantastic. Somewhere my CS prof is smiling
  - wepple 1y 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 1y 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 1y ago
        Thanks! Looks hefty but I’ll try give it a crack

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

neuroelectron 1y 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 1y 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 1y ago
  This is fantastic. Somewhere my CS prof is smiling
- wepple 1y 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 1y 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 1y ago
      Thanks! Looks hefty but I’ll try give it a crack