scottk/OpenCellular
1
0
Fork 0
mirror of https://github.com/Telecominfraproject/OpenCellular.git synced 2026-01-12 19:04:59 +00:00
Code Issues Packages Projects Releases Wiki Activity

g: add documentation pointing to p256 modular reduction verification in Coq

Browse Source 
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 <jadep@google.com>
Reviewed-on: https://chromium-review.googlesource.com/1080795
Commit-Ready: Vincent Palatin <vpalatin@chromium.org>
Tested-by: Vincent Palatin <vpalatin@chromium.org>
Reviewed-by: Vincent Palatin <vpalatin@chromium.org>
This commit is contained in:
Jade Philipoom
2018-05-31 20:28:19 +02:00
committed by chrome-bot
parent bdc27c3085
commit 607691568f
1 changed files with 28 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

28
chip/g/dcrypto/proofs_p256.md Normal file
View File

@@ -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).