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
gfverif's way of doing quick and dirty verification of existing C code is somewhere between genius and madness - define a new "mockup" integer type and use C++ to overload the operators like plus or minus, instead of doing calculations, it generates SageMath scripts of equivalent operations in algebra. This way, the entire C algorithm can be automatically extracted without writing any parser or compiler... The only problem: conditional branches using data are not supported, but you're not supposed to do that in crypto anyway... 🤣
Bignum addition code for PDP-11 has been formally verified by CBMC automatically in 0.2 seconds, showing its equivalence to the reference implementation. It also verified that a carry cannot occur after a specific addition, magic! Now trying to see whether it could handle multiplication... I don't expect success, the SMT solver will probably get stuck somewhere...
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.
Verifying the complied Cryptoline assembly code from C, which itself is a model of the PDP-11 assembly code, is a futile attempt. After C optimization, logic is different and useful invariants disappear. New idea: write an assembler to convert PDP-11 assembly directly to the Cryptoline verification language - both are at the assembly level and should be easier to work with.
I still have difficulties on verifying the full PDP-11 multiplication routine. Arguing with #Singular on the correctness of the math is not fun at all - the actual equation it's verifying looks like this... Good luck if the output is not zero. This is how humanity ends.
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...
Just verified 800 lines of unrolled PDP-11 assembly code for 120 x 120 = 240 bit bignum multiplication using the #Cryptoline verification tool and my script. This routine uses 16-bit words to represent radix-15 integers, correctness is not obvious. It's amazing that #Singular can solve these crazy equations in 0.1 seconds.
Finished formal verification for PDP-11 column-wise (Comba) bignum multiplication, should be 20% faster than row-wise multiplication. The messy macro assembly macros are difficult for humans to audit, but not a problem for #Cryptoline, #Boolector and #Singular. Next step: implementing and verifying Karastuba multiplication.
@niconiconi I'd have guessed, it's because of possible interference with ADC (add with carry) instruction, but IDK, ADD unlike ADC.
@amiloradovsky I thought about it too, the 17-bit integer is simulated using 32-bit word, it should never carry out, and ADD ignores the carry flag. Perhaps it's useful on other architectures. Still, I can't think of a computer that doesn't allow you to ignore the carry flag, other than the 6502.
@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?
@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 this looks immensely useful to me. i know enough crypto to know how easy it is to fake but i keep getting tasked with evaluating draft implementations.
@EWings The usual way is implementing and verifying everything in a very-high-level functional programming language. Model-checking tools for C programs also exists. Cryptoline is a domain-specific tool for low-level crypto code.
@EWings I just started looking for verification tools for cryptography since a week ago. I don't know any more than you...