Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Make the ref implementation accepted by the safety checker #4

Open
wants to merge 4 commits into
base: master
Choose a base branch
from
Open

Make the ref implementation accepted by the safety checker #4

wants to merge 4 commits into from

Conversation

vbgl
Copy link
Contributor

@vbgl vbgl commented Mar 9, 2023

The changes in this PR and the changes to the safety checker enabling annotations (jasmin-lang/jasmin#362) make the safety analysis of the keypair function go through.

Quick measurements show that these changes have no impact on the run-time performance (this REF version is already quite slow).

I’ve no clue about what impact they may have about the correctness proofs.

@vbgl vbgl marked this pull request as draft March 10, 2023 07:10
@vbgl
Copy link
Contributor Author

vbgl commented Mar 10, 2023

I may have a different workaround for NTT: tweak the safety checker (jasmin-lang/jasmin#384) rather than changing the analyzed program.

@vbgl
ref: tighter loop bounds
dc0cd28
@vbgl
ref/gen-matrix: explicitly initialize the “poly” array
c4ad140
@vbgl
ref/gen-matrix: rework loop condition in rej_uniform
5be30db 
When the destination array rp is full, the loop nonetheless continues to
completely consume the buf array. There is no longer an early exit, and
the loop will always iterate 56 times.
@vbgl
ref: annotate loops to guide the safety checker
511a108 
With these annotations, the key generation function can be proved safe
by the automatic safety checker.

The “no-termination-check” annotation in gen-matrix acknowledges that
proving (propabilistic) termination of this loop is beyond the scope of
the automated checker and must be justified by other means.
@vbgl vbgl changed the title Make ref_keypair accepted by the safety checker Make the ref implementation accepted by the safety checker Mar 13, 2023
@vbgl vbgl marked this pull request as ready for review March 13, 2023 12:09
@vbgl
Copy link
Contributor Author

vbgl commented Mar 13, 2023

With small fixes & improvements to the safety checker (jasmin-lang/jasmin#384, jasmin-lang/jasmin#387), the three main entrypoints of the ref implementations can be verified for safety with the changes made in this PR:

  • in gen-matrix , an early exit has been removed; this will impact the proof, but should be doable;
  • in the same procedure, an array is now explicitly initialized; this increases the code size, but the run-time effect of this change should not be a concern;
  • the rejection-sampling loop is annotated with #no_termination_check, meaning that it is not the duty of the automatic checker to prove termination (note that this loop almost surely terminates);
  • a few loop guards are made tighter: this is a syntactic change that allows the widening heuristic to make better guesses;
  • a few loops are annotated with #bounded, to tell the analyzer to unroll them: this is required for loops that initialize arrays.

Beware that safety analysis is costly. Witnesses report about 6h of computation for keypair and nearly 16h for decaps, encaps being somewhere in between.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
1 participant
@vbgl