vbgl
commented
5 months ago I’ve run the SCT checker on all .jazz files in the main branch of libjade. Only the following files are accepted (probably because the other ones lack initial fences or things like that):
./crypto_scalarmult/curve25519/amd64/mulx/scalarmult.jazz ./crypto_scalarmult/curve25519/amd64/ref5/scalarmult.jazz ./crypto_scalarmult/curve25519/amd64/ref4/scalarmult.jazz ./crypto_kem/xwing/amd64/ref/kem.jazz ./crypto_kem/xwing/amd64/avx2/kem.jazz ./crypto_kem/mlkem/mlkem768/amd64/ref/kem.jazz ./crypto_kem/mlkem/mlkem768/amd64/avx2/kem.jazz
All these files are still accepted by the sct checker after this PR. Comparing the results is a bit tricky as many type variables differ (say ?31026 becomes ?30964). There are a few real changes though, e.g., nomodmsf __init_points4 : #poly = { n = ?243, s = ?242} -> #public * #public * #poly = { n = ?243, s = ?242} * #public becomes nomodmsf __init_points4 : #poly = { n = ?233, s = secret} -> #transient * #public * #poly = { n = ?233, s = secret} * #transient.
Lessons learned:
- the inferred types are indeed smaller but that seems OK in practice
- the output of the checker must be polished.
Stack-variables are now considered transient before initialization. Indeed and in particular after a few compilation passes, stack variables may contain secrets before their initialization. When (mis)speculative execution can bypass initialization, said secret can be exposed.
See new test file for a precise example illustrating the issue.