Jonathan Protzenko

We have more post-docs in Azure Research! Consider applying to in Systems & Security (lnkd.in/e-mp63GV) or in AI Security & Privacy (lnkd.in/e5H5Gybt).

Quick reminder that I'm co-chairing VSTTE with @AzaleaRaad this year, and submission deadline is in just a few days!! vstte2024.hotcrp.com/u/2/

@djco *clone

@djco For now, you can close the repository and directly use the package here: github.com/hacl-star/hacl… relying on path dependencies in your cargo file: #specifying-path-dependencies" target="_blank" rel="nofollow noopener">doc.rust-lang.org/cargo/referenc…

HACL*, the verified crypto library, now available as pure, safe Rust: jonathan.protzenko.fr/2024/03/20/hac… -- alpha release.

@djco This will eventually be distributed as part of libcrux which I believe will have all of the bells and whistles like proper packaging and documentation.

@_protz_ Are you publishing this to crates.io or, failing that, do you have a self-hosted copy of the rustdoc?

@BRIAN_____ @cryptopathe I think that’s one of the conclusions of the Kyber experiment by @_franziskus_ and Goutam. Most of it is pure state-passing yet ends up delivering the same performance anyhow.

@_protz_ @cryptopathe Interesting. That seems to imply that we don’t need to support the in-place form for many operations. I think that it is worth considering adding an in-place-or-disjoint slice type to Rust. Rust Crypto and *ring* have both had to create it, mixed up w/ MaybeUninit for disjoint.

New blog post! I share plans to modernize HACL* by bringing it to a pure, safe Rust world. I also talk about a new backwards-compat tool, Eurydice, for new verified Rust code that still needs to exist in legacy C environments. jonathan.protzenko.fr/2024/01/05/eur…

@BRIAN_____ @cryptopathe Yes we need something general because sometimes indices are indeed non constant but still relatable to each other, e.g. f() and f()+4

@_protz_ @cryptopathe And is the reason you are doing the split_at stuff because of the non-constant indexes? I would have expected slice pattern matching could be used for the cases where the indexes are known at compile time, at least.

@BRIAN_____ @cryptopathe Yes we haven’t observed anything meaningful in terms of perf. Even cases where it got faster (perhaps because the callee is a local function and never receives aliased arguments anymore).

@_protz_ @cryptopathe Does the `let dst_copy = copy dst` end up getting optimized away?

@lastland0 Please get in touch with @sonmarcho and I!

Another amazing endeavour of nimble compilation to connect proofs, programs and languages together, by my esteemed PhD advisor!

Just made the repository public: github.com/AeneasVerif/eu…

It was an absolute pleasure to be here and I had a blast! Thanks for the invitation, it was an honor to be in such great company.

Super excited to have @_protz_ visiting @NUSComputing and giving an invited talk on formally verified cryptography and security protocols!

here we go! This month we will meet one week early on Jan. 22 to hear @_protz_ talk about HACL-Rust and Eurydice. Make sure to join us! eventbrite.com/e/modernizing-…

Had a great time doing a keynote at @ProssimoISRG on Microsoft approach to memory safety. Made a huge announcement - @microsoft is going big on Rust and spending $10 million to make it 1st class language in our engineering systems + $1 million @rustlang foundation. #memorysafety

I was very happy to give a talk at Galois to present the latest progress on Aeneas, our framework to verify Rust programs. On the menu: latest features, future extensions, ongoing verification effort, and most of all demo of the Lean backend! galois.com/blog/2023/10/a…

Our quantum-resistant protocol upgrade, PQXDH, is now “the first machine-checked post-quantum security proof of a real-world cryptographic protocol.” Thanks to the researchers who did this important formal verification! Read more from them here👇 cryspen.com/post/pqxdh

A new paper called "Comparse: Provably Secure Formats for Cryptographic Protocols" is out! eprint.iacr.org/2023/1390 A few explanations below. 🧵