-
Notifications
You must be signed in to change notification settings - Fork 0
/
Overview.html
215 lines (199 loc) · 12.3 KB
/
Overview.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
<!DOCTYPE html>
<html class="writer-html4" lang="en" >
<head>
<meta charset="utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<title>Underlying research — HACL* and EverCrypt Manual documentation</title><link rel="stylesheet" href="static/css/theme.css" type="text/css" />
<link rel="stylesheet" href="static/pygments.css" type="text/css" />
<!--[if lt IE 9]>
<script src="static/js/html5shiv.min.js"></script>
<![endif]-->
<script>
var DOCUMENTATION_OPTIONS = {
URL_ROOT:'./',
VERSION:'',
LANGUAGE:'None',
COLLAPSE_INDEX:false,
FILE_SUFFIX:'.html',
HAS_SOURCE: true,
SOURCELINK_SUFFIX: '.txt'
};
</script>
<script src="static/jquery.js"></script>
<script src="static/underscore.js"></script>
<script src="static/doctools.js"></script>
<script src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.1/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script>
<script src="static/js/theme.js"></script>
<link rel="index" title="Index" href="genindex.html" />
<link rel="search" title="Search" href="search.html" />
<link rel="next" title="Using the crypto library" href="Obtaining.html" />
<link rel="prev" title="List of supported algorithms" href="Supported.html" />
</head>
<body class="wy-body-for-nav">
<div class="wy-grid-for-nav">
<nav data-toggle="wy-nav-shift" class="wy-nav-side">
<div class="wy-side-scroll">
<div class="wy-side-nav-search" >
<a href="index.html" class="icon icon-home"> HACL* and EverCrypt Manual
</a>
<div role="search">
<form id="rtd-search-form" class="wy-form" action="search.html" method="get">
<input type="text" name="q" placeholder="Search docs" />
<input type="hidden" name="check_keywords" value="yes" />
<input type="hidden" name="area" value="default" />
</form>
</div>
</div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
<p class="caption"><span class="caption-text">Contents:</span></p>
<ul class="current">
<li class="toctree-l1"><a class="reference internal" href="HaclValeEverCrypt.html">HACL*, Vale, and EverCrypt</a></li>
<li class="toctree-l1"><a class="reference internal" href="Supported.html">List of supported algorithms</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">Underlying research</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#what-is-verified-software">What is verified software?</a></li>
<li class="toctree-l2"><a class="reference internal" href="#history-and-publications">History and publications</a></li>
<li class="toctree-l2"><a class="reference internal" href="#our-verification-tools">Our Verification Tools</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="Obtaining.html">Using the crypto library</a></li>
<li class="toctree-l1"><a class="reference internal" href="General.html">Digging into the F* source code</a></li>
<li class="toctree-l1"><a class="reference internal" href="HaclDoc.html">HACL APIs</a></li>
<li class="toctree-l1"><a class="reference internal" href="EverCryptDoc.html">EverCrypt APIs</a></li>
<li class="toctree-l1"><a class="reference internal" href="API.html">Which API to use</a></li>
<li class="toctree-l1"><a class="reference internal" href="Applications.html">Verified Applications</a></li>
</ul>
</div>
</div>
</nav>
<section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
<i data-toggle="wy-nav-top" class="fa fa-bars"></i>
<a href="index.html">HACL* and EverCrypt Manual</a>
</nav>
<div class="wy-nav-content">
<div class="rst-content">
<div role="navigation" aria-label="Page navigation">
<ul class="wy-breadcrumbs">
<li><a href="index.html" class="icon icon-home"></a> »</li>
<li>Underlying research</li>
<li class="wy-breadcrumbs-aside">
</li>
</ul>
<hr/>
</div>
<div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
<div itemprop="articleBody">
<div class="section" id="underlying-research">
<h1>Underlying research<a class="headerlink" href="#underlying-research" title="Permalink to this headline">¶</a></h1>
<div class="section" id="what-is-verified-software">
<h2>What is verified software?<a class="headerlink" href="#what-is-verified-software" title="Permalink to this headline">¶</a></h2>
<p>Formal verification involves using software tools to analyze <strong>all
possible behaviors</strong> of a program and prove mathematically that they comply with
the code’s specification (i.e., a machine-readable description of the
developer’s intentions). Unlike software testing, formal verification provides
strong guarantees that a program behaves as expected and is free from entire
classes of errors.</p>
<p>Our specifications cover a range of properties, including:</p>
<ul class="simple">
<li>Memory safety: our code never violates memory abstractions,
and, as a consequence, is free from common bugs and vulnerabilities like
buffer overflows, null-pointer dereferences, use-after-frees, double-frees,
etc.</li>
<li>Type safety: our code respects the interfaces amongs its components
including any abstraction boundaries; e.g., one component never passes
the wrong kind of parameters to another, or accesses its private state.</li>
<li>Functional correctness: our code’s input/output behavior is fully
characterized by simple mathematical functions derived directly
from the official cryptographic standards (e.g., from NIST or the IETF).</li>
<li>Secret Independence: Observations about our code’s low-level behavior
(specifically, the time it takes to execute or the memory addresses that it
accesses) are independent of the secrets manipulated by the library. Hence, an
adversary monitoring these “side-channels” learns nothing about the secrets.</li>
</ul>
<p>All of these guarantees <em>do not</em> prevent our code from achieving good
performance! HACL* meets or beats the performance of most existing
cryptographic implementations in C, and on certain platforms, Vale
code meets or beats the performance of hand-tuned assembly code in
state-of-the-art libraries. By bringing them together, the EverCrypt
provider provides best-in-class performance on most platforms.</p>
</div>
<div class="section" id="history-and-publications">
<h2>History and publications<a class="headerlink" href="#history-and-publications" title="Permalink to this headline">¶</a></h2>
<p>Our cryptographic code is the culmination of several years of research carried
through <a class="reference external" href="https://project-everest.github.io/">Project Everest</a>.</p>
<p>Early attempts at verifying cryptographic code in F* were presented at CSF 2016:
<a class="reference external" href="https://hal.inria.fr/hal-01425957">A Verified Extensible Library of Elliptic Curves</a> (Jean Karim Zinzindohoué, Evmorfia-Iro
Bartzia, Karthikeyan Bhargavan). This work established an initial body of
verified libraries, but extracted to OCaml and had substandard performance.
More on this early work be found in J-K Zinzindohoué’s <a class="reference external" href="https://www.theses.fr/s175861">Ph.D. thesis</a>.</p>
<p>To deliver better performance, we established a C-like subset of F* that would
compile to C, called Low*. Its foundations were presented at ICFP 2017:
<a class="reference external" href="https://arxiv.org/abs/1703.00053">Verified Low-Level Programming Embedded in F*</a> (Jonathan Protzenko, Jean-Karim
Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago
Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan
Bhargavan, Cédric Fournet, and Nikhil Swamy).</p>
<p>Using Low*, and inspired by discussions at the
<a class="reference external" href="https://github.com/HACS-workshop">HACS series of workshops</a>, we presented the
first version of the HACL* library at CCS 2017:
<a class="reference external" href="http://eprint.iacr.org/2017/536">HACL*: A Verified Modern Cryptographic Library</a> (Jean-Karim Zinzindohoué, Karthikeyan
Bhargavan, Jonathan Protzenko, Benjamin Beurdouche).</p>
<p>In parallel to work on HACL*, the Vale team set out to design a DSL for assembly programming,
for those algorithms which could not achieve maximal performance unless written in hand-tuned
assembly. The first version of Vale, which used Dafny as its verified backend,
was presented at Usenix 2017 (distinguished paper award): <a class="reference external" href="https://project-everest.github.io/assets/vale2017.pdf">Vale: Verifying
High-Performance Cryptographic Assembly Code</a> (Barry Bond, Chris
Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno,
Ashay Rane, Srinath Setty, Laure Thompson).</p>
<p>In order to unify C-like and ASM-like programming, Vale was overhauled to use F*
as its verification infrastructure; this second version of Vale was presented at
POPL 2019: <a class="reference external" href="https://www.microsoft.com/en-us/research/publication/a-verified-efficient-embedding-of-a-verifiable-assembly-language/">A Verified, Efficient Embedding of a Verifiable Assembly Language</a>
(Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem
Rastogi, Nikhil Swamy).</p>
<p>Having both C-like and ASM-like implementations all expressed in F* allowed us
to connect the two semantics and establish deep integrations between parts of
the codebase written in C and those written in assembly. Connecting C and ASM also
enabled implementation multiplexing and algorithmic agility, while establishing
strong abstraction boundaries to serve as a foundation for other verified
clients. We call the result EverCrypt: <a class="reference external" href="https://eprint.iacr.org/2019/757">EverCrypt: A Fast, Verified,
Cross-Platform Cryptographic Provider</a>
(Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina
Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine
Delignat-Lavaud, Cedric Fournet, Tahina Ramananandro, Aseem Rastogi, Nikhil
Swamy, Christoph Wintersteiger and Santiago Zanella-Beguelin).</p>
</div>
<div class="section" id="our-verification-tools">
<h2>Our Verification Tools<a class="headerlink" href="#our-verification-tools" title="Permalink to this headline">¶</a></h2>
<p>HACL* and EverCrypt are written and verified
using the <a class="reference external" href="https://github.com/FStarLang/kremlin/">F*</a> language, then compiled
to a mixture of C (using a dedicated compiler, <a class="reference external" href="https://github.com/FStarLang/kremlin/">KreMLin</a>).</p>
<p>The Vale cryptographic libraries (used in EverCrypt) rely on the
<a class="reference external" href="https://github.com/project-everest/vale/">Vale</a> tool, which compiles the Vale DSL to F*, and is
responsible for compiling the Vale code to assembly.</p>
</div>
</div>
</div>
</div>
<a href="https://github.com/project-everest/hacl-star/">
<img style="position: absolute; top: 0; right: 0; border: 0;" src="https://s3.amazonaws.com/github/ribbons/forkme_right_darkblue_121621.png" alt="Fork me on GitHub">
</a>
<footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
<a href="Supported.html" class="btn btn-neutral float-left" title="List of supported algorithms" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
<a href="Obtaining.html" class="btn btn-neutral float-right" title="Using the crypto library" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
</div>
<hr/>
<div role="contentinfo">
<p>© Copyright 2019, INRIA, Microsoft Research, CMU.</p>
</div>
Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
<a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
provided by <a href="https://readthedocs.org">Read the Docs</a>.
</footer>
</div>
</div>
</section>
</div>
<script>
jQuery(function () {
SphinxRtdTheme.Navigation.enable(true);
});
</script>
</body>
</html>