Improvements to formal verification of P-384 #141

apetcher-amazon · 2024-03-28T17:44:37Z

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

This PR has the following significant improvements to the formal verification of P-384

Constant values like the pre-computed table of multiples of the base point are no longer assumed to be correct. Instead, these values are tested using formally-verified tests, and we assume these tests pass in the Coq proof. These assumptions are sufficient to prove that the constant values are correct.
The ECDH output conversion, including the field inverse square operation and Jacobian to affine conversion, is formally verified. After this change, all field/point conversion operations are either verified in these proofs or provided by formally verified field arithmetic libraries.

The README file was updated to remove the two significant caveats associated with the changes above. I also added two new caveats:

ECDH_InfinityTestCorrect describes an assumption about the behavior of a particular subroutine used in ECDH output conversion. Previously, the entire conversion routine (not just this subroutine) was assumed to be correct.
SAW_EC_FieldGap is a caveat that should have been included in the last PR on this topic. This caveat makes it clear that there is a gap between the semantics and memory model used to verify the field arithmetic vs other P-384 operations.

There are also significant organizational changes to the Coq proof in this PR. These changes should improve the overall organization, and they were helpful in isolating Coq performance issues that arise from operating on actual values.

…on. Working on improving the organization.

…erification into p384_validate_2

…oint.

patch in a script.

pennyannn

I reviewed the SAW proof part of this PR.

SAW/proof/EC/EC_P384_validate.saw

SAW/spec/EC/EC_mul.cry

README.md

Coq/EC/EC_P384_Abstract_5_equiv.v

khieta

I looked through the files in Coq/EC/ and the README and didn't find anything problematic -- the Coq changes are largely refactoring.

Some more high-level comments:

I left a couple minor comments about documenting assumptions in the proofs when a comment wasn't readily available. For easier review in the future, you might consider adding a special comment string (e.g. "ASSUMPTION") to assumptions like Variable and Hypothesis.
If you're in the mood for some hacking, you could even set up GitHub CI to check that all assumptions are documented, and nothing is admitted. We do something sort of similar in our Rust code, where we check that any function that can panic is prefixed by a comment with the string "PANIC SAFETY".
How are the new table validation functions actually run? I see that they're assumed to pass in the proofs, but I didn't notice them being extracted anywhere.

khieta · 2024-04-17T13:36:12Z

SAW/scripts/x86_64/entrypoint_check.sh

-# First, apply some patches (TODO: remove them)...
+ # Start by patching in the constant validation tests and executing them
+apply_patch "p384_validate"


Out of curiosity: what are these patches for? Are they changes that need to be contributed back to the SAW tool? Are you doing any verification pre-patching, or is all testing/verification done on the patched code?

The patches are mostly used to make trivial modifications to the code (that we believe produce semantically equivalent code) to work around tool limitations or otherwise allow the formal verification to work. Most patches are used to mark functions as noinline so they will not be inlined when compiling from C to LLVM, and so we can prove them correct and re-use these proofs when functions are called. All verification is done after patching the code.

This particular patch adds in the constant verification code. This test code uses symbols that are not visible outside the p384.c file, so the test code needs to be inside this file. The simple solution is to patch it in, and then invoke the test function from the existing test suite.

To answer your question about how the test is executed: it is patched in to the test suite by the patch on line 20 of this file, and then then the entire test suite is executed on line 30.

But the code patched in here is C code, right? How does that relate to the Coq validation functions?

The patched in C functions are verified against a Cryptol spec using SAW. This is done in EC_P384_validate.saw, and the Cryptol spec was added to EC_mul.cry (e.g. validate_base_table). The Cryptol spec is converted to Gallina functions with the same name, and we prove the required correctness properties of these functions in Coq. We also assume that validate_base_table was executed on the pre-computed table on line 648 of EcEqProof.v, and this assumption is justified by the fact that we executed a C function that is proven to behave in the same way as this function.

Got it, thanks for the clarification!

khieta · 2024-04-17T15:19:00Z

Coq/EC/ECEqProof.v

+  Variable felem_from_bytes : Vector.t bool 384 -> F.
+  Variable felem_to_bytes : F -> Vector.t bool 384.
+  Hypothesis felem_from_to_bytes_inv : forall x, felem_from_bytes (felem_to_bytes x) = x.
+  Hypothesis felem_to_from_bytes_inv : forall x,  felem_to_bytes (felem_from_bytes x) = x.


Add explanation for these variables and hypotheses

Added comments. I also removed the second Hypothesis because it is not necessary, and also probably not true for the conversion routines supplied by fiat-crypto and s2n-bignum.

khieta · 2024-04-17T15:19:27Z

Coq/EC/ECEqProof.v

+  Variable F_order_correct : nat -> Prop.
+  Context `{F_FiniteField : @FiniteField F_order_correct F Feq _ _ _ _ _ _ _ _ F_field}.
+  Hypothesis p384_field_order_correct : F_order_correct p384_field_order.


Add explanation for these variables and hypotheses

Added a comment.

khieta · 2024-04-17T15:29:03Z

Coq/EC/Util.v

+Theorem sub_eq_mono : forall x1 x2 y1 y2,
+  x1 = x2 ->
+  y1 = y2 ->
+  (x1 - y1)%nat = (x2 - y2)%nat.


Several of the lemmas in this file seem like they could be discharged by builtin tactics like lia. Are you separating them out for performance reasons?

Lemmas like this are only used to help me structure proofs of other facts. In the case of this lemma, if I have a goal like x1 - y1 = x2 - y2, I can apply this theorem to replace it with goals x1 = x2 and y1 = y2. I could accomplish the same thing with Ltac or rewriting (in some cases), but applying a theorem is often simpler.

khieta · 2024-04-17T15:33:34Z

Coq/EC/EC_P384_Abstract_Model_equiv.v

+  Variable point_double : point -> point.
+  Variable point_add : bool -> point -> point -> point.
+  Variable sign_extend_16_64 : (bitvector 16) -> (bitvector 64).
+  Variable point_id_to_limb : (bitvector 16) -> (bitvector 64).
+  Variable F_cmovznz : (bitvector 64) -> F -> F -> F.
+  Variable select_point_loop_body : (bitvector 64) -> point -> (bitvector 64) -> point -> point.
+  Definition double_add_body_abstract := @double_add_body_abstract Fopp F_cmovznz select_point_loop_body 
+    point_add point_double sign_extend_16_64.
+  Definition select_point_abstract := @select_point_abstract select_point_loop_body.
+
+  Hypothesis F_cmovznz_equiv : forall x y z,
+    F_cmovznz x y z = if (bvEq _ x (intToBv 64 0)) then y else z.
+
+  Hypothesis select_point_loop_body_equiv : forall w x y z,
+    select_point_loop_body w x y z = 
+       if (bvEq _ y w) then z else x.
+
+  Hypothesis point_add_jac_eq : forall (a b: Curve.point) a' b',
+    jac_eq (fromPoint a) (seqToProd a') ->
+    jac_eq (fromPoint b) (seqToProd b') -> 
+    jac_eq (fromPoint (Curve.add a b)) (seqToProd (point_add false a' b')).
+
+  Hypothesis point_add_mixed_eq : forall (a b:Curve.point) a' b',
+    nth_order b' two_lt_three = Fone -> 
+    jac_eq (fromPoint a) (seqToProd a') ->
+    jac_eq (fromPoint b) (seqToProd b') -> 
+    jac_eq (fromPoint (Curve.add a b)) (seqToProd (point_add true a' b')).
+
+  Hypothesis point_double_minus_3_jac_eq : forall (p:Curve.point) p',
+      jac_eq (fromPoint p) (seqToProd p') ->
+      jac_eq (fromPoint (Curve.double_minus_3 p)) (seqToProd (point_double p')).
+
+  Hypothesis sbvToInt_sign_extend_16_64_equiv : forall x,
+    sbvToInt _ (sign_extend_16_64 x) = sbvToInt _ x.


Add explanation for these variables and hypotheses

(Similar comment for other uses of Hypothesis in this file, but wanted to avoid spamming comments.)

I added some comments and re-organized the file a bit. Many of these variables/hypotheses are internal to the proof, and they are replaced with concrete terms and proofs in ECEqProof.v. Let me know if more documentation is needed to make all this clear.

Thanks, the new re-org and comments are useful.

apetcher-amazon added 25 commits December 27, 2023 19:09

Verified validation of P-384 base point table.

fe488ab

Minor fixes

48fe2ff

Base point table validation proof complete, but can't close the Secti…

023c5a1

…on. Working on improving the organization.

Still improving proof and trying to close Section.

4be47e4

Need to reorginize files.

30df4c8

Proof re-organization in progress

1e38fe4

Factored out some curve stuff into a type class.

85b5c5d

Factoring out curve parameters/facts

6eb6222

Improved organization. Still can't close section.

7e29f72

Proof works. Need ot go back and clean up assumptions.

cf935c1

Minor improvements to assumptions.

859ee8a

Adding SAW proof for ECDH output conversion

90c3446

Merge branch 'p384_validate_2' of github.com:apetcher-amazon/aws-lc-v…

66f67df

…erification into p384_validate_2

Moving ECDH spec into Cryptol file.

5c72740

Some work on inverse square operation.

03f315e

Merge branch 'p384_validate_2' of github.com:apetcher-amazon/aws-lc-v…

013fd29

…erification into p384_validate_2

Correctness of Jacobian to affine conversion

5fe9b11

Re-structured to remove an admission.

acd2d05

Small comment change.

0f9c2fb

Added constant validation to scripts

f4d8d66

Improved assumptions on pre-computed table of multiples of the base p…

94cdb67

…oint.

Improvements to assumptions related to field order.

00e617c

Improvements to finite field definition.

0f92eb9

Updating documentation

7630c6b

Cleaning up proof a bit.

31fff76

apetcher-amazon requested review from andrewhop and pennyannn as code owners March 28, 2024 17:44

apetcher-amazon added 3 commits March 29, 2024 09:27

Merge remote-tracking branch 'upstream/master' into p384_validate_2

c1150bb

Fixing a couple of bugs

df4d524

Added test for hard-coded Montgomery "1" element, and removed an extra

3515ff4

patch in a script.

pennyannn reviewed Apr 2, 2024

View reviewed changes

SAW/proof/EC/EC_P384_validate.saw Show resolved Hide resolved

SAW/spec/EC/EC_mul.cry Outdated Show resolved Hide resolved

README.md Show resolved Hide resolved

apetcher-amazon added 3 commits April 8, 2024 12:18

Added verification of test for P-384 one value.

f159c0a

Added SAW proof for top-level constant validation function.

f5dad26

Moving ECDH derive spec to its own file.

57dec43

apetcher-amazon changed the title ~~Imrovements to formal verification of P-384~~ Improvements to formal verification of P-384 Apr 8, 2024

apetcher-amazon added 3 commits April 8, 2024 16:02

Improvement to README

65d26d0

Fix to Coq Dockerfile.

691274b

Fixing a Cryptol->Coq extraction issue.

d9cb16d

pennyannn reviewed Apr 9, 2024

View reviewed changes

Coq/EC/EC_P384_Abstract_5_equiv.v Show resolved Hide resolved

Adding a top-level comment to one of the Coq files.

b5bb507

khieta approved these changes Apr 17, 2024

View reviewed changes

Some documentation and organization improvements.

0225789

pennyannn approved these changes Apr 19, 2024

View reviewed changes

Upading src submodule

72c8dc6

apetcher-amazon merged commit fbcf31b into awslabs:master Apr 22, 2024
4 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Improvements to formal verification of P-384 #141

Improvements to formal verification of P-384 #141

apetcher-amazon commented Mar 28, 2024 •

edited

Loading

pennyannn left a comment

khieta left a comment

khieta Apr 17, 2024

apetcher-amazon Apr 17, 2024

apetcher-amazon Apr 17, 2024

khieta Apr 19, 2024

apetcher-amazon Apr 19, 2024

khieta Apr 19, 2024

khieta Apr 17, 2024

apetcher-amazon Apr 18, 2024

khieta Apr 17, 2024

apetcher-amazon Apr 18, 2024

khieta Apr 17, 2024

apetcher-amazon Apr 18, 2024

khieta Apr 17, 2024

apetcher-amazon Apr 18, 2024

khieta Apr 19, 2024

Improvements to formal verification of P-384 #141

Improvements to formal verification of P-384 #141

Conversation

apetcher-amazon commented Mar 28, 2024 • edited Loading

pennyannn left a comment

Choose a reason for hiding this comment

khieta left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

apetcher-amazon commented Mar 28, 2024 •

edited

Loading