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

Kyber: add F* proofs #161

Merged
merged 118 commits into from
Jan 12, 2024
Merged

Kyber: add F* proofs #161

merged 118 commits into from
Jan 12, 2024

Conversation

W95Psp
Copy link
Contributor

@W95Psp W95Psp commented Jan 9, 2024 •
edited by karthikbhargavan
Loading

This PR adds a new directory extraction-edited to proofs/fstar/ with a set of proof for the Kyber implementation.
The code in this new directory started as a snapshot of the generated F* code in proofs/fstar/extraction but has been hand edited with annotations, invariants, pre- and post-conditions, as well as a functional specification of Kyber.

The proofs currently check the following:

  • all the modules are proved to be panic-free
  • modular arithmetic are functionally verified (Libcrux.Kem.Kyber.Arithmetic)
  • constant-time operations are functionally verified (Libcrux.Kem.Kyber.Constant_time_ops)
  • the functions implementing IND-CPA encryption, and the IND-CCA KEM are functionally verified
  • part of serialization and NTT are functionally verified; in particular, we prove that all range assumptions hold, and that there are no arithmetic overflows
  • secret independence is partially verified (in particular, division with secret inputs is forbidden)

However, some parts remain, and we are adding open issues to track them and will address them in future PRs.

  • full functional correctness for NTT, matrix operations, and serialization
  • secret independence for the whole code

In further future work, we will seek to address the following:

  • minimize diffs between extraction-edited and extraction by propagating pre- and post- conditions and meaningful annotations to the source Rust code
  • put the proofs and the proof-related patch in extraction-edited under CI
  • re-verify any recent changes to the Rust code

karthikbhargavan and others added 30 commits December 1, 2023 11:41
@karthikbhargavan
local cache in make
14bc9b7
@karthikbhargavan
first set of modules
92426d1
@karthikbhargavan
first set of modules
8e35cc9
@karthikbhargavan
CI friendly makefile
bdea39e
@karthikbhargavan
ind-spa panic free with assumes
d84a265
@karthikbhargavan
passing over a few more modules
b701df3
@karthikbhargavan
Constant_time_ops panic free
448a156
@karthikbhargavan
more modules towards panic freedom
abcea42
@karthikbhargavan
snapshotting extraction to enable diff with generated code
c6730ea
@karthikbhargavan
serialize to p-f with assumes
5789134
@karthikbhargavan
putting hand-edited extraction folder in parallel
4464295
@karthikbhargavan
fix renaming
dbb692b
@karthikbhargavan
sprinked admits to finish p-f pass
6461981
@karthikbhargavan
added spec, linked to kyber768, proof for one module
adaa30c
@karthikbhargavan
ind-cca spec
a80528a
@karthikbhargavan
ind-cca spec
a8d51f8
@karthikbhargavan
fix a type error
0f87924
@karthikbhargavan
ind-cpa interface
4d559e2
@karthikbhargavan
ind-cca verified
244fefe
@karthikbhargavan
wip
3283b89
@franziskuskiefer @msprotz @karthikbhargavan
kyber crate extraction script (#136)
f7bdccf 
* script to extract kyber as crate
* Make sed invocation portable

---------

Co-authored-by: Jonathan Protzenko <[email protected]>
@karthikbhargavan @franziskuskiefer @xvzcf
Verify Kyber Fstar extraction using strict and lax typechecking. (#140)
3fce1f5 
* run hax on proof changes

* Add lax and strict typechecking to the CI.

---------

Co-authored-by: Franziskus Kiefer <[email protected]>
Co-authored-by: xvzcf <[email protected]>
@franziskuskiefer @karthikbhargavan
refactor ind_cpa
c516b42
@franziskuskiefer @karthikbhargavan
refactor ntt for proofs
4af02d5
@franziskuskiefer @karthikbhargavan
refactor serialize for proofs
62895a2
@franziskuskiefer @karthikbhargavan
drop UpdatableArray
57693f4
@xvzcf @karthikbhargavan
Refactoring ind_cpa.rs
307b15d
@franziskuskiefer @karthikbhargavan
cleanup and pulling types to the kem
7f9eddf
@franziskuskiefer @karthikbhargavan
fix verification
812036f
@karthikbhargavan
removed Conversions from the generated F* and Makefile
2e6e3ff
@W95Psp W95Psp changed the base branch from dev to lucas/fstar-add-interfaces January 9, 2024 16:33
@W95Psp W95Psp changed the base branch from lucas/fstar-add-interfaces to dev January 9, 2024 16:34
franziskuskiefer
franziskuskiefer reviewed Jan 10, 2024
View reviewed changes
Copy link
Member

@franziskuskiefer franziskuskiefer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks like this needs to be rebased and cleaned up a little.
Is there another reason this is a draft?

specs/kyber/src/ind_cpa.rs Outdated Show resolved Hide resolved
src/kem/kyber/helper.rs Outdated Show resolved Hide resolved
This was referenced Jan 10, 2024
Open
Closed
Closed
@karthikbhargavan karthikbhargavan marked this pull request as ready for review January 10, 2024 20:40
@franziskuskiefer franziskuskiefer linked an issue Jan 11, 2024 that may be closed by this pull request
Panic Freedom for Kyber #142
Closed
16 tasks
@W95Psp
Copy link
Contributor Author

W95Psp commented Jan 11, 2024

I disabled CI for now on extraction-edited, see #168.

franziskuskiefer
franziskuskiefer approved these changes Jan 12, 2024
View reviewed changes
Copy link
Member

@franziskuskiefer franziskuskiefer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, let's get this in.
Not sure if you want to update the PROOFS.md before merging.

@karthikbhargavan
Copy link
Contributor

Ok, let's get this in. Not sure if you want to update the PROOFS.md before merging.

That file was out of date, so I removed it. The comments on this PR and the remaining issues are the ones that are most relevant.

@franziskuskiefer franziskuskiefer merged commit 16a3a7f into dev Jan 12, 2024
15 checks passed
@franziskuskiefer franziskuskiefer deleted the dev_proofs branch January 12, 2024 13:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@franziskuskiefer franziskuskiefer franziskuskiefer approved these changes

Assignees
No one assigned
Labels
None yet
Projects
libcrux
Status: ✅ Done
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Panic Freedom for Kyber
4 participants
@W95Psp @karthikbhargavan @franziskuskiefer @xvzcf