Commit 552234ec authored by Franziskus Kiefer's avatar Franziskus Kiefer

Bug 1574643 - NSS changes for haclv2 r=jcj,kjacobs

This patch contains the changes in NSS, necessary to pick up HACL*v2 in D55413. It has a couple of TODOs:
* The chacha20 saw verification fails for some reason; it's disabled pending Bug 1604130.
* The hacl task on CI requires Bug 1593647 to get fixed.

Depends on D55413.

Differential Revision: https://phabricator.services.mozilla.com/D55414

--HG--
extra : moz-landing-system : lando
parent b119c419
......@@ -34,7 +34,7 @@ let SpecChaCha20 n = do {
};
print "Proving equality for a single block...";
time (llvm_verify m "Hacl_Chacha20_chacha20" [] (SpecChaCha20 64));
time (llvm_verify m "Hacl_Chacha20_chacha20_encrypt" [] (SpecChaCha20 64));
print "Proving equality for multiple blocks...";
time (llvm_verify m "Hacl_Chacha20_chacha20" [] (SpecChaCha20 256));
time (llvm_verify m "Hacl_Chacha20_chacha20_encrypt" [] (SpecChaCha20 256));
......@@ -34,9 +34,13 @@ RUN apt-get update \
pkg-config \
valgrind \
zlib1g-dev \
clang-format-3.9 \
&& rm -rf /var/lib/apt/lists/* \
&& apt-get autoremove -y && apt-get clean -y
RUN update-alternatives --install /usr/bin/clang-format \
clang-format $(which clang-format-3.9) 10
# Latest version of abigail-tools
RUN apt-get update \
&& apt-get install -y --no-install-recommends automake libtool libxml2-dev \
......
-----BEGIN PGP PUBLIC KEY BLOCK-----
mQINBFS+1SABEACnmkESkY7eZq0GhDjbkWpKmURGk9+ycsfAhA44NqUvf4tk1GPM
5SkJ/fYedYZJaDVhIp98fHgucD0O+vjOzghtgwtITusYjiPHPFBd/MN+MQqSEAP+
LUa/kjHLjgyXxKhFUIDGVaDWL5tKOA7/AQKl1TyJ8lz89NHQoUHFsF/hu10+qhJe
V65d32MXFehIUSvegh8DrPuExrliSiORO4HOhuc6151dWA4YBWVg4rX5kfKrGMMT
pTWnSSZtgoRhkKW2Ey8cmZUqPuUJIfWyeNVu1e4SFtAivLvu/Ymz2WBJcNA1ZlTr
RCOR5SIRgZ453pQnI/Bzna2nnJ/TV1gGJIGRahj/ini0cs2x1CILfS/YJQ3rWGGo
OxwG0BVmPk0cmLVtyTq8gUPwxcPUd6WcBKhot3TDMlrffZACnQwQjlVjk5S1dEEz
atUfpEuNitU9WOM4jr/gjv36ZNCOWm95YwLhsuci/NddBN8HXhyvs+zYTVZEXa2W
l/FqOdQsQqZBcJjjWckGKhESdd7934+cesGD3O8KaeSGxww7slJrS0+6QJ8oBoAB
P/WCn/y2AiY2syEKp3wYIGJyAbsm542zMZ4nc7pYfSu49mcyhQQICmqN5QvOyYUx
OSqwbAOUNtlOyeRLZNIKoXtTqWDEu5aEiDROTw6Rkq+dIcxPNgOLdeQ3HwARAQAB
tCFIYW5zIFdlbm5ib3JnIDxoYW5zQGNocm9taXVtLm9yZz6JARwEEAECAAYFAlT2
MQAACgkQVfXNcLtaBWnDKgf/fjusXk+kh1zuyn5eOCe16+2vV1lmXZrDIGdJtXDW
ZtHKele1Yv1BA3kUi5tKQi+VOOrvHL0+TMjFWFiCy1sYJS9qgkS08kReI2nAnhZ7
INdqEVxtVk1TTOhtYjOPy6txwujoICuPv5F4rHVhn1LPKGTLtYD2LOwf/8eKYQox
51gaJ8dNxpcHE/iFOIDXdebJPufo3EhqDRihchxb8AVLhrNss7pGGG/tVfichmHK
djPT2KfSh14pq1ahFOz0zH4nmTu7CCLnLAdRBHuhL8HVDbi0vKBtCiSmQggdxvoj
u+hpXiiDFQoCjLh0zVCwtFqWDZbnKMTBNNF26aTmQ+2fiYkBMwQQAQgAHRYhBB/m
NI7eqCWiKXDlxI3TBA8SPMP0BQJbcLU1AAoJEI3TBA8SPMP021sH/jD1m7azNCN6
DVL1iDJT6uIIYCTylygH5XI46CRoWaz/LwdFnUqWHHTcQxJ5pIkWV9KF+SIgMT42
brdZZmNvvSdX0odjFKqj5UR6w+wDN+uZ6Q40zu4pNoNzbk7pRpbFf1XIfGB1liyu
m28EJ58IXu/0AV7FiDAHGGBqppK/cwQN8pGLwmz1n6YELtXeFmtOGnusO6iLYOE7
3ByFCCqJB6twT5+7dDqFYqqQJgQ6jDTy19dDZ1vDhDttL+2Rn0OYXqPw7gy/1D2p
Y1cM9PgPBsR4EXhbtV0uKUNomk8tM/HnGMFT0KirI/tSwEP3v9g5YH992mrvNuIV
TkyQn0jGeMeJATMEEAEIAB0WIQRswFHTwdmkr54mDFjT45SsdE4uuwUCW3haCQAK
CRDT45SsdE4uu4JjCACppkreiMrpJSREKbUscdOvFxFRYzkTFeSCwX9Ih7r5ENpa
zjczfIqCCfWzioV6y4K0V04y8CXt/5S5a9vfW801pBUdF9nG4X8YbUn/xSe+8A9m
MsfDjMNcF7Cp5czVoSS4/4oHm9mQUMYQsn3AwwCPDKFORRRv5Eb0om9JawKtt++7
ZW0fOgDkvOCm14SN0UtVc4mxTx6iyxdMDgrKinBZVjxEh5oeqUyXh5TYM+XyWFVh
/gDUvUWwLI0GUWNTyOyUQU1oPVp+sWqrEe1BXLVCKFVWaSTtgJtJ5FyP+z2uzRcv
aanPOj/ohHAo8VBq9QbefYVAkShNBEuJkATnXhcGiQEzBBABCAAdFiEEvlzFWRM6
4JjNAb2a+j2ZL9Cqr7wFAlkBCcIACgkQ+j2ZL9Cqr7yB9AgArj+0+i0DCo1nm4MF
TLnW1Y9GF/Hq/mBva1MhkT0j3BzENK3xgqrqac8KqupsporNEmJ0ZbZzilJdZImb
o4X5BFdmmnjMiGaH6GAiPqRBBHGvLV2r2pG467J4tOMWO3XipFRf7FibbfhAU1lV
/GLWYTSwLqwWwBE8u5rriEvDngWUJw2Yd4Yqwduef7O6F+JfsGPRXFomR3387II0
8AXo/C+P5cl64llaxV6BmkJhQ6ydL0/KwSkHVdlXugk1sPtV/qOyPQ5L1Ibqbsvh
lLq/jhHlUUNLFjlQ2lrS9bhHGw9OIHTMJvS8RDrk0yAmoHAyRWNgbFN7aA62vBhq
pcUVzokBMwQQAQgAHRYhBPZ+fW6ADyQOg+vIZ/9qyaZGTfCcBQJa+ZAwAAoJEP9q
yaZGTfCcKMgH/jRxGfYhhGnlMnDLAEpYC+TGSDLMgmg9cOZbonqyMv+7Kts+pV03
KUr9SPV+VtGtOxRNiqwFt6V2MHcwPJfTXuH/bBW/HCCpr6UlOVWqIiCNK0Gnpcj5
rRt5unjG9CwsgyaK9QPI8bGin/c6m8BjwmEdfJ01ATLiUb8WuDHQy9OCyrEAnzSq
FD5ZtFmAFxvzm2x1nwb5HPuqkOqbRatp8aRJzTxIeSJPpgLw0PawHKGN3Ckp7REc
g26P1spkPe7SIVRsobH3al4uw7mgs7wiDWN3t8CdmuHAzmB2UrsR84JMTb45GboO
Bc1CX8xZcHyNaDEpyWHav+P8nZqwfBm+cLiJAjMEEAEIAB0WIQSawVDb4dGOtiX0
+gWyD0lU8+/LPwUCW/4O9QAKCRCyD0lU8+/LPyI7EACWtj0GEb1VT02gKwtKwgFn
RJ2pz8vYm188wgJwCJaL04d2D/VwE0jMvmfH80hSKgSLPAVMG06RIOb/tGhHsQKU
zBlHiAFmfjlJo1FC/Mp44RrERRsFAWBg0/URIs4vP8+5Vl+5m70sZrQpKeq+6TLM
1dQ0Ohz+QkQ04Z+DTroChWU8/7Uw0E3CqGGKYqPvDh54T1q4s8FoN0no8ZUlt/O+
r/3c7awr85ZnxqtnHIcuMbVyIZ+gOqXdrLa85yZITsh4zQrjYuyTEg7dpziReyiZ
+rkpdIdFKl8YeD+d0JWzVm7kq9D4K3+x9C509z0IgJUT3bhsX/N0Yf/QUtUW5oxI
T7fod86B/Q2M7zBTttFhd1vAjiSjEalK48SjTzWqTDYVIkea1+f1kZK5A0QlthqG
P2zy5GUjZVzOiCSOhyEOvAorU3zKD2s84VFKlayZEqlHJh8u5U59TWBdkW3qZUJd
ewW31xt0s8IovYSgOwX3wbsClQs6eVwNuCZT2yQAgAyXA5iFztBvDRQ0qmetvzV2
Ay9SrjvkQ3qr/eZmbMErEwEUxIO4b1rctCQ6jcbyVxMTAZAfaDoVKWEMXNiF2KSw
F9SSzGPIZDgiEXUlgaJBlUIYSFxrPuE+da0CM5RixyYIinU6AER6crl9C4C9XL6a
u3jf+5MTGxviRGn2oQzSCYkCMwQQAQgAHRYhBKeHFU4z7cw4HFbYuaxFYRTTj42I
BQJboq6kAAoJEKxFYRTTj42IWIAP/3rc9GjDTM4nI6Oi4OzLkwm/I2Vr7LUKG8oX
8E4Nj3amvNGupzGySjB+vrM6APrMSScXunvM0f19LV84EnNrUQ3KFZcSC6r5WC0B
2+TVRYGpY+6R9AQpqnuxicW0sa/AlV9WSEb4fDavCel2nW0arH4wkkCzTThUxoBB
X4I9nf4ZzGoUnnDAwTD9rN0gpI6Td/7faa3t99dRLb6AHJ1KhvyiiV3lr0xtTssD
xVHo0SpzQTnOcRJnYf/2rTny8bVfROPWieh6HuEiP7SxT1HyeTr4WSAjSCoG95O2
b3OgSMl0Z82FRMoJYmxID/V5YqH7015SjCxKdYhEZVp9YwWruEJIH8r6MGbWYNAl
REnyDvfGzAF0L0+gAUymDRmtp1jeXLo+HmLgVEUWegafs1TPfCWS/H9n10Upjmuq
akituzacz6Kjleq9qbnl81Xmh4AKmOILRwE7Pmcbl8HATOrmi5EaKffjMdWFzOWh
3U4/VsNDujqSTXD88EjGcpLiIiYefGy0sURJbIMTkfXVt3ruHLyuvhsRE/2QEAi7
gWB0zuBV8iGBaag+6RQkxGdpemPiogzuDijqZHoUXlp7Q6IYLanXeweyivdrSyTB
4HOECDbWEPZwk6tCxnuklW5iJndxBmxjSxefIMGU7G2JS9quppCVFCrKUjIWnf7b
gXnNji5JiQIzBBABCAAdFiEExZuSbLy7rtFhdiOuHt8NuZ2LeoQFAluirpUACgkQ
Ht8NuZ2LeoR/gQ/6A71JxUavzyBlCXlMy2Hx2+gOfy68b8UWl7DwKTOBSoZOzPC7
dVCSTzoK8dRELqsp7CkFImWcEwLJWMptuH2I1nK+Ua8bvxJSMJnOlPxYE8Wz5EK3
SQ2mQvifRezQTe8zjdpxEDSR6xocSiigvJow4X+Mivrxxj8sMgu1KA1ud2VGX/IR
wMbwuBTH9YydgvzmFzTxdlJHEYmsI8koHrVWPHm//QqqPBn+qz2z9uAzDmGAiDYg
qtQijo5IJC8ZjxgdcTfCkN6he+GhHtOhyP/KF/FcRHY83DoNCtqexQZWGuKtbd8o
nQYtmemRFob5kR7GxuNdAqF74oQfXcvXZNtHSuN3VtLqkB4fzW+21JBJCsP3XCzd
nKjR4erXNrQycmp3shSoJbnVvdbDwaVlWhDen1DvJb0Lj2sO3PQPcwVQbf5XHWR/
ZCf2OQTfVgwFEB4/0Twv70XwYIui2Ry9hmTPbD4Nn+UXbMQ3SOp90tj/e2yY/MFt
FvcIYcJTk9LM5IsnKgh+fSWDmdS3HD5Kjv2EPUHTNalruwwfmhS+ScJwM4XqHTJY
JkB16j/Xv2FTF+6KlbA1zdOVycPzoFKjAENYccQBVo2B+WQac7dFDqGEVNal9z66
DyU4ciAHl6PsbuN7DWeuScLoqq5jwx61bZgn71mUOYC1/47ypat2BKCOXZ2JAjME
EgEIAB0WIQSm5op4O95BdGcqQkHwXKpE5VGK/wUCWie53AAKCRDwXKpE5VGK/3rM
D/9jcYKOjYaPJh3Q7wNC1HjjUa73eo5GvJqyXbsXufIh/RAYgQkD08P5JgzfXvQ0
zOQTtDlDTVG8VMFoBYeMJVDd0k9LBbaljxcttMPfOll+AlQGAL7iQIqTAndknkJL
CFdl0ypa5GVsl1tzqmNC5fuMJ3vBoRtYbMitlHQkO0vLjZ7yl9fz+7YkREpEo/d5
Ya8t4+L6el6lrETYaiGCTxHcbYD7VdiJxpxFQlpgl+XKtobrj70RocGQ5JwUNilC
nRJKUb33lbmntwDwQ1y1AjCnhB++3GHjJDXBPgYFDCSZPCndKeOXhxmB2psFf41i
8foJPJXuh1vWOqArdwseFCRM6W2deF1utZmROMSkUo6IC8dYlucO/hjpjhG+C8Zv
QiM5uLylD3IPMX9wCz1tAhMNs3v4pEPo/4A//1cdLkor9cQVLFj3+TkS888EWZdj
Y8mUTIXU6yL1DXcj8CfDPS29fMpDorDpK1swl4pN5qgGfsL5BSAXUf1AZDWbxnEY
xf5rakfHDzrfbtbTSSfrBxS8gdW2vBKM+3nL21BeP8hQ0tkLA7bn2fNGz3aCOw46
XeVJdBk1gVTwazspylqrh1ljr0hQEN4gs/8kM645BRdD0IyAFFcI44VmuVwd8+2g
5miAGmVKSqN77w2cgMRnF7xpUsanv+3zKzaTnG+2liTeCokCPgQTAQIAKAUCVL7V
IAIbAwUJBaOagAYLCQgHAwIGFQgCCQoLBBYCAwECHgECF4AACgkQD8MELjRa0F1m
RhAAj9X+/4iiQsN888dNW/H1wEFFTd/1vqb2j0sHP3t02LkEPN5Ii9u71TSD2gSD
WTu1Eb46nRDcapFNv5M0vXcWrEt7PK9b51Kuj4KpP5IjJHpTl2g7umaYQWC8fqcY
TJTH0guMSCzZlsP0xGLbAj3cG6X5OPzCO+IxEafXmE//SfS9w46n1OC57ca1Y0Fp
WXfjA0sJrcozgNchsptu3jg/oEteYJoxDAzNO45O4geNONq5D9PUQPb+H5Vv5zpy
MI7iUJhVnTOFvnoUgRS7v6pWiA3flh5FelK8tYPCzEfvxfe7EB5GO7MaJEO3ZLni
COaAZ3Nfn6Tt28tCOgd052W4FeGWow7iYCS1Wgd30bq/FNgnl+tKv2woxmWt4jJv
ioBHQ4PbUnap2RCmBFaG7llRkrKP8nhWSUdwSS3OmDwAfxTTXjPaESK9EX9OV9Xo
or07thq+7OMs+2cyiy2jSfIau0SELy/tVioZBhoB7hzAJUB8sGHOxMPlVDFdUr3x
F/cgCclWANhw2xvgPim1wQ0XpeZe6w9RpmjZR7ReMYwxn8APBDP/e9R5aLDUQAep
2hrJUPK38D0L69RnpWQsR9hZ2hEOrMV2M6ChlvhwHbGSdJ2CcqG5Jx4ZAP23DK3A
N26TB88H9F7IMrM0REZeu7KzvYwCWlpg0zMXXKQ/2vovoe2JAlUEEwECAD8CGwMG
CwkIBwMCBhUIAgkKCwQWAgMBAh4BAheAFiEEtsj5goK5ROOw1cJTD8MELjRa0F0F
Alpd+i0FCQ8FJo0ACgkQD8MELjRa0F3X3A//dBQLm6GmXlQFjxZbukTw0lZsevFR
M/6ljZTxp7bsC+HFzYoaCKv6rikaWzytxk//SOaLKrB4Z9HjAlpBMtyLl2Hk7tcZ
bPpFafNmQ+4KgWNjLXCvt9se8BGrQvGQUrbE6YowbXa2YIgxIVEncFzIECAsp/+N
xbMcZN5/X1PJxKi/N22gP4nn47muN6L3pKez3CXgWnhGYSc7BuD5ALWYH7yMYUem
d4jlXfu5xkBIqirj1arIYC9wmF4ldbLNDPuracc8LmXcSqa5Rpao0s4iVzAD+tkX
vE/73m3rhepwBXxrfk0McXuI9aucf5h4/KkIBzZsaJ6JM1tzlrJzzjaBKJF9OI5T
jA0qTxdGzdPztS8gPaPcMkRFfh9ti0ZDx4VeF3s8sOtmMRHeGEWfxqUAbBUbwFsa
JDu/+8/VO4KijfcuUi8tqJ/JHeosCuGE7TM93LwJu6ZcqMYOPDROE/hsnGm0ZU92
xedu+07/X1ESHkSFPoaSHD5/DCNa/tXIyJZ8X7gF3eoDP5mSmrJqIqsOBR9WOVYv
dI8i0GHTXbrZj8WXdoS+N8wlyMLLbAS2jvTe7M5RoqbLz4ABOUUnLVoEE0CiccVZ
bW75BPxOfaD0szbinAeX6HDPI7St0MbKrRPjuDXjD0JVkLqFINtZfYLGMLss4tgn
suefr0Bo9ISwG3u5Ag0EVL7VIAEQAOxBxrQesChjrCqKjY5PnSsSYpeb4froucrC
898AFw2DgN/Zz+W7wtSTbtz/GRcCurjzZvN7o2rCuNk0j0+s1sgZZm2BdldlabLy
+UF/kSW1rb5qhfXcGGubu48OMdtSfok9lOc0Q1L4HNlGE4lUBkZzmI7Ykqfl+Bwr
m9rpi54g4ua9PIiiHIAmMoZIcbtOG1KaDr6CoXRk/3g2ZiGUwhq3jFGroiBsKEap
2FJ1bh5NJk2Eg8pV7fMOF7hUQKBZrNOtIPu8hA5WEgku3U3VYjRSI3SDi6QXnDL+
xHxajiWpKtF3JjZh8y/CCTD8PyP34YjfZuFmkdske5cdx6H0V2UCiH453ncgFVdQ
DXkY4n+0MTzhy2xu0IVVnBxYDYNhi+3MjTHJd9C4xMi9t+5IuEvDAPhgfZjDpQak
EPz6hVmgj0mlKIgRilBRK9/kOxky9utBpGk3jEJGru/hKNloFNspoYtY6zATAr8E
cOgoCFQE0nIktcg3wF9+OCEnV28/a7XZwUZ7Gl/qfOHtdr374wo8kd8R3V8d2G9q
5w0/uCV9NNQ0fGWZDPDoYt6wnPL6gZv/nJM8oZY+u0rC24WwScZIniaryC4JHDas
Ahr2S2CtgCvBgslK6f3gD16KHxPZMBpX73TzOYIhMEP/vXgVJbUD6dYht+U9c4Oh
EDJown0dABEBAAGJAjwEGAECACYCGwwWIQS2yPmCgrlE47DVwlMPwwQuNFrQXQUC
Wl36SwUJDwUmqwAKCRAPwwQuNFrQXT1/D/9YpRDNgaJl3YVDtVZoeQwh7BQ6ULZT
eXFPogYkF2j3VWg8s9UmAs4sg/4a+9KLSantXjX+JFsRv0lQe5Gr/Vl8VQ4LKEXB
fiGmSivjIZ7eopdd3YP2w6G5T3SA4d2CQfsg4rnJPnXIjzKNiSOi368ybnt9fL0Y
2r2aqLTmP6Y7issDUO+J1TW1XHm349JPR0Hl4cTuNnWm4JuX2m2CJEc5XBlDAha9
pUVs+J5C2D0UFFkyeOzeJPwy6x5ApWHm84n8AjhQSpu1qRKxKXdwei6tkQWWMHui
+TgSY/zCkmD9/oY15Ei5avJ4WgIbTLJUoZMi70riPmU8ThjpzA7S+Nk0g7rMPq+X
l1whjKU/u0udlsrIJjzkh6ftqKUmIkbxYTpjhnEujNrEr5m2S6Z6x3y9E5QagBMR
dxRhfk+HbyACcP/p9rXOzl4M291DoKeAAH70GHniGxyNs9rAoMr/hD5XW/Wrz3dc
KMc2s555E6MZILE2ZiolcRn+bYOMPZtWlbx98t8uqMf49gY4FGQBZAwPglMrx7mr
m7HTIiXahThQGOJg6izJDAD5RwSEGlAcL28T8KAuM6CLLkhlBfQwiKsUBNnh9r8w
V3lB+pV0GhL+3i077gTYfZBRwLzjFdhm9xUKEaZ6rN1BX9lzix4eSNK5nln0jUq1
67H2IH//2sf8dw==
=fTDu
-----END PGP PUBLIC KEY BLOCK-----
\ No newline at end of file
FROM ubuntu:xenial
MAINTAINER Franziskus Kiefer <franziskuskiefer@gmail.com>
# Based on the HACL* image from Benjamin Beurdouche and
# the original F* formula with Daniel Fabian
# Pinned versions of HACL* (F* and KreMLin are pinned as submodules)
ENV haclrepo https://github.com/mitls/hacl-star.git
# Define versions of dependencies
ENV opamv 4.05.0
ENV haclversion 1442c015dab97cdf203ae238b1f3aeccf511bd1e
# Install required packages and set versions
ADD B6C8F98282B944E3B0D5C2530FC3042E345AD05D.asc /tmp/B6C8F98282B944E3B0D5C2530FC3042E345AD05D.asc
ADD setup.sh /tmp/setup.sh
RUN bash /tmp/setup.sh
# Create user, add scripts.
RUN useradd -ms /bin/bash worker
WORKDIR /home/worker
ADD bin /home/worker/bin
RUN chmod +x /home/worker/bin/*
USER worker
# Build F*, HACL*, verify. Install a few more dependencies.
ENV OPAMYES true
ENV PATH "/home/worker/hacl-star/dependencies/z3/bin:$PATH"
ADD setup-user.sh /tmp/setup-user.sh
ADD license.txt /tmp/license.txt
RUN bash /tmp/setup-user.sh
#!/usr/bin/env bash
set -v -e -x
if [ $(id -u) = 0 ]; then
# Drop privileges by re-running this script.
exec su worker $0
fi
# Default values for testing.
REVISION=${NSS_HEAD_REVISION:-default}
REPOSITORY=${NSS_HEAD_REPOSITORY:-https://hg.mozilla.org/projects/nss}
# Clone NSS.
for i in 0 2 5; do
sleep $i
hg clone -r $REVISION $REPOSITORY nss && exit 0
rm -rf nss
done
exit 1
/* Copyright 2016-2017 INRIA and Microsoft Corporation
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
* You may obtain a copy of the License at
*
* http://www.apache.org/licenses/LICENSE-2.0
*
* Unless required by applicable law or agreed to in writing, software
* distributed under the License is distributed on an "AS IS" BASIS,
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
* See the License for the specific language governing permissions and
* limitations under the License.
*/
#!/usr/bin/env bash
set -v -e -x
# Prepare build (OCaml packages)
opam init
echo ". /home/worker/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true" >> .bashrc
opam switch -v ${opamv}
opam install ocamlfind batteries sqlite3 fileutils yojson ppx_deriving_yojson zarith pprint menhir ulex process fix wasm stdint
# Get the HACL* code
git clone ${haclrepo} hacl-star
git -C hacl-star checkout ${haclversion}
# Prepare submodules, and build, verify, test, and extract c code
# This caches the extracted c code (pins the HACL* version). All we need to do
# on CI now is comparing the code in this docker image with the one in NSS.
opam config exec -- make -C hacl-star prepare -j$(nproc)
make -C hacl-star -f Makefile.build snapshots/nss -j$(nproc)
KOPTS="-funroll-loops 5" make -C hacl-star/code/curve25519 test -j$(nproc)
make -C hacl-star/code/salsa-family test -j$(nproc)
make -C hacl-star/code/poly1305 test -j$(nproc)
# Cleanup.
rm -rf ~/.ccache ~/.cache
#!/usr/bin/env bash
set -v -e -x
# Update packages.
export DEBIAN_FRONTEND=noninteractive
apt-get -qq update
apt-get install --yes libssl-dev libsqlite3-dev g++-5 gcc-5 m4 make opam pkg-config python libgmp3-dev cmake curl libtool-bin autoconf wget locales
update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 200
update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-5 200
# Get clang-format-3.9
curl -LO https://releases.llvm.org/3.9.1/clang+llvm-3.9.1-x86_64-linux-gnu-ubuntu-16.04.tar.xz
curl -LO https://releases.llvm.org/3.9.1/clang+llvm-3.9.1-x86_64-linux-gnu-ubuntu-16.04.tar.xz.sig
# Verify the signature. The key used for verification was fetched via:
# gpg --keyserver pgp.key-server.io --recv-keys B6C8F98282B944E3B0D5C2530FC3042E345AD05D
# Use a local copy to workaround bug 1565013.
gpg --no-default-keyring --keyring tmp.keyring --import /tmp/B6C8F98282B944E3B0D5C2530FC3042E345AD05D.asc
gpg --no-default-keyring --keyring tmp.keyring --verify clang+llvm-3.9.1-x86_64-linux-gnu-ubuntu-16.04.tar.xz.sig
# Install into /usr/local/.
tar xJvf *.tar.xz -C /usr/local --strip-components=1
# Cleanup.
rm *.tar.xz*
locale-gen en_US.UTF-8
dpkg-reconfigure locales
# Cleanup.
rm -rf ~/.ccache ~/.cache
apt-get autoremove -y
apt-get clean
apt-get autoclean
......@@ -41,11 +41,6 @@ const FUZZ_IMAGE_32 = {
path: "automation/taskcluster/docker-fuzz32"
};
const HACL_GEN_IMAGE = {
name: "hacl",
path: "automation/taskcluster/docker-hacl"
};
const SAW_IMAGE = {
name: "saw",
path: "automation/taskcluster/docker-saw"
......@@ -1026,6 +1021,10 @@ function scheduleTests(task_build, task_cert, test_base) {
NSS_DISABLE_SSSE3: "1"
}, group: "Cipher"
}));
queue.scheduleTask(merge(cert_base_long, {
name: "Cipher tests", symbol: "NoSSE4.1", tests: "cipher",
env: {NSS_DISABLE_SSE4_1: "1"}, group: "Cipher"
}));
queue.scheduleTask(merge(cert_base, {
name: "EC tests", symbol: "EC", tests: "ec"
}));
......@@ -1154,7 +1153,7 @@ async function scheduleTools() {
queue.scheduleTask(merge(base, {
symbol: "hacl",
name: "hacl",
image: HACL_GEN_IMAGE,
image: LINUX_BUILDS_IMAGE,
command: [
"/bin/bash",
"-c",
......@@ -1200,18 +1199,22 @@ async function scheduleTools() {
]
}));
queue.scheduleTask(merge(base, {
parent: task_saw,
symbol: "ChaCha20",
group: "SAW",
name: "chacha20.saw",
image: SAW_IMAGE,
command: [
"/bin/bash",
"-c",
"bin/checkout.sh && nss/automation/taskcluster/scripts/run_saw.sh chacha20"
]
}));
// TODO: The ChaCha20 saw verification is currently disabled because the new
// HACL 32-bit code can't be verified by saw right now to the best of
// my knowledge.
// Bug 1604130
// queue.scheduleTask(merge(base, {
// parent: task_saw,
// symbol: "ChaCha20",
// group: "SAW",
// name: "chacha20.saw",
// image: SAW_IMAGE,
// command: [
// "/bin/bash",
// "-c",
// "bin/checkout.sh && nss/automation/taskcluster/scripts/run_saw.sh chacha20"
// ]
// }));
queue.scheduleTask(merge(base, {
parent: task_saw,
......
......@@ -8,33 +8,25 @@ fi
set -e -x -v
# The docker image this is running in has the HACL* and NSS sources.
# The extracted C code from HACL* is already generated and the HACL* tests were
# successfully executed.
# Verify HACL*. Taskcluster fails when we do this in the image build.
make -C hacl-star verify-nss -j$(nproc)
# Add license header to specs
spec_files=($(find ~/hacl-star/specs -type f -name '*.fst'))
for f in "${spec_files[@]}"; do
cat /tmp/license.txt "$f" > /tmp/tmpfile && mv /tmp/tmpfile "$f"
done
# Format the extracted C code.
cd ~/hacl-star/snapshots/nss
# The docker image this is running in has NSS sources.
# Get the HACL* source, containing a snapshot of the C code, extracted on the
# HACL CI.
# When bug 1593647 is resolved, extract the code on CI again.
git clone -q "https://github.com/project-everest/hacl-star" ~/hacl-star
git -C ~/hacl-star checkout -q 186a985597d57e3b587ceb0ef6deb0b5de706ae2
# Format the C snapshot.
cd ~/hacl-star/dist/mozilla
cp ~/nss/.clang-format .
find . -type f -name '*.[ch]' -exec clang-format -i {} \+
cd ~/hacl-star/dist/kremlin
cp ~/nss/.clang-format .
find . -type f -name '*.[ch]' -exec clang-format -i {} \+
# These diff commands will return 1 if there are differences and stop the script.
files=($(find ~/nss/lib/freebl/verified/ -type f -name '*.[ch]'))
for f in "${files[@]}"; do
diff $f $(basename "$f")
done
# Check that the specs didn't change either.
cd ~/hacl-star/specs
files=($(find ~/nss/lib/freebl/verified/specs -type f))
for f in "${files[@]}"; do
diff $f $(basename "$f")
file_name=$(basename "$f")
hacl_file=($(find ~/hacl-star/dist/mozilla/ ~/hacl-star/dist/kremlin/ -type f -name $file_name))
diff $hacl_file $f
done
......@@ -74,6 +74,7 @@ class Pkcs11ChaCha20Poly1305Test
// Check ciphertext and tag.
if (ct) {
ASSERT_EQ(ct_len, encrypted_len);
EXPECT_TRUE(!memcmp(ct, encrypted.data(), encrypted.size() - 16));
EXPECT_TRUE(!memcmp(ct, encrypted.data(), encrypted.size()) !=
invalid_tag);
}
......
......@@ -535,42 +535,26 @@ endif # lcc
endif # USE_64
ifndef HAVE_INT128_SUPPORT
DEFINES += -DKRML_NOUINT128
DEFINES += -DKRML_VERIFIED_UINT128
endif
ifndef NSS_DISABLE_CHACHAPOLY
ifeq ($(CPU_ARCH),x86_64)
ifdef HAVE_INT128_SUPPORT
EXTRA_SRCS += Hacl_Poly1305_64.c
else
EXTRA_SRCS += Hacl_Poly1305_32.c
endif
else
ifeq ($(CPU_ARCH),aarch64)
EXTRA_SRCS += Hacl_Poly1305_64.c
else
EXTRA_SRCS += Hacl_Poly1305_32.c
endif
EXTRA_SRCS += Hacl_Poly1305_128.c Hacl_Chacha20_Vec128.c Hacl_Chacha20Poly1305_128.c
endif # x86_64
VERIFIED_SRCS += Hacl_Chacha20.c
VERIFIED_SRCS += Hacl_Chacha20_Vec128.c
VERIFIED_SRCS += Hacl_Poly1305_32.c Hacl_Chacha20.c Hacl_Chacha20Poly1305_32.c
endif # NSS_DISABLE_CHACHAPOLY
ifeq (,$(filter-out i386 x386 x86 x86_64 aarch64,$(CPU_ARCH)))
# All intel architectures get the 64 bit version
# With custom uint128 if necessary (faster than generic 32 bit version).
ifeq (,$(filter-out x86_64 aarch64,$(CPU_ARCH)))
# All 64-bit architectures get the 64 bit version.
ECL_SRCS += curve25519_64.c
VERIFIED_SRCS += Hacl_Curve25519.c
VERIFIED_SRCS += Hacl_Curve25519_51.c
else
# All non intel architectures get the generic 32 bit implementation (slow!)
# All other architectures get the generic 32 bit implementation
ECL_SRCS += curve25519_32.c
endif
ifndef HAVE_INT128_SUPPORT
VERIFIED_SRCS += FStar.c
endif
#######################################################################
# (5) Execute "global" rules. (OPTIONAL) #
#######################################################################
......@@ -599,7 +583,7 @@ vpath %.c mpi ecl verified
vpath %.S mpi ecl
vpath %.s mpi ecl
vpath %.asm mpi ecl
INCLUDES += -Impi -Iecl -Iverified
INCLUDES += -Impi -Iecl -Iverified -Iverified/kremlin/include -Iverified/kremlin/kremlib/dist/minimal
DEFINES += -DMP_API_COMPATIBLE
......@@ -792,3 +776,7 @@ endif
ifeq ($(CPU_ARCH),ppc)
$(OBJDIR)/$(PROG_PREFIX)gcm-ppc$(OBJ_SUFFIX): CFLAGS += -mcrypto -maltivec
endif
$(OBJDIR)/$(PROG_PREFIX)Hacl_Chacha20_Vec128$(OBJ_SUFFIX): CFLAGS += -mssse3 -msse4 -mavx -maes
$(OBJDIR)/$(PROG_PREFIX)Hacl_Chacha20Poly1305_128$(OBJ_SUFFIX): CFLAGS += -mssse3 -msse4 -mavx -maes
$(OBJDIR)/$(PROG_PREFIX)Hacl_Poly1305_128$(OBJ_SUFFIX): CFLAGS += -mssse3 -msse4 -mavx -maes -mpclmul
......@@ -81,6 +81,8 @@ PRBool aesni_support();
PRBool clmul_support();
PRBool avx_support();
PRBool ssse3_support();
PRBool sse4_1_support();
PRBool sse4_2_support();
PRBool arm_neon_support();
PRBool arm_aes_support();
PRBool arm_pmull_support();
......
......@@ -28,6 +28,8 @@ static PRBool aesni_support_ = PR_FALSE;
static PRBool clmul_support_ = PR_FALSE;
static PRBool avx_support_ = PR_FALSE;
static PRBool ssse3_support_ = PR_FALSE;
static PRBool sse4_1_support_ = PR_FALSE;
static PRBool sse4_2_support_ = PR_FALSE;
static PRBool arm_neon_support_ = PR_FALSE;
static PRBool arm_aes_support_ = PR_FALSE;
static PRBool arm_sha1_support_ = PR_FALSE;
......@@ -74,6 +76,8 @@ check_xcr0_ymm()
#define ECX_OSXSAVE (1 << 27)
#define ECX_AVX (1 << 28)
#define ECX_SSSE3 (1 << 9)
#define ECX_SSE4_1 (1 << 19)
#define ECX_SSE4_2 (1 << 20)
#define AVX_BITS (ECX_XSAVE | ECX_OSXSAVE | ECX_AVX)
void
......@@ -84,6 +88,8 @@ CheckX86CPUSupport()
char *disable_pclmul = PR_GetEnvSecure("NSS_DISABLE_PCLMUL");
char *disable_avx = PR_GetEnvSecure("NSS_DISABLE_AVX");
char *disable_ssse3 = PR_GetEnvSecure("NSS_DISABLE_SSSE3");
char *disable_sse4_1 = PR_GetEnvSecure("NSS_DISABLE_SSE4_1");
char *disable_sse4_2 = PR_GetEnvSecure("NSS_DISABLE_SSE4_2");
freebl_cpuid(1, &eax, &ebx, &ecx, &edx);
aesni_support_ = (PRBool)((ecx & ECX_AESNI) != 0 && disable_hw_aes == NULL);
clmul_support_ = (PRBool)((ecx & ECX_CLMUL) != 0 && disable_pclmul == NULL);
......@@ -93,6 +99,10 @@ CheckX86CPUSupport()
disable_avx == NULL;
ssse3_support_ = (PRBool)((ecx & ECX_SSSE3) != 0 &&
disable_ssse3 == NULL);
sse4_1_support_ = (PRBool)((ecx & ECX_SSE4_1) != 0 &&
disable_sse4_1 == NULL);
sse4_2_support_ = (PRBool)((ecx & ECX_SSE4_2) != 0 &&
disable_sse4_2 == NULL);
}
#endif /* NSS_X86_OR_X64 */
......@@ -337,6 +347,16 @@ ssse3_support()
return ssse3_support_;
}
PRBool
sse4_1_support()
{
return sse4_1_support_;
}
PRBool
sse4_2_support()
{
return sse4_2_support_;
}
PRBool
arm_neon_support()
{
return arm_neon_support_;
......
......@@ -13,91 +13,40 @@
#include "secerr.h"
#include "blapit.h"
#include "blapii.h"
#ifndef NSS_DISABLE_CHACHAPOLY
#include "chacha20poly1305.h"
// Forward declaration from "Hacl_Chacha20_Vec128.h".
extern void Hacl_Chacha20_Vec128_chacha20(uint8_t *output, uint8_t *plain,
uint32_t len, uint8_t *k, uint8_t *n1,
uint32_t ctr);
// Forward declaration from "Hacl_Chacha20.h".
extern void Hacl_Chacha20_chacha20(uint8_t *output, uint8_t *plain, uint32_t len,
uint8_t *k, uint8_t *n1, uint32_t ctr);
#if defined(HAVE_INT128_SUPPORT) && (defined(NSS_X86_OR_X64) || defined(__aarch64__))
/* Use HACL* Poly1305 on 64-bit Intel and ARM */
#include "verified/Hacl_Poly1305_64.h"
#define NSS_POLY1305_64 1
#define Hacl_Poly1305_update Hacl_Poly1305_64_update
#define Hacl_Poly1305_mk_state Hacl_Poly1305_64_mk_state
#define Hacl_Poly1305_init Hacl_Poly1305_64_init
#define Hacl_Poly1305_finish Hacl_Poly1305_64_finish
typedef Hacl_Impl_Poly1305_64_State_poly1305_state Hacl_Impl_Poly1305_State_poly1305_state;
#else
/* All other platforms get the 32-bit poly1305 HACL* implementation. */
#include "verified/Hacl_Poly1305_32.h"
#define NSS_POLY1305_32 1
#define Hacl_Poly1305_update Hacl_Poly1305_32_update
#define Hacl_Poly1305_mk_state Hacl_Poly1305_32_mk_state
#define Hacl_Poly1305_init Hacl_Poly1305_32_init
#define Hacl_Poly1305_finish Hacl_Poly1305_32_finish
typedef Hacl_Impl_Poly1305_32_State_poly1305_state Hacl_Impl_Poly1305_State_poly1305_state;
#endif /* HAVE_INT128_SUPPORT */
static void
Poly1305PadUpdate(Hacl_Impl_Poly1305_State_poly1305_state state,
unsigned char *block, const unsigned char *p,
const unsigned int pLen)
{
unsigned int pRemLen = pLen % 16;
Hacl_Poly1305_update(state, (uint8_t *)p, (pLen / 16));
if (pRemLen > 0) {
memcpy(block, p + (pLen - pRemLen), pRemLen);
Hacl_Poly1305_update(state, block, 1);
}
}
/* Poly1305Do writes the Poly1305 authenticator of the given additional data
* and ciphertext to |out|. */
static void
Poly1305Do(unsigned char *out, const unsigned char *ad, unsigned int adLen,
const unsigned char *ciphertext, unsigned int ciphertextLen,
const unsigned char key[32])
{
#ifdef NSS_POLY1305_64
uint64_t stateStack[6U] = { 0U };
size_t offset = 3;
#elif defined NSS_POLY1305_32
uint32_t stateStack[10U] = { 0U };
size_t offset = 5;
#else
#error "This can't happen."
#endif
Hacl_Impl_Poly1305_State_poly1305_state state =
Hacl_Poly1305_mk_state(stateStack, stateStack + offset);
unsigned char block[16] = { 0 };
Hacl_Poly1305_init(state, (uint8_t *)key);
Poly1305PadUpdate(state, block, ad, adLen);
memset(block, 0, 16);
Poly1305PadUpdate(state, block, ciphertext, ciphertextLen);
unsigned int i;
unsigned int j;
for (i = 0, j = adLen; i < 8; i++, j >>= 8) {
block[i] = j;
}
for (i = 8, j = ciphertextLen; i < 16; i++, j >>= 8) {
block[i] = j;
}
Hacl_Poly1305_update(state, block, 1);
Hacl_Poly1305_finish(state, out, (uint8_t *)(key + 16));
#undef NSS_POLY1305_64
#undef NSS_POLY1305_32
}
#endif /* NSS_DISABLE_CHACHAPOLY */
// There are two implementations of ChaCha20Poly1305:
// 1) 128-bit with hardware acceleration used on x64
// 2) 32-bit used on all other platforms
// Instead of including the headers (they bring other things we don't want),
// we declare the functions here.
// Usage is guarded by runtime checks of required hardware features.
// Forward declaration from Hacl_Chacha20_Vec128.h and Hacl_Chacha20Poly1305_128.h.
extern void Hacl_Chacha20_Vec128_chacha20_encrypt_128(uint32_t len, uint8_t *out,
uint8_t *text, uint8_t *key,
uint8_t *n1, uint32_t ctr);
extern void
Hacl_Chacha20Poly1305_128_aead_encrypt(uint8_t *k, uint8_t *n1, uint32_t aadlen,
uint8_t *aad, uint32_t mlen, uint8_t *m,
uint8_t *cipher, uint8_t *mac);
extern uint32_t
Hacl_Chacha20Poly1305_128_aead_decrypt(uint8_t *k, uint8_t *n1, uint32_t aadlen,
uint8_t *aad, uint32_t mlen, uint8_t *m,
uint8_t *cipher, uint8_t *mac);
// Forward declaration from Hacl_Chacha20.h and Hacl_Chacha20Poly1305_32.h.
extern void Hacl_Chacha20_chacha20_encrypt(uint32_t len, uint8_t *out,
uint8_t *text, uint8_t *key,
uint8_t *n1, uint32_t ctr);
extern void
Hacl_Chacha20Poly1305_32_aead_encrypt(uint8_t *k, uint8_t *n1, uint32_t aadlen,
uint8_t *aad, uint32_t mlen, uint8_t *m,
uint8_t *cipher, uint8_t *mac);
extern uint32_t
Hacl_Chacha20Poly1305_32_aead_decrypt(uint8_t *k, uint8_t *n1, uint32_t aadlen,
uint8_t *aad, uint32_t mlen, uint8_t *m,
uint8_t *cipher, uint8_t *mac);
SECStatus
ChaCha20Poly1305_InitContext(ChaCha20Poly1305Context *ctx,
......@@ -162,10 +111,13 @@ void
ChaCha20Xor(uint8_t *output, uint8_t *block, uint32_t len, uint8_t *k,
uint8_t *nonce, uint32_t ctr)
{
if (ssse3_support() || arm_neon_support()) {
Hacl_Chacha20_Vec128_chacha20(output, block, len, k, nonce, ctr);
} else {
Hacl_Chacha20_chacha20(output, block, len, k, nonce, ctr);
#ifdef NSS_X64
if (ssse3_support() && sse4_1_support() && avx_support()) {
Hacl_Chacha20_Vec128_chacha20_encrypt_128(len, output, block, k, nonce, ctr);
} else
#endif
{
Hacl_Chacha20_chacha20_encrypt(len, output, block, k, nonce, ctr);
}
}
#endif /* NSS_DISABLE_CHACHAPOLY */
......@@ -198,8 +150,6 @@ ChaCha20Poly1305_Seal(const ChaCha20Poly1305Context *ctx, unsigned char *output,
#ifdef NSS_DISABLE_CHACHAPOLY
return SECFailure;
#else
unsigned char block[64];
unsigned char tag[16];
if (nonceLen != 12) {
PORT_SetError(SEC_ERROR_INPUT_LEN);
......@@ -215,16 +165,18 @@ ChaCha20Poly1305_Seal(const ChaCha20Poly1305Context *ctx, unsigned char *output,
return SECFailure;
}
PORT_Memset(block, 0, sizeof(block));
// Generate a block of keystream. The first 32 bytes will be the poly1305
// key. The remainder of the block is discarded.
ChaCha20Xor(block, (uint8_t *)block, sizeof(block), (uint8_t *)ctx->key,
(uint8_t *)nonce, 0);
ChaCha20Xor(output, (uint8_t *)input, inputLen, (uint8_t *)ctx->key,
(uint8_t *)nonce, 1);
Poly1305Do(tag, ad, adLen, output, inputLen, block);
PORT_Memcpy(output + inputLen, tag, ctx->tagLen);
#ifdef NSS_X64
if (ssse3_support() && sse4_1_support() && avx_support()) {
Hacl_Chacha20Poly1305_128_aead_encrypt(
(uint8_t *)ctx->key, (uint8_t *)nonce, adLen, (uint8_t *)ad, inputLen,
(uint8_t *)input, output, output + inputLen);
} else
#endif