5 ms·
Can anyone comment on how this implementation of TLS compares to the recent ocaml/mirageOS version? How much does formal verification matter/increase confidenc
by rudenoise 10y ago
Can anyone comment on how this implementation of TLS compares to the recent ocaml/mirageOS version?
How much does formal verification matter/increase confidence?
Is the rust version easier to integrate with other stacks?
https://mirage.io/blog/why-ocaml-tls https://mirage.io/blog/why-ocaml-tls
- hannob 10y agoNeither ocaml-tls nor this new one do formal verification. The only TLS library that does so is miTLS.
- nickpsecurity 10y agoLet's not forget the security kernel in Guttman's cryptlib. It's like a lightweight variant of formal verification that justs makes sure things interface correctly.
- strmpnk 10y agoWhich is interating here since F* can extract to OCaml. I wonder how hard it would be to wire up a test harness to compare the two with randomized tests.
- jeffdavis 10y agoOCaml has more runtime requirements. Can someone comment on how invasive those requirements are, and whether that would limit adoption of the OCaml version compared with C or rust?
- edraferi 10y agoIs that still true in MirageOS, which runs as a Unikernel on top of Xen?