Search Results

Documents authored by Bhargavan, Karthikeyan

Document
DOI: 10.4230/DagRep.13.3.1
Foundations of WebAssembly (Dagstuhl Seminar 23101)

Authors: Karthikeyan Bhargavan, Jonathan Protzenko, Andreas Rossberg, and Deian Stefan

Published in: Dagstuhl Reports, Volume 13, Issue 3 (2023)

Abstract
WebAssembly (Wasm) is a new portable code format with a formal semantics whose popularity has been growing fast, as a platform for new application domains, as a target for compilers and languages, and as a subject of research into its semantics, its performance, and its use in building verified and secure systems. This Dagstuhl Seminar brought together leading academics and industry representatives currently involved in the design, implementation and formal study of Wasm, to exchange ideas around topics such as formal methods for, verified compilation to, and verified implementation of Wasm.
Cite as

Karthikeyan Bhargavan, Jonathan Protzenko, Andreas Rossberg, and Deian Stefan. Foundations of WebAssembly (Dagstuhl Seminar 23101). In Dagstuhl Reports, Volume 13, Issue 3, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{bhargavan_et_al:DagRep.13.3.1,
  author =	{Bhargavan, Karthikeyan and Protzenko, Jonathan and Rossberg, Andreas and Stefan, Deian},
  title =	{{Foundations of WebAssembly (Dagstuhl Seminar 23101)}},
  pages =	{1--16},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2023},
  volume =	{13},
  number =	{3},
  editor =	{Bhargavan, Karthikeyan and Protzenko, Jonathan and Rossberg, Andreas and Stefan, Deian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.3.1},
  URN =		{urn:nbn:de:0030-drops-192255},
  doi =		{10.4230/DagRep.13.3.1},
  annote =	{Keywords: Compilation, Formal methods, Programming languages, Verification, Virtual machines, WebAssembly}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSTTCS.2019.1
Practical Formal Methods for Real World Cryptography (Invited Talk)

Authors: Karthikeyan Bhargavan and Prasad Naldurg

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)

Abstract
Cryptographic algorithms, protocols, and applications are difficult to implement correctly, and errors and vulnerabilities in their code can remain undiscovered for long periods before they are exploited. Even highly-regarded cryptographic libraries suffer from bugs like buffer overruns, incorrect numerical computations, and timing side-channels, which can lead to the exposure of sensitive data and long-term secrets. We describe a tool chain and framework based on the F* programming language to formally specify, verify and compile high-performance cryptographic software that is secure by design. This tool chain has been used to build a verified cryptographic library called HACL*, and provably secure implementations of sophisticated secure communication protocols like Signal and TLS. We describe these case studies and conclude with ongoing work on using our framework to build verified implementations of privacy preserving machine learning software.
Cite as

Karthikeyan Bhargavan and Prasad Naldurg. Practical Formal Methods for Real World Cryptography (Invited Talk). In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 1:1-1:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bhargavan_et_al:LIPIcs.FSTTCS.2019.1,
  author =	{Bhargavan, Karthikeyan and Naldurg, Prasad},
  title =	{{Practical Formal Methods for Real World Cryptography}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{1:1--1:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.1},
  URN =		{urn:nbn:de:0030-drops-115632},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.1},
  annote =	{Keywords: Formal verification, Applied cryptography, Security protocols, Machine learning}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2017.1
Everest: Towards a Verified, Drop-in Replacement of HTTPS

Authors: Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jianyang Pan, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, and Jean-Karim Zinzindohoué

Published in: LIPIcs, Volume 71, 2nd Summit on Advances in Programming Languages (SNAPL 2017)

Abstract
The HTTPS ecosystem is the foundation on which Internet security is built. At the heart of this ecosystem is the Transport Layer Security (TLS) protocol, which in turn uses the X.509 public-key infrastructure and numerous cryptographic constructions and algorithms. Unfortunately, this ecosystem is extremely brittle, with headline-grabbing attacks and emergency patches many times a year. We describe our ongoing efforts in Everest (The Everest VERified End-to-end Secure Transport) a project that aims to build and deploy a verified version of TLS and other components of HTTPS, replacing the current infrastructure with proven, secure software. Aiming both at full verification and usability, we conduct high-level code-based, game-playing proofs of security on cryptographic implementations that yield efficient, deployable code, at the level of C and assembly. Concretely, we use F*, a dependently typed language for programming, meta-programming, and proving at a high level, while relying on low-level DSLs embedded within F* for programming low-level components when necessary for performance and, sometimes, side-channel resistance. To compose the pieces, we compile all our code to source-like C and assembly, suitable for deployment and integration with existing code bases, as well as audit by independent security experts. Our main results so far include (1) the design of Low*, a subset of F* designed for C-like imperative programming but with high-level verification support, and KreMLin, a compiler that extracts Low* programs to C; (2) an implementation of the TLS-1.3 record layer in Low*, together with a proof of its concrete cryptographic security; (3) Vale, a new DSL for verified assembly language, and several optimized cryptographic primitives proven functionally correct and side-channel resistant. In an early deployment, all our verified software is integrated and deployed within libcurl, a widely used library of networking protocols.
Cite as

Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jianyang Pan, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, and Jean-Karim Zinzindohoué. Everest: Towards a Verified, Drop-in Replacement of HTTPS. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 1:1-1:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bhargavan_et_al:LIPIcs.SNAPL.2017.1,
  author =	{Bhargavan, Karthikeyan and Bond, Barry and Delignat-Lavaud, Antoine and Fournet, C\'{e}dric and Hawblitzel, Chris and Hritcu, Catalin and Ishtiaq, Samin and Kohlweiss, Markulf and Leino, Rustan and Lorch, Jay and Maillard, Kenji and Pan, Jianyang and Parno, Bryan and Protzenko, Jonathan and Ramananandro, Tahina and Rane, Ashay and Rastogi, Aseem and Swamy, Nikhil and Thompson, Laure and Wang, Peng and Zanella-B\'{e}guelin, Santiago and Zinzindohou\'{e}, Jean-Karim},
  title =	{{Everest: Towards a Verified, Drop-in Replacement of HTTPS}},
  booktitle =	{2nd Summit on Advances in Programming Languages (SNAPL 2017)},
  pages =	{1:1--1:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-032-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{71},
  editor =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2017.1},
  URN =		{urn:nbn:de:0030-drops-71196},
  doi =		{10.4230/LIPIcs.SNAPL.2017.1},
  annote =	{Keywords: Security, Cryptography, Verification, TLS}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact