-
Notifications
You must be signed in to change notification settings - Fork 0
/
Obtaining.html
255 lines (239 loc) · 16.1 KB
/
Obtaining.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
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
<!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>Using the crypto library — 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="Digging into the F* source code" href="General.html" />
<link rel="prev" title="Underlying research" href="Overview.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"><a class="reference internal" href="Overview.html">Underlying research</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">Using the crypto library</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#picking-a-distribution">Picking a distribution</a></li>
<li class="toctree-l2"><a class="reference internal" href="#compiling-a-full-distribution">Compiling a full distribution</a></li>
<li class="toctree-l2"><a class="reference internal" href="#integrating-the-code">Integrating the code</a></li>
<li class="toctree-l2"><a class="reference internal" href="#bindings-for-other-languages">Bindings for Other Languages</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#ocaml">OCaml</a></li>
<li class="toctree-l3"><a class="reference internal" href="#javascript">JavaScript</a></li>
<li class="toctree-l3"><a class="reference internal" href="#rust">Rust</a></li>
</ul>
</li>
</ul>
</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>Using the crypto library</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="using-the-crypto-library">
<h1>Using the crypto library<a class="headerlink" href="#using-the-crypto-library" title="Permalink to this headline">¶</a></h1>
<div class="section" id="picking-a-distribution">
<h2>Picking a distribution<a class="headerlink" href="#picking-a-distribution" title="Permalink to this headline">¶</a></h2>
<p>Building the full <code class="docutils literal notranslate"><span class="pre">hacl-star</span></code> repository verifies the source F* and Vale code,
then proceeds to extract it to C and assembly. However, users do not have to use
this full build process: we provide the generated code in the <code class="docutils literal notranslate"><span class="pre">dist/</span></code>
directory, under version control to facilitate obtaining the source code.</p>
<p>Each subdirectory corresponds to a <em>distribution</em>, i.e. a particular set of
options passed to KreMLin (the F*-to-C compiler) that influence how the
generated C code looks like.</p>
<p>There is a total order on distributions:
<code class="docutils literal notranslate"><span class="pre">c89-compatible</span> <span class="pre"><=</span> <span class="pre">msvc-compatible</span> <span class="pre"><=</span> <span class="pre">gcc-compatible</span> <span class="pre"><=</span> <span class="pre">gcc64-only</span></code></p>
<ul class="simple">
<li>The C89 distribution will work with the most C compilers; it relies on
<code class="docutils literal notranslate"><span class="pre">alloca</span></code>; eliminates compound literals and enforces C89 scope to generate
syntactically C89-compliant code; code still relies on inttypes.h and other
headers that you may have to provide depending on your target. It does not
include Merkle Trees and the code is incredibly verbose.</li>
<li>The MSVC distribution relies on <code class="docutils literal notranslate"><span class="pre">alloca</span></code> to avoid C11 VLA for the sake of
MSVC; relies on KreMLin for tail-call optimizations. It also does not use GCC
inline assembly for Curve25519 and uses external linkage instead.</li>
<li>The GCC distribution relies on C11 VLA and therefore does not work with MSVC.</li>
<li>The GCC64 distribution assumes a native <code class="docutils literal notranslate"><span class="pre">unsigned</span> <span class="pre">__int128</span></code> type which can be
manipulated via the standard arithmetic operators. This generates very compact
code but only works on 64-bit GCC and Clang.</li>
</ul>
<p>Other distributions are either for distinguished consumers of our code who need
specific KreMLin compilation options (e.g. Mozilla, CCF) or for testing (e.g.
portable-gcc-compatible, which compiles without <code class="docutils literal notranslate"><span class="pre">-march=native</span></code>, to ensure all
our assumptions about CPU targets are explicit in our Makefile).</p>
</div>
<div class="section" id="compiling-a-full-distribution">
<h2>Compiling a full distribution<a class="headerlink" href="#compiling-a-full-distribution" title="Permalink to this headline">¶</a></h2>
<p>Each distribution comes with its own Makefile. It builds a static object
(libevercrypt.a) and a dynamic object (libevercrypt.{so,dll}) along with the
import library for Windows systems (libevercrypt.dll.a). On Windows, the
Makefile has been tested in a Cygwin environment equipped with the MinGW
cross-compilers. The <cite>dist/compact-msvc</cite> distribution works with the Microsoft
compilers, but we provide no build support (i.e. no Visual Studio project, no
NMake-compatible makefile).</p>
<div class="admonition note">
<p class="first admonition-title">Note</p>
<p class="last">The <code class="docutils literal notranslate"><span class="pre">gcc-compatible</span></code> distribution also features OCaml bindings to our code.
These require a valid OCaml setup, including packages ctypes, ctypes-foreign
and bigstring, usually obtained via OPAM. You can easily disable building
these bindings by removing the <code class="docutils literal notranslate"><span class="pre">lib_gen</span></code> directory in
<code class="docutils literal notranslate"><span class="pre">dist/gcc-compatible</span></code>.</p>
</div>
</div>
<div class="section" id="integrating-the-code">
<h2>Integrating the code<a class="headerlink" href="#integrating-the-code" title="Permalink to this headline">¶</a></h2>
<p>To incorporate our verified crypto code into a C software project, a developer
has two choices.</p>
<ul class="simple">
<li>Pick a full EverCrypt distribution, along with the
<cite>dist/kremlin</cite> directory, thus giving a “wholesale” integration of
the EverCrypt library, including all supported algorithms from HACL* and Vale.</li>
<li>For a more selective integration, cherry-pick the C or assembly
files for specific versions of specific algorithms. Each header
file contains the list of other headers (and implementations) it
depends on so it’s easy to integrate, say, an individual algorithm
from the HACL API without taking the full library.</li>
</ul>
<p>The <code class="docutils literal notranslate"><span class="pre">dist/kremlin</span></code> directory contains all the required headers from
KreMLin. In particular, these headers contain implementations of
FStar.UInt128, the module for 128-bit arithmetic. The
<code class="docutils literal notranslate"><span class="pre">kremlin/include/kremlin/internal/types.h</span></code> header will attempt to
use C preprocessor macros to pick the right UInt128 implementation for
your platform:</p>
<ul class="simple">
<li>64-bit environment with GCC/Clang: hand-written implementation using
<code class="docutils literal notranslate"><span class="pre">unsigned</span> <span class="pre">__int128</span></code> (unverified)</li>
<li>MSVC: hand-written implementation using intrinsics (also unverified)</li>
<li>every other case, or when <code class="docutils literal notranslate"><span class="pre">KRML_VERIFIED_UINT128</span></code> is defined at compile-time:
verified (slow) implementation extracted from FStar.UInt128</li>
</ul>
</div>
<div class="section" id="bindings-for-other-languages">
<h2>Bindings for Other Languages<a class="headerlink" href="#bindings-for-other-languages" title="Permalink to this headline">¶</a></h2>
<p>HACL* and EverCrypt are designed to primarily be used either within
verification-oriented projects in F* or as part of larger C
developments. In addition to these use cases, the library developers
and other HACL* users have also developed bindings for other programming languages:</p>
<div class="section" id="ocaml">
<h3>OCaml<a class="headerlink" href="#ocaml" title="Permalink to this headline">¶</a></h3>
<p>The KReMLin compiler auto-generates <code class="docutils literal notranslate"><span class="pre">ocaml-ctypes</span></code> bindings for HACL*. On top
of these “raw” bindings, we add a high-level wrapper that uses functors, shares
type signatures, performs run-time checks and offers a much more idiomatic API.</p>
<p>They are both available as opam packages and can be installed using
<code class="docutils literal notranslate"><span class="pre">opam</span> <span class="pre">install</span> <span class="pre">hacl-star</span></code> or, to get the low-level bindings only,
<code class="docutils literal notranslate"><span class="pre">opam</span> <span class="pre">install</span> <span class="pre">hacl-star-raw</span></code>.</p>
<p>From source, the low-level bindings can be installed by running
<code class="docutils literal notranslate"><span class="pre">make</span> <span class="pre">install-hacl-star-raw</span></code> in <code class="docutils literal notranslate"><span class="pre">dist/gcc-compatible</span></code>. Then, the high-level
wrapper can be installed by running <code class="docutils literal notranslate"><span class="pre">dune</span> <span class="pre">build</span> <span class="pre">&&</span> <span class="pre">dune</span> <span class="pre">install</span></code> in
<code class="docutils literal notranslate"><span class="pre">bindings/ocaml</span></code>.</p>
<p>Documentation for the high-level API is available <a class="reference external" href="https://hacl-star.github.io/ocaml_doc/">here</a>.</p>
</div>
<div class="section" id="javascript">
<h3>JavaScript<a class="headerlink" href="#javascript" title="Permalink to this headline">¶</a></h3>
<p>HACL* is compiled to WebAssembly via the WASM backend of KreMLin (see the
Oakland’19 paper for details). We offer an idiomatic JavaScript API on top of
HACL-WASM so that clients do not have to be aware of the KreMLin memory layout,
calling convention, etc. This latter API is available as a
<a class="reference external" href="https://www.npmjs.com/package/hacl-wasm">Node.js package</a>.</p>
<p>The <cite>jsdoc</cite> documentation of the package can be found <a class="reference external" href="https://hacl-star.github.io/javascript_doc/">online</a>. Please note that the API is
asynchronous (it uses promises).</p>
<p>Here is a small example of how to use the library (with Node.js) :</p>
<div class="highlight-javascript notranslate"><div class="highlight"><pre><span></span><span class="kd">var</span> <span class="nx">hacl</span> <span class="o">=</span> <span class="nx">require</span><span class="p">(</span><span class="s2">"hacl-wasm"</span><span class="p">);</span>
<span class="nx">hacl</span><span class="p">.</span><span class="nx">Curve25519</span><span class="p">.</span><span class="nx">ecdh</span><span class="p">(</span><span class="ow">new</span> <span class="nb">Uint8Array</span><span class="p">(</span><span class="mf">32</span><span class="p">),</span> <span class="ow">new</span> <span class="nb">Uint8Array</span><span class="p">(</span><span class="mf">32</span><span class="p">)).</span><span class="nx">then</span><span class="p">(</span><span class="kd">function</span> <span class="p">(</span><span class="nx">result</span><span class="p">)</span> <span class="p">{</span>
<span class="c1">// Here result contains an Uint8Array of size 32 with the DH exchange result</span>
<span class="p">});</span>
</pre></div>
</div>
</div>
<div class="section" id="rust">
<h3>Rust<a class="headerlink" href="#rust" title="Permalink to this headline">¶</a></h3>
<p>Various users have also published Rust crates for HACL*, but these have not been
vetted by the HACL maintainers.</p>
</div>
</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="Overview.html" class="btn btn-neutral float-left" title="Underlying research" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
<a href="General.html" class="btn btn-neutral float-right" title="Digging into the F* source code" 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>