Re: [Ufmrg] bugs in formal methods software

[Nadim Kobeissi <[e-mail]>]

Dear Gergely,

Ahh, how to answer this! The bugs that I've seen are rather mostly anecdotal, I'm afraid. I suspect this is largely because of the way formal methods tools tend to be used:

1. If you find a bug in a formal methods tool, it's likely because you're one of the very few people doing something very advanced or unusual with it.
2. If you're doing something advanced or unusual with a formal methods tool, you are almost certainly in a Slack or Zulip with its creators. (It's impossible to learn how to use EasyCrypt or F* to do something advanced otherwise, that's just the truth!)
3. If you find the bug, you're likely to report it then and there, and it gets patched rather informally, again, given the size of the user base and the academic nature of the tooling.

Some anecdotes I can share:
1. I remember a long time ago an early version of CryptoVerif mixed namespaces: you could have two `let`s in different scopes and if the variable name matched, you'd get mixing. This was fixed rather quickly in 2015 if I recall correctly.
2. At one point, there was an F* build that forgot the commutative property of addition. i.e. a + b == b + a returned false. I remember that was a funny moment and it was also fixed quickly.
3. Tons of subtle issues with ProVerif that led to crashes, eating up all the RAM, etc. -- most of these were discovered due to our work back in the day on modeling Signal [1] and Noise [2] in ProVerif, and Bruno's team released, as a result, major updates to ProVerif which shortened the analysis time of our Noise models in once instance from 170 hours to 20 minutes [3]

There are also a bunch of stories about bugs in Coq, but again, I ran past those in real life while working at Inria, and it wasn't a sort of situation where they were documented anywhere.

Of course, Verifpal has probably had more bugs than any other three formal analysis tools combined! Although the bug that Usama mentions (found during the Eurocrypt 2022 workshop) was indeed amply documented [4] and an update was released with credit to Oskar Goldhahn, who found the bug [5]. Luckily the bug was only due to some ill-thought code optimization that I dreamt up that I thought would make analysis faster. The optimization was promptly removed.

Unrelatedly, Verifpal has really painted itself into a corner due to its extreme focus on acting as a learning tool and ease of use: the language is so small and inexpressive that at this point it can never be used to reason protocols in a truly nuanced way, and the analysis logic is inspired by the language (Chomsky was right? [6]) I also think it was a mistake to write it in Go, but what can you do. I still get really excited when it's used in undergraduate courses, and I was nutty enough to ship a manual with a full-blown manga of Verifpal punching bad guys. [7]

It's important to remember that in the end, all of this stuff is software, too. Software verifies software (or logical representations), but who verifies the verifiers? You've got to put your trust somewhere, which is why, anyway, I've always advocated for making models easier to read: if the modeling tool/language is so complex that the tool itself (Be it EasyCrypt, Tamarin, whatever) can check the model, but you (or others) can't even read it, then what's the point? You're just blindly trusting that software at that point, and Haskell/OCaml code ain't perfect, either.

It's fun to talk about this stuff, I hope we can have more discussions like this!

References:
[1] https://bblanche.gitlabpages.inria.fr/proverif/publications/KobeissiBhargavanBlanchetEuroSP17.html
[2] https://noiseexplorer.com 
[3] https://bblanche.gitlabpages.inria.fr/proverif/publications/BlanchetEtAlSP22.html
[4] https://github.com/symbolicsoft/verifpal/commit/eeaed68fecae463b3fbb9f57357591d5e73b9df0
[5] https://github.com/symbolicsoft/verifpal/commit/dad640afa0ff544b6f0d0e960ec3c49130a9e4b5
[6] https://en.wikipedia.org/wiki/Language_and_thought
[7] https://verifpal.com/res/pdf/manual.pdf

On Fri, Sep 8, 2023, at 5:31 PM, Muhammad Usama Sardar wrote:
> Hello Gergely, 
> 
> One of these bugs was found in Verifpal by one of the trainees during the tutorial in Eurocrypt 2021. I don't find it documented, though. 
> 
> 
> 
> ------------------------------------------------------------------------------------------------------------------------------------------
> Best Regards, 
> Muhammad Usama Sardar (M.Sc.)
> 
> Research Associate
> 
> Technische Universität Dresden
> 
> 
> 
> Faculty of Computer Science
> 
> Institute of Systems Architecture
> 
> Chair of Systems Engineering
> 
> 
> 
> Office: APB 3073
> 
> Phone: [phone]
> 
> Email: [e-mail]
> 
> Website: https://tu-dresden.de/ing/informatik/sya/se/die-professur/beschaeftigte/muhammad-usama-sardar
> 
> ------------------------------------------------------------------------------------------------------------------------------------------
> 
> 
> *Von:* Ufmrg <[e-mail]> im Auftrag von Gergely Buday <g.buday=[e-mail]>
> *Gesendet:* Freitag, 8. September 2023 15:39:55
> *An:* [e-mail]; [e-mail]
> *Betreff:* [Ufmrg] bugs in formal methods software
>  
> Dear Nadim
> 
> at the interim meeting you were talking about discovered bugs in formal methods software for security protocols.
> 
> Could you please tell us a few words about these as it is interesting: what kind of bugs are these, where can we read about them and how they influence the use of these tools?
> 
> Yours
> 
> - Gergely

Nadim Kobeissi
Symbolic Software • https://symbolic.software