-
Notifications
You must be signed in to change notification settings - Fork 0
/
HaclValeEverCrypt.html
152 lines (136 loc) · 7.46 KB
/
HaclValeEverCrypt.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
<!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>HACL*, Vale, and EverCrypt — 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="List of supported algorithms" href="Supported.html" />
<link rel="prev" title="A High Assurance Cryptographic Library" href="index.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 current"><a class="current reference internal" href="#">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"><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>HACL*, Vale, and EverCrypt</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="hacl-vale-and-evercrypt">
<span id="hacl-vale-evercrypt"></span><h1>HACL*, Vale, and EverCrypt<a class="headerlink" href="#hacl-vale-and-evercrypt" title="Permalink to this headline">¶</a></h1>
<p>The <a class="reference external" href="https://github.com/project-everest/hacl-star/">hacl-star</a> repository
contains code from several related projects developed as part of
<a class="reference external" href="https://project-everest.github.io/">Project Everest</a>, which aims to build
and deploy a verified HTTPS stack. These components are arranged as shown below.</p>
<a class="reference internal image-reference" href="images/diagram.png"><img alt="images/diagram.png" class="align-center" src="images/diagram.png" style="width: 80%;" /></a>
<ul class="simple">
<li>HACL* provides a set of highly efficient, pure C implementations of complete
cryptographic primitives. Each algorithm comes with its own API callable from
C clients.</li>
<li>Vale provides optimized assembly (ASM) core routines for performance-critical
code. Vale code is not intended to be called from C by end users.</li>
<li>EverCrypt brings HACL* and Vale under an abstract, high-level API
that automatically picks the best Vale or HACL* implementation depending on
the machine the code is running on (multiplexing). EverCrypt also offers a
single API for all algorithms from the same family (e.g. AEAD, hashes),
allowing clients to reconfigure their choice of algorithm dynamically without
recompiling (agility).</li>
</ul>
<p>All of this code is verified using the F* programming language; once verified,
our code is extracted to a mixture of C and ASM.</p>
<p>Our code is callable from C clients, and from OCaml, via ctypes bindings. A
subset of our code (the HACL API) compiles to WebAssembly via a dedicated,
formalized codepath of the <a class="reference external" href="https://github.com/FStarLang/kremlin/">KreMLin</a> compiler and can be used for any Web context
(e.g. Electron, website) where modern, trustworthy cryptography is in order.</p>
<p>In addition to unverified clients, verified clients can be built atop the
EverCrypt API. These include a library of Merkle Trees, distributed in the
present repository, but also an implementation of the Signal protocol in F*.</p>
</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="index.html" class="btn btn-neutral float-left" title="A High Assurance Cryptographic Library" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
<a href="Supported.html" class="btn btn-neutral float-right" title="List of supported algorithms" 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>