formosa-crypto / formosa-mlkem

Other
11 stars 7 forks source link

fix poly_decompress: read out of bounds #17

Closed tfaoliveira closed 9 months ago

tfaoliveira commented 9 months ago

originally proposed here: https://github.com/formosa-crypto/libjade/commit/d05492d5eab67c86733b5e841d910bc353f1b38d

TODO proofs; I'm will be unable to fix the proofs. @vbgl ? @MQuaresma ? thanks!

vbgl commented 9 months ago

I’ll give a look at the proof.

vbgl commented 9 months ago

I think I’m done fixing the proof. Let’s wait for EasyCrypt to double-check.

CI job: https://github.com/vbgl/hakyber/actions/runs/7813196009/job/21311837128