Fix tests when "special context of execution" is not provided
Opened this issue · 2 comments
Just an issue to track this recurring issue better: ocaml/opam-repository#16212 (comment)
As I said, I'd be really happy to see this resolved. It would make our life 10x better.
An interesting resource exists to check our assertions: https://eprint.iacr.org/2016/1123.pdf
But I tried locally to reproduce their result and... it does not work. Then, I don't think that it's the good way when, on our side, we want to check that our function are constant-time and on their side, they want to check that the given function is not constant-time.
The abstract interpretation implemented into gas-eqaf seems the more "deterministic" way to check if our function are in constant time.
The issue still is open because we must assert our behavior but again, the check/check.exe is too fragile to be systematically exploitable (specially into a CI context). I removed the check/check.exe test to help me about the release process and, on the other side, a PR should not be easy to merge and must have a review by hands.
Until we does not have a better CI for eqaf, this is the best solution.