License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2019.1
URN: urn:nbn:de:0030-drops-115632
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11563/
Go to the corresponding LIPIcs Volume Portal

Bhargavan, Karthikeyan ; Naldurg, Prasad

Practical Formal Methods for Real World Cryptography (Invited Talk)

pdf-format:
LIPIcs-FSTTCS-2019-1.pdf (0.9 MB)

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.

BibTeX - Entry

@InProceedings{bhargavan_et_al:LIPIcs:2019:11563,
  author =	{Karthikeyan Bhargavan and Prasad Naldurg},
  title =	{{Practical Formal Methods for Real World Cryptography (Invited Talk)}},
  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 =	{Arkadev Chattopadhyay and Paul Gastin},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2019/11563},
  URN =		{urn:nbn:de:0030-drops-115632},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.1},
  annote =	{Keywords: Formal verification, Applied cryptography, Security protocols, Machine learning}
}

Keywords: Formal verification, Applied cryptography, Security protocols, Machine learning
Collection: 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)
Issue Date: 2019
Date of publication: 04.12.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI