From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTP id C59F45D4 for ; Thu, 14 May 2020 15:00:34 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.73,391,1583190000"; d="scan'208";a="449723568" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 14 May 2020 17:00:33 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 4AAC77F49A; Thu, 14 May 2020 17:00:33 +0200 (CEST) Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 49EF67F491 for ; Thu, 14 May 2020 17:00:25 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonathan.protzenko@gmail.com; spf=Pass smtp.mailfrom=jonathan.protzenko@gmail.com; spf=None smtp.helo=postmaster@mail-pl1-f194.google.com IronPort-PHdr: =?us-ascii?q?9a23=3ANKGfxhChunnbTVqPEH8KUyQJP3N1i/DPJgcQr6Af?= =?us-ascii?q?oPdwSPXzo8bcNUDSrc9gkEXOFd2Cra4d1qyH7eu/BCQp2tWoiDg6aptCVhsI24?= =?us-ascii?q?09vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7?= =?us-ascii?q?Ovr6GpLIj8Swyuu+54Dfbx9HiTagYb5+NhG7oATeusQUgYZpN7o8xAbOrnZUYe?= =?us-ascii?q?pd2HlmJUiUnxby58ew+IBs/iFNsP8/9MBOTLv3cb0gQbNXEDopPWY15Nb2tRbY?= =?us-ascii?q?VguA+mEcUmQNnRVWBQXO8Qz3UY3wsiv+sep9xTWaMMjrRr06RTiu86FmQwLvhy?= =?us-ascii?q?kaKj4563nXhdJsg6JHrhyhoBl/zJTVYIGTKfFyeqzQcNcfSWdHQ81fVTFOApmk?= =?us-ascii?q?YoUPEuQPI+VWoYfzqFQBsRSwChKhBP/txzJSmnP6waM33uYnHArb3AIgBdUOsH?= =?us-ascii?q?HModvxM6cSV/q6zLXIzTrZafNdxC3z6JLPchA9oPCDQ7RwccnWyUIyEA7FjFKQ?= =?us-ascii?q?qYr/MDOJ1uQCqW6b4/B4VeK1jG4ntwBwrSapxscvjYnEnY0VylXe+iV4xIY5P8?= =?us-ascii?q?G3SEl+YdO9FpZbqi6VOZdsTMw4X2FopDg1yqcAuZOjcyYHx5QqyhrBZvKJc4aF?= =?us-ascii?q?/A/uWumRLzp3i39oerCyihmz/EWg1ODwSsq53VhUoiRKkNTBuWwA2hPS58WFSv?= =?us-ascii?q?Zw/0Gs0iuB2QDU7+FLO0E0lazDJp4uw74wipoTsVnYESPsmUX2i7eadkol+ui0?= =?us-ascii?q?6+Tnf67pqoWAOI9zjwHzNLkllM+nAekgLAQCQ2yW9f6/2bDj50H1XqhGg/Isnq?= =?us-ascii?q?XEtJ3XKtwXqrO7DgJayIov9QuzAy273NkXg3ULNk9JdRyEgoXvJlrAOur3De2l?= =?us-ascii?q?jFSpiDprx+7JPrnmApjVK3jMirbhfbJk505EzAo/0MlT55xJBrwFL///QEDxtN?= =?us-ascii?q?vfDh82Nwy73fzrB8l61oMbQW6PA6mZP73OsVKQ+O4jP+2BaJUWtTv9MfQp+ePi?= =?us-ascii?q?gHAjlVMAeaSk0oMbaHWiEfRnJ0WZb2DsgtAEEWoSvAo+S+rqh0eeUT5TfXmyWb?= =?us-ascii?q?gw5ikhCIKhEYfCR56igLqC3Ce8BZBWaWVGBUqNEXfsbYmLR/AMaCeKLs97jjME?= =?us-ascii?q?TaShS5Mm1Ry2qAD10b9nLu7N9i0ctJLjz8R16vbIlRAy8Dx0F96S33uMT2FyhG?= =?us-ascii?q?MIRiU50LpxoUxnmR+/1v1zivlcUNhS/O9hUwEgNJeawfYpJcr1X1fjedGAVFav?= =?us-ascii?q?RJ2eGzYtXN83wNhGN0R6Hdy+jhnFmTKwBKMHmrqIA7Q796vd2z76IMMrmCWO77?= =?us-ascii?q?Uok1RzGpgHDmahnKMqq1mKWtz51n6BnqPvTpwymS7A8GDZkziLtUBcFRZ0CODL?= =?us-ascii?q?BCFDIETRqtv96wXJSLr8Ue17YDsE8taLL+5xUvOslU9PHa6xN9HXYmb3kGC1V0?= =?us-ascii?q?7Rl+G8KbHycmBY5x3zTU0NkgQd53GDbFFsCSKoomaYBztrRwvi?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AZEgBrXL1edMLWVdFmHgEBCxIMQIRiV?= =?us-ascii?q?V6EJYN6hQeFdoFkhCCHDZAJA1QLAQMBCgEBBSAIAgQBAYZbHAcBBDQTAhABAQU?= =?us-ascii?q?BAQECAQIDBAETAQoLDAcnhV8MgjsMg0MRFQgBGx4DEhAPAhgOAiURAQUBAi0IA?= =?us-ascii?q?QEegwQBgkoBAy4PoyyCHYEEPYsogRUFAReDAgWCSoIoChkoDWIDgTQCAQYJAQh?= =?us-ascii?q?8KoxCD4FMP4ERJ4FHdINTAgGCMYJHgmAEjjpAiipJmREHglB/BIcakBEGHZARj?= =?us-ascii?q?TcBjBaLRoIvk1kCCgcGDyOBRoF4TSOBAYI4UBgNkEANFoNPgmSIEiEzAjUCBgg?= =?us-ascii?q?BAQMJWI5sAQE?= X-IPAS-Result: =?us-ascii?q?A0AZEgBrXL1edMLWVdFmHgEBCxIMQIRiVV6EJYN6hQeFdoF?= =?us-ascii?q?khCCHDZAJA1QLAQMBCgEBBSAIAgQBAYZbHAcBBDQTAhABAQUBAQECAQIDBAETA?= =?us-ascii?q?QoLDAcnhV8MgjsMg0MRFQgBGx4DEhAPAhgOAiURAQUBAi0IAQEegwQBgkoBAy4?= =?us-ascii?q?PoyyCHYEEPYsogRUFAReDAgWCSoIoChkoDWIDgTQCAQYJAQh8KoxCD4FMP4ERJ?= =?us-ascii?q?4FHdINTAgGCMYJHgmAEjjpAiipJmREHglB/BIcakBEGHZARjTcBjBaLRoIvk1k?= =?us-ascii?q?CCgcGDyOBRoF4TSOBAYI4UBgNkEANFoNPgmSIEiEzAjUCBggBAQMJWI5sAQE?= X-IronPort-AV: E=Sophos;i="5.73,391,1583190000"; d="scan'208";a="449723487" X-MGA-submission: =?us-ascii?q?MDGM9WdFJRNMVXwYtkPaUaCVaW0cCEd7BhVDno?= =?us-ascii?q?sobMtV3JBB75D7A+eocWx0LzmU9nxARDuzzudmfawvgtiGIs5/gqwMpz?= =?us-ascii?q?UHNFTUyRVkroxK8orFJnHng9zgGO9zEELpec6GbehdOht3/C6WHdyrBs?= =?us-ascii?q?4AMxnaco0Fh7bXnzCHYW0HGw=3D=3D?= Received: from mail-pl1-f194.google.com ([209.85.214.194]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES256-GCM-SHA384; 14 May 2020 17:00:24 +0200 Received: by mail-pl1-f194.google.com with SMTP id q16so39676plr.2 for ; Thu, 14 May 2020 08:00:24 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:subject:to:message-id:date:user-agent:mime-version :content-transfer-encoding:content-language; bh=AGiM0pwboAu40CjWP5oeoiMUUuO54/14cmAYeOQx/I0=; b=QDhYBUdng1n3zcTqfechj50WmYN9f9ALWNikOanSg7QceERV1dSiNePxh3B20H1kWY c/m5WoFAmG3idNrxmLhE6egUymIWH+KwYH7Vw2Fs/LQZufYHSc1NNMUtlMTOvfoR7D1n y/xtKnxG1NsxvQOFv2DeAGderos2vVWhveYojl453I12+XJPvo+X8dyF3Jm0DKm2QfGb 7yqD+iG3TbwsyWCqnx9W5tdESIAi1okR8kVmXa3sfEJNQYVr6teh0OtteM0tRXr46sOd TjSc2i7FCwJcuAQKv2cgFKRQcXWVh/5Zs0KTCE7Ri+Ckw0Ytfm70sIi5RfIvY8872/5o zKKA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:subject:to:message-id:date:user-agent :mime-version:content-transfer-encoding:content-language; bh=AGiM0pwboAu40CjWP5oeoiMUUuO54/14cmAYeOQx/I0=; b=oRjgKabv9+qekEUdCAqs66cheBe0tWtpxb+SB4+5DD6bk4AEjTC6usxIov9oSkcNOT JI3zxuwPItesdr0BDCJPADvmMEJyQstCa1BNXyFevYdVxK7yck4V7K5FqHIismm7s1ry aQn6j8K8qZSC6dOz2sfgNZbg8r7MH3CnaBDivQIimrQz4TPRi+qgTqBaUwbs3FQQHOyb WXVrn/Cj7Et78LNRsXwtR/RrK947fXrFTpB48e5vQxJGJwLfeaccdg4BSt8YD6w+Dqw1 IP0OjlX3BSF2+eKafccxqn8RkvbPw/LZ4NU8rgmYK0Wh3g/g8d/egQpZ4SaufktMxAhg 4liQ== X-Gm-Message-State: AGi0PuaqbYQYXUONkcKYE1Z7XELunlQSupzKE/ffDZSVfnbq3ZzJTdWn Rc+p6IdB3FYozrqyBcuVNyXI2cg/CQ4= X-Google-Smtp-Source: APiQypJrc9pOnVV4vvR1ezyqjyUZL0FicMGes+FfSftelc7C97gik/E4hw7bn0kjvpPkj1W9LVhlfw== X-Received: by 2002:a17:90a:69e1:: with SMTP id s88mr41570207pjj.199.1589468421214; Thu, 14 May 2020 08:00:21 -0700 (PDT) Received: from absinthe.local (174-21-142-138.tukw.qwest.net. [174.21.142.138]) by smtp.gmail.com with ESMTPSA id p1sm19023182pjf.15.2020.05.14.08.00.19 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 14 May 2020 08:00:19 -0700 (PDT) From: Jonathan Protzenko To: caml-list@inria.fr Message-ID: Date: Thu, 14 May 2020 08:00:18 -0700 User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:68.0) Gecko/20100101 Thunderbird/68.7.0 MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit Content-Language: en-US Subject: [Caml-list] [ANN] Official OCaml bindings for verified Everest cryptography Reply-To: Jonathan Protzenko X-Loop: caml-list@inria.fr X-Sequence: 18141 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: The Everest team is pleased to announce the release of official OCaml bindings for all of our verified cryptographic algorithms, now available through OPAM as packages hacl-star and hacl-star-raw. We provide bindings for the following: - HACL*, a library of pure C algorithms - Vale, a collection of optimized core assembly routines for maximum performance - EverCrypt, an agile, multiplexing API with CPU auto-detection that brings together HACL* and Vale. Our code is compiled from the F* programming language to C via the KReMLin compiler ("K&R meets ML"). We offer two OPAM packages: - hacl-star-raw consists of low-level ocaml-ctypes bindings generated by KReMLin - hacl-star is a hand-written OCaml idiomatic API that uses much more pleasant signatures, types and abstractions and is also safer, as it checks all static preconditions at run-time We support AES{128,256}-GCM, Chacha20-Poly1305, Curve25519 / Ed25519, P256, MD5, SHA-{1,2,3} (all variants), Blake2 (s&b), HMAC/HKDF, and the HPKE and SecretBox high-level APIs. Some algorithms are optimized for Intel chips, notably AES-GCM -- see https://hacl-star.github.io/Supported.html for full details. General documentation about the project is available at https://hacl-star.github.io/index.html -- sample code for the OCaml API is provided as part of the test suite https://github.com/project-everest/hacl-star/tree/master/bindings/ocaml/tests This work was performed by Victor Dumitrescu from Nomadic Labs, one of the teams responsible for the core development of the Tezos blockchain. Happy hacking, Jonathan, on behalf of the Everest Team