Skip to content

External CI

Jump to bottom
François Dupressoir edited this page Sep 20, 2024 · 4 revisions

What is is the external CI?

The external CI is a list of external (proof) projects who have an identified and active maintainer, and that we run planned EasyCrypt changes against for early warning of any proof breakage.

Currently, this list includes:

  • Jasmin's EClib
  • A proof of indifferentiability (and security) for SHA3
  • A proof of security for the NIKE + AE construction of public key authenticated encryption (as embodied in NaCl's crypto_box), done SSP-style.
  • A proof of a nonce-extending cascade mode for blockciphers, and its application in XSalsa20
  • A proof of unforgeability for XMSS.
  • A proof of unforgeability for SPHINCS+.

How do I add my project to the external CI?

Please make a pull request adding a simple entry in the array in .github/workflows/external.json.

Each entry must include the following string-typed fields:

  • name: a name to identify your proof by, ideally unique;
  • repository: a public cloning URL for your repository;
  • branch: the branch you want us to run the CI on—keep in mind that the runs will be done with PRs onto EasyCrypt's main, so the branch you provide will need maintenance between releases;
  • subdir: the sub-directory in which EasyCrypt should run (as easycrypt runtest)—please use "." if the run should take place at the repo's root;
  • config: the path (relative to the subdir) at which the easycrypt runtest config file can be found;
  • scenario: the scenario that should be run;
  • options: any options that should be passed to easycrypt runtest during the run.

Please then assign the PR to yourself, and assign fdupress as a reviewer. The time your proof takes to check will be taken into account, and we may ask for information about your local CI setup (any CI that runs on your side when you push changes to your external proof).

Your proof must be public and publicly cloneable for us to consider including it in our external CI.

Projects we would like to bring under external CI

For sure:

  • Saber
  • Dilithium

Maybe, but perhaps best as Formosa/Jasmin:

  • ChaCha functional
  • SHA3 functional

Maybe, after some effort:

  • KMS
  • Yao's Garbled Circuits
  • CMAC
  • CV2EC

Truly external and need community work:

  • Maurer MPC (Aarhus)
  • MPC in the head (Aarhus)
  • Rewinding (Tartu)
  • Whatever secret things lurk waiting to be made public
Clone this wiki locally