Interesting, DJB and Peter Schwabe have a demo program for verifying the correctness of finite-field arithmetic in Curve25519 code, it's almost fully automatic, only needs minimum annotations. It simply extracts the calculation you are trying do to, generates a SageMath script, and calls SageMath to crosscheck the math. Not real "formal verification", but certainly better than staring at the screen with pen and paper...

Perhaps it's really possible to hack the code and use it to verify my PDP-11 assembly code. http://gfverif.cryptojedi.org/index.shtml

Follow

Cryptoline looks like the most complete solution for verifying crypto code for now. But the toolchain couldn't fully understand bitwise operations. A simple add routine requires 83 TODO items.

GCC optimizes an 1-bit leftshift on a 17-bit integer to...

addl %eax, %eax

andl $0x1FFFE, %eax

The unused top 15 bits are cleared, which makes sense. But why does it clear the 0th bit too? It's guaranteed to be 0 unless my understanding of a computer is horribly wrong. Spent 20 minutes on this question... I was overthinking it, it's probably just a meaningless compiler artifact.

Ha! Problem solved. The formal verification was failing because my code has a typo!

#Singular: I told ya so but you didn't believe me...

@niconiconi I'd not heard of Cryptoline before, and when I search for it, I get pages full of bitcoin related websites.

Do you have a link to a site that describes this tool?

Thanks.

@niconiconi Thanks!!

@vertigo The previous paper describes the verification of C programs by a LLVM IR translator. For the underlying Cryptoline verification language, also see https://www.iis.sinica.edu.tw/papers/byyang/21728-F.pdf

As someone with zero knowledge on formal verification, I'm really surprised by its usability. Everything is designed specifically for finite field bignum code in public-key crypto. You can simply write pre/post conditions in high-level algebraic statement, like "assert a + b = c (mod n)" and the tool handles the rest.

@niconiconi Does this kind of tools only exists for assembly languages? Just being curious.

@niconiconi Ah I see. Was trying to change the "write it and let it run" way of programming recently so this kind of things are interesting.

niconiconi@niconiconi@cybre.spaceStill can't understand the purpose of adding precondition and postcondition to bitshift instructions... Time to start nagging the researchers with my clueless emails.