From 607691568f2f71a1dd08facd91bbd6b2fab3a03f Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Thu, 31 May 2018 20:28:19 +0200 Subject: [PATCH] g: add documentation pointing to p256 modular reduction verification in Coq Added a markdown file with some explanation and links to Coq code in a public GitHub repository. BUG=none BRANCH=cr50 TEST=none Change-Id: I4b40a94ce8686e5115b6b09825dfde0894d67a50 Signed-off-by: Jade Philipoom Reviewed-on: https://chromium-review.googlesource.com/1080795 Commit-Ready: Vincent Palatin Tested-by: Vincent Palatin Reviewed-by: Vincent Palatin --- chip/g/dcrypto/proofs_p256.md | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 chip/g/dcrypto/proofs_p256.md diff --git a/chip/g/dcrypto/proofs_p256.md b/chip/g/dcrypto/proofs_p256.md new file mode 100644 index 0000000000..c0fa7ef6ad --- /dev/null +++ b/chip/g/dcrypto/proofs_p256.md @@ -0,0 +1,28 @@ +Proving P256 dcrypto code +========================= + +In 2018, partial proofs of modular reduction were written in the Coq proof +assistant. +They can be used against the crypto accelerator code in [chip/g/dcrypto/dcrypto_p256.c](dcrypto_p256.c). + +The Coq code is in this file: +[github.com/mit-plv/fiat-crypto/.../Experiments/SimplyTypedArithmetic.v](https://github.com/mit-plv/fiat-crypto/blob/e469076c37fc8b1b6d66eb700e379b9b2a093cb7/src/Experiments/SimplyTypedArithmetic.v) + +Specific lines of interest: + +Instruction specifications: +[fiat-crypto/.../Experiments/SimplyTypedArithmetic.v#L10014](https://github.com/mit-plv/fiat-crypto/blob/e469076c37fc8b1b6d66eb700e379b9b2a093cb7/src/Experiments/SimplyTypedArithmetic.v#L10014) + +Printouts of verified code versions with explanatory comments are at the very +end of the same file (which GitHub cuts off, so here is the link to the raw +version): +https://raw.githubusercontent.com/mit-plv/fiat-crypto/e469076c37fc8b1b6d66eb700e379b9b2a093cb7/src/Experiments/SimplyTypedArithmetic.v + +Additionally, the MulMod procedure in p256 uses a non-standard Barrett +reduction optimization. In particular, it assumes that the quotient estimate is +off by no more than 1, while most resources say it can be off by 2. This +assumption was proven correct for most primes (including p256) here: + +[fiat-crypto/.../Arithmetic/BarrettReduction/Generalized.v#L140](https://github.com/mit-plv/fiat-crypto/blob/e469076c37fc8b1b6d66eb700e379b9b2a093cb7/src/Arithmetic/BarrettReduction/Generalized.v#L140) + +The proofs can be re-checked using Coq version 8.7 or 8.8 (or above, probably).