Zobrazeno 1 - 10
of 22
pro vyhledávání: '"Jonathan Protzenko"'
Autor:
Jonathan Protzenko, Son Ho
Publikováno v:
Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, 2022, 6 (ICFP), pp.711-741. ⟨10.1145/3547647⟩
Proceedings of the ACM on Programming Languages, 2022, 6 (ICFP), pp.711-741. ⟨10.1145/3547647⟩
We present Aeneas, a new verification toolchain for Rust programs based on a lightweight functional translation. We leverage Rust’s rich region-based type system to eliminate memory reasoning for a large class of Rust programs, as long as they do n
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::bccfa28d928c2941ece976a71309f2c4
Autor:
Ravi Ramamurthy, Johannes Gehrke, Nikhil Swamy, Jonathan Protzenko, Arvind Arasu, Tahina Ramananandro, Min Xu, Esha Ghosh, Donald Kossmann, Badrish Chandramouli, Srinath Setty, Alexander van Renen, Aseem Rastogi
Publikováno v:
SIGMOD Conference
We present FastVer, a high-performance key-value store with strong data integrity guarantees. FastVer is built as an extension of FASTER, an open-source, high-performance key-value store. It offers the same key-value API as FASTER plus an additional
Autor:
Jonathan Protzenko, Itsaka Rakotonirina, Jay Bosamiya, Yi Zhou, Joseph Lallemand, Antoine Delignat-Lavaud, Bryan Parno, Tahina Ramananandro, Cédric Fournet
Publikováno v:
IEEE Symposium on Security and Privacy
Drawing on earlier protocol-verification work, we investigate the security of the QUIC record layer, as standardized by the IETF in draft version 30. This version features major differences compared to Google’s original protocol and early IETF draf
Autor:
Nikhil Swamy, Antoine Delignat-Lavaud, Jonathan Protzenko, Joonwon Choi, Bryan Parno, Christoph M. Wintersteiger, Chris Hawblitzel, Aseem Rastogi, Natalia Kulatova, Aymeric Fromherz, Marina Polubelova, Santiago Zanella-Béguelin, Tahina Ramananandro, Karthikeyan Bhargavan, Benjamin Beurdouche, Cédric Fournet
Publikováno v:
SP 2020-IEEE Symposium on Security and Privacy
SP 2020-IEEE Symposium on Security and Privacy, May 2020, San Francisco / Virtual, United States. pp.983-1002, ⟨10.1109/SP40000.2020.00114⟩
IEEE Symposium on Security and Privacy
2020 IEEE Symposium on Security and Privacy (SP)
SP 2020-IEEE Symposium on Security and Privacy, May 2020, San Francisco / Virtual, United States. pp.983-1002, ⟨10.1109/SP40000.2020.00114⟩
IEEE Symposium on Security and Privacy
2020 IEEE Symposium on Security and Privacy (SP)
International audience; We present EverCrypt: a comprehensive collection of verified, high-performance cryptographic functionalities available via a carefully designed API. The API provably supports agility (choosing between multiple algorithms for t
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b754b12d09129b9fb446c4bb80a284b0
https://inria.hal.science/hal-03154278
https://inria.hal.science/hal-03154278
Publikováno v:
IEEE Symposium on Security and Privacy
SP 2019-40th IEEE Symposium on Security and Privacy
SP 2019-40th IEEE Symposium on Security and Privacy, May 2019, San Francisco, United States. pp.1256-1274, ⟨10.1109/SP.2019.00064⟩
2019 IEEE Symposium on Security and Privacy (SP)
SP 2019-40th IEEE Symposium on Security and Privacy
SP 2019-40th IEEE Symposium on Security and Privacy, May 2019, San Francisco, United States. pp.1256-1274, ⟨10.1109/SP.2019.00064⟩
2019 IEEE Symposium on Security and Privacy (SP)
International audience; After suffering decades of high-profile attacks, the need for formal verification of security-critical software has never been clearer. Verification-oriented programming languages like F * are now being used to build high-assu
Autor:
Jonathan Protzenko
Publikováno v:
IWIL@LPAR
We present the proof search monad, a set of combinators that allows one to write a proof search engine in a style that resembles the formal rules closely. The user calls functions such as premise, prove or choice; the library then takes care of gener
Publikováno v:
ACM Conference on Computer and Communications Security (CCS)
ACM Conference on Computer and Communications Security (CCS), Oct 2017, Dallas, United States
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security -CCS '17
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security-CCS 17
CCS
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security
ACM Conference on Computer and Communications Security (CCS), Oct 2017, Dallas, United States
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security -CCS '17
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security-CCS 17
CCS
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security
International audience; HACL* is a verified portable C cryptographic library that implements modern cryptographic primitives such as the ChaCha20 and Salsa20 encryption algorithms, Poly1305 and HMAC message authentication, SHA-256 and SHA-512 hash fu
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d62cf6cf20db7d98bd926288eeef8e93
https://hal.inria.fr/hal-01588421v2/document
https://hal.inria.fr/hal-01588421v2/document
Autor:
Aseem Rastogi, Cédric Fournet, Karthikeyan Bhargavan, Santiago Zanella-Béguelin, Tahina Ramananandro, Cătălin Hriţcu, Jean Karim Zinzindohoue, Antoine Delignat-Lavaud, Nikhil Swamy, Jonathan Protzenko, Peng Wang
Publikováno v:
Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2017, 1 (ICFP), pp.17:1--17:29. ⟨10.1145/3110261⟩
Proceedings of the ACM on Programming Languages, 2017, 1 (ICFP), pp.17:1--17:29. ⟨10.1145/3110261⟩
22nd International Conference on Functional Programming
Proceedings of the ACM on Programming Languages, ACM, 2017, 1 (ICFP), pp.17:1--17:29. ⟨10.1145/3110261⟩
Proceedings of the ACM on Programming Languages, 2017, 1 (ICFP), pp.17:1--17:29. ⟨10.1145/3110261⟩
22nd International Conference on Functional Programming
We present Low*, a language for low-level programming and verification, and its application to high-assurance optimized cryptographic libraries. Low* is a shallow embedding of a small, sequential, well-behaved subset of C in F*, a dependently-typed v
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::08bf5be5baf6171ffa0a43f50c049e47
https://hal.archives-ouvertes.fr/hal-01672706
https://hal.archives-ouvertes.fr/hal-01672706
Autor:
Jean Karim Zinzindohoue, Markulf Kohlweiss, Aseem Rastogi, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy, Jianyang Pan, Jonathan Protzenko, Karthikeyan Bhargavan, Santiago Zanella-Béguelin
Publikováno v:
Delignat-Lavaud, A, Fournet, C, Kohlweiss, M, Protzenko, J, Rastogi, A, Swamy, N, Béguelin, S Z, Bhargavan, K, Pan, J & Zinzindohoue, J K 2017, Implementing and Proving the TLS 1.3 Record Layer . in 2017 IEEE Symposium on Security and Privacy, SP 2017, San Jose, CA, USA, May 22-26, 2017 . Institute of Electrical and Electronics Engineers (IEEE), San Jose, CA, USA, pp. 463-482, 2017 IEEE Symposium on Security and Privacy, San Jose, CA, United States, 22/05/17 . https://doi.org/10.1109/SP.2017.58
2017 IEEE Symposium on Security and Privacy (SP)
SP 2017-38th IEEE Symposium on Security and Privacy
SP 2017-38th IEEE Symposium on Security and Privacy, May 2017, San Jose, United States. pp.463-482, ⟨10.1109/SP.2017.58⟩
IEEE Symposium on Security and Privacy
2017 IEEE Symposium on Security and Privacy (SP)
SP 2017-38th IEEE Symposium on Security and Privacy
SP 2017-38th IEEE Symposium on Security and Privacy, May 2017, San Jose, United States. pp.463-482, ⟨10.1109/SP.2017.58⟩
IEEE Symposium on Security and Privacy
The record layer is the main bridge between TLS applications and internal sub-protocols. Its core functionality is an elaborate form of authenticated encryption: streams of messages for each sub-protocol (handshake, alert, and application data) are f
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7648b940afdc8afbf8352d1c015115b0
https://www.pure.ed.ac.uk/ws/files/55275610/Implementing_and_Proving_the_TLS_1.3_Record_Layer.pdf
https://www.pure.ed.ac.uk/ws/files/55275610/Implementing_and_Proving_the_TLS_1.3_Record_Layer.pdf
Publikováno v:
ACM Transactions on Programming Languages and Systems (TOPLAS)
ACM Transactions on Programming Languages and Systems (TOPLAS), 2016, 38 (4), pp.94. ⟨10.1145/2837022⟩
ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2016, 38 (4), pp.94. ⟨10.1145/2837022⟩
ACM Transactions on Programming Languages and Systems (TOPLAS), 2016, 38 (4), pp.94. ⟨10.1145/2837022⟩
ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2016, 38 (4), pp.94. ⟨10.1145/2837022⟩
International audience; The programming language Mezzo is equipped with a rich type system that controls aliasing and access to mutable memory. We give a comprehensive tutorial overview of the language. Then, we present a modular formalization of Mez
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::172bbed05c3b9f0823c4b3b374f64f2f
https://inria.hal.science/hal-01246534/file/bpp-mezzo-journal.pdf
https://inria.hal.science/hal-01246534/file/bpp-mezzo-journal.pdf