sl plug: We're working on this using F* (https://fstar-lang.org/ ) as part of https://project-everest.github.io/ . Also applies to TLS msgs.
-
-
-
I know. It's on my TODO list to contact y'all about trying to collaborate in some way, as our interests overlap considerably!
-
One issue is that in webpki I'm trying, for now at least, to avoid any memory allocation during cert. parsing & verification.
-
This is also our concern, though we can prove memory safety. No reason why it shouldn't work with static or preallocated bufs.
End of conversation
New conversation -
-
-
IIUC, that's for a different but related thing: protocol. Not sure how I would apply it to parsig/building/verifying cert chains.
End of conversation
New conversation
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.