Why does my assembly code even work at this point?! I hope one day one doesn't need to be a PhD to formally verify it...

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. gfverif.cryptojedi.org/index.s

Show thread
Follow

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

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

Show thread

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.

Show thread

Managed to save yet another cycle with the help from the formal verifier.

Show thread

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

Show thread

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

Show thread

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

Sign in to participate in the conversation
Cybrespace

cybrespace: the social hub of the information superhighway jack in to the mastodon fediverse today and surf the dataflow through our cybrepunk, slightly glitchy web portal support us on patreon or liberapay!