Follow

Oh no, the program correctness verifier has SIGSEGVed and crashed. "You've become the very thing you swore to destroy"...

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...

Show thread

As expected, the MiniSAT solver gets stuck when attempting to formally verify the PDP-11 multiplication routine via CBMC, 20 minutes and it's still running... Meanwhile, Z3 solved it in 5 minutes, magic! I, for one, welcome our new Microsoft overlord...

Show thread

Deliberately "unfixed" a carry bug in the code, CBMC was able to catch it in 5 minutes using the Z3 solver.

Show thread

Added a tricky optimization, saves 2 cycles, but I'm afraid it's sometimes wrong. But CBMC proved its correctness, magic.

Someone should make a video tutorial on formal verification and name it "Bugs DESTROYED by FACTS and LOGIC!11!" Of all things that use this stupid meme, this will be the only legit one...

> size of program expression: 50300 steps

> Generated 8194 VCC(s)

> Running SMT2 QF_AUFBV using Z3

I don't think the solver is able to answer this huge problem. Anyway, I'll know when I wake up tomorrow...

@niconiconi 之前上课的时候请外面的人来讲他们搞形式证明就是用的他们自己搞的C parser。这里直接不要parser就很有意思。

niconiconi@niconiconi@cybre.spacegfverif'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... 🤣