2019
[15] EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider (, , , , , , , , , , , , , , ) Cryptology ePrint Archive: Report 2019/757 .
[14] EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats (, , , , , , ) In Proceedings of the 28th USENIX Security Symposium . (To Appear)
[13] Dijkstra Monads for All (, , , , , , ), In 24th ACM SIGPLAN International Conference on Functional Programming (ICFP), . (To Appear) [bibtex] [pdf]
[12] Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms (, , , , , , , , , , , , ), In 28th European Symposium on Programming (ESOP), Springer, . [bibtex] [pdf] [doi]
[11] Formally Verified Cryptographic Web Applications in WebAssembly (, , , ), In 2019 IEEE Symposium on Security and Privacy (SP), . [bibtex] [pdf] [doi]
[10] Wys*: A DSL for Verified Secure Multi-party Computations (, , ), In 8th International Conference on Principles of Security and Trust (POST) (Flemming Nielson, David Sands, eds.), Springer, volume 11426, . [bibtex] [pdf] [doi]
[9] A Verified, Efficient Embedding of a Verifiable Assembly Language (, , , , , ) In Proceedings of the Symposium on Principles of Programming Languages (POPL) .
2018
[8] Recalling a Witness: Foundations and Applications of Monotonic State (, , , , , ), In PACMPL, volume 2(POPL), . [bibtex] [pdf]
[7] A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations (, , , , , , , , , ), In The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, . [bibtex] [pdf]
2017
[6] HACL*: A Verified Modern Cryptographic Library (, , , ) In Proceedings of the ACM Conference on Computer and Communications Security (CCS) .
[5] Vale: Verifying High-Performance Cryptographic Assembly Code (, , , , , , , , ) In Proceedings of the USENIX Security Symposium (Distinguished Paper Award) .
[4] Implementing and Proving the TLS 1.3 Record Layer (, , , , , , , , , ) In 38th IEEE Symposium on Security and Privacy, IEEE Computer Society 2017. . [bibtex] [pdf]
[3] Everest: Towards a Verified, Drop-in Replacement of HTTPS (, , , , , , , , , , , , , , , , , , , , , ) In Proceedings of the Summit on Advances in Programming Languages (SNAPL). .
[2] Verified Low-Level Programming Embedded in F* (, , , , , , , , , , ), In PACMPL, volume 1(ICFP), . [bibtex] [pdf] [doi]
[1] Dijkstra Monads for Free (, , , , , , , ), In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), . [bibtex] [pdf]