4 ms·

> Does he mean doing what Galois did [1][2] with tools like CRYPTOL [3][4]? Or something more like this [5] with EasyCrypt and CompCert? Or something simpler li

> Does he mean doing what Galois did [1][2] with tools like CRYPTOL [3][4]? Or something more like this [5] with EasyCrypt and CompCert? Or something simpler like Altran's SPARK crypto [6]? And maybe with protocol-level verification like miTLS [7]? Yes. > I don't think there's a question about whether the goals can be met so much as a lack of uptake of methods and tools that meet them. I agree. And, that's a big part of the reason I didn't spend a lot of time on formal verification when I wrote what I wrote. The target audience of my writing is people think that the result must be as fast as the fastest implementation, but that only think that formal verification of correctness is nice to have and/or impractical to the point of not being worth trying. That isn't my own personal prioritization, but I think that actually describes the prioritization of almost everybody deploying open source crypto software today. Anyway, I hope to have more to say about formal verification of ECC implementations later.

nickpsecurity 11y ago
Well, best response I've seen to a post like this. The audience you refer to might be best served with a SPARK, Frama-C, etc. implementation decomposed as much as possible with experts doing the DbC annotations or VCC's. More likely an informal method. In the distant past, my method was to use a language with compile-time macro's to decompose the overall algorithm into simplest functions. In dev mode, I could manually run checks to hopefully ensure my assumptions were correct. Each module was simple enough to extensively test and spot coding defects. If necessary, I could do it at ASM level while wrapping low-level stuff in HLL calls w/ checks. In production mode, it compiled to straight-forward, high-performance, low-level code. So, two routes with different levels of formality and optimization. The 2nd method is more likely to get adopted. Just not sure how many weird corner cases can be prevented that way.

nickpsecurity 11y ago

Well, best response I've seen to a post like this. The audience you refer to might be best served with a SPARK, Frama-C, etc. implementation decomposed as much as possible with experts doing the DbC annotations or VCC's. More likely an informal method. In the distant past, my method was to use a language with compile-time macro's to decompose the overall algorithm into simplest functions. In dev mode, I could manually run checks to hopefully ensure my assumptions were correct. Each module was simple enough to extensively test and spot coding defects. If necessary, I could do it at ASM level while wrapping low-level stuff in HLL calls w/ checks. In production mode, it compiled to straight-forward, high-performance, low-level code. So, two routes with different levels of formality and optimization. The 2nd method is more likely to get adopted. Just not sure how many weird corner cases can be prevented that way.