3 ms·
Regarding (c), if your program is written say Agda[1], the code can come with a proof that it has the mathematical properties you want. Or rather, your implemen
by black_knight 11y ago
Regarding (c), if your program is written say Agda[1], the code can come with a proof that it has the mathematical properties you want. Or rather, your implementation might simply be the proof.
[1] https://en.wikipedia.org/wiki/Agda_(programming_language) https://en.wikipedia.org/wiki/Agda_(programming_language)
- cvwright 11y agoThe folks at Galois have a language called Cryptol that can be used for similar things with hardware. https://galois.com/project/cryptol/ https://galois.com/project/cryptol/
- imrehg 11y agoI'd guess that (c) refers to the fact that implementation details can expose the algorithm too, e.g. side-channel attacks, leaking timing info, and so on... Things like constant-time comparisons are not generally part of the consideration of the algorithms and proofs (imho).