<vbmithr>
I know a guy from the team, Pierre Yves Strub
<hannes>
vbmithr: an amazing piece of work in my opinion
<hannes>
(we used it as inspiration for ocaml-tls every now and then :)
<vbmithr>
Do you take inspiration from it for your caml tls impl ?
<vbmithr>
ok
<vbmithr>
Would it be possible to translate it into ocaml ?
<hannes>
I would not know the answer to your question
<hannes>
we actually came across it when we already had a big chunk of tls written down, thus we did not bother to trying to automatically translate it
<NoNNaN>
hannes: is other ocaml submission are available too ?
<hannes>
NoNNaN: not that I know of
<vbmithr>
cool, thanks!
<NoNNaN>
hannes: do you have any plan for provable security properties ? (protocol states, ordering, etc)
<hannes>
NoNNaN: I'm not a cryptographer. I think mitls already does a great job at verifying the cryptographic security of TLS.
thomasga has quit [Quit: Leaving.]
<def`>
hannes: do you have any idea about how to prove correctness of your ocaml code?
<hannes>
def`: depends on what the specification for "correctness" is ;)
<NoNNaN>
eg.: a high level protocol specification, something like in mltls
<def`>
hannes: right :)
<def`>
first that the api is safe to use, then that it is actually TLS that is spoken, then maybe implementation details like robustness against timing attack
<hannes>
NoNNaN: their lemmas are about cryptographic security afaics ; and they prove them using their code (which basically is a 'high-level protocol specification')
<NoNNaN>
and they use dependent types (F7) to prove it
<hannes>
def`: a) should be done by interop-tests imho (with other stacks) b) well, proving anything to be 'robust against timing (or more general side channels)' -- I've not seen this at all..
<hannes>
NoNNaN: yes, but the proofs (afaics) are solely on the cryptographic level, not functional correctness
<NoNNaN>
you could later probably use fstar (f7 successor, recently open sourced), with mapping from ocaml types to fstar types
<def`>
hannes: ok, so there are no place for formal methods in your approach
<def`>
(which is ok :), just different from mitls)
<hannes>
(I mean - don't get me wrong - I did formal verification in my PhD - and am interested in applying them to TLS! but atm I'm struggling with what the specification should be ;)
<def`>
hannes: hmm, this could have broader implications that just providing a tls implementation
<def`>
interesting :)
<hannes>
[and if you have any further ideas regarding specifications, I'm happy to hear / discuss :)]
<hannes>
def`: in my opinion there is a big lack of a TLS 'test suite' -- I mean this is a protocol used since 15 years. most widely used cryptographic protocol. and nevertheless there is no test suite available!?
djs55 has quit [Quit: Leaving.]
mort___ has joined #mirage
mort___ has quit [Ping timeout: 252 seconds]
thomasga has joined #mirage
<vbmithr>
Camlp4: Uncaught exception: DynLoader.Error ("/usr/lib/ocaml/sexplib/pa_sexp_conv.cma", "interface mismatch on Cam
<vbmithr>
lp4_import")
<vbmithr>
Does it rings something ? (when trying to install ocaml-ipaddr
<vbmithr>
mmh, I think I know. Dependency problem.
djs55 has joined #mirage
thomasga has quit [Quit: Leaving.]
amirmc has joined #mirage
djs55 has quit [Quit: Leaving.]
amirmc has quit [Quit: Leaving.]
tlockney_away is now known as tlockney
djs55 has joined #mirage
thomasga has joined #mirage
<jonludlam>
djs55, am I taking you or anil to the hackathon tonight?
rgrinberg has joined #mirage
djs55 has quit [Quit: Leaving.]
amirmc has joined #mirage
amirmc has quit [Client Quit]
philtor has joined #mirage
boogie has quit [Remote host closed the connection]
boogie has joined #mirage
philtor_ has joined #mirage
rgrinberg1 has joined #mirage
rgrinberg has quit [Ping timeout: 265 seconds]
djs55 has joined #mirage
<djs55>
jonludlam: nope we're going to the hackathon first thing tomorrow am
dsheets has quit [Ping timeout: 265 seconds]
djs55 has quit [Quit: Leaving.]
philtor_ has quit [Ping timeout: 264 seconds]
dsheets has joined #mirage
rgrinberg1 has quit [Quit: Leaving.]
philtor has quit [Ping timeout: 240 seconds]
NoNNaN has quit [Remote host closed the connection]
NoNNaN has joined #mirage
cr409 has quit [Ping timeout: 252 seconds]
rgrinberg has joined #mirage
NoNNaN has quit [Quit: []]
philtor_ has joined #mirage
djs55 has joined #mirage
avsm has joined #mirage
<thomasga>
dsheets: recursive stores are almost there
<dsheets>
thomasga, yay! v exciting
<dsheets>
i'm struggling with an odd functor type error just now but think i'll resume in the morning
<thomasga>
(and I'm following your advice to store some kind of resolver in the final nodes, with explicit boundary gaps)
<thomasga>
that's quite elegant I'd say, now need to find a nice way to expose that to the user
<dsheets>
in the final ones?
<dsheets>
i think the symlink idea is solid
<dsheets>
and readlink will let them discover wth is going on
<avsm>
rgrinberg: that's the greatest patchset ive seen in ages. zero-copy parsing for cohttp would speed it up massively!
<rgrinberg>
avsm: is it a such a big deal anymore? we barely use re anyway
<rgrinberg>
i recall for cookies and content types
<rgrinberg>
i guess we could it bring it back if it's 0 copy
<avsm>
sort of — we use it in a few places, and that's enough to trigger a bigarray->string copy
<avsm>
which is frustrating, since in mirage we have this nice, careful zero copy stack that uses bigarrays. until http, and then everything descends into copying chaos
<avsm>
with re supporting bigarray (and therefore making cstruct's regexable), we could scan in place
dsheets has quit [Ping timeout: 240 seconds]
<avsm>
but iirc, the other possible issue is detecting when the regexp tries to scan out of bound, and blocking on a Lwt thread
<avsm>
needs to be restartable for that
<rgrinberg>
yeah that last use case would need a new interface I think