4 ms·

I hear this claim a lot but I question it's truth. I'm faster with formal tools than without. For instance, this week I needed to build a distributed locking m

I hear this claim a lot but I question it's truth. I'm faster with formal tools than without. For instance, this week I needed to build a distributed locking mechanism so a collection of asynchronous actors could only access resources in one region at a time. I described my two requirements in TLA+: only one zone at a time, and everyone who wants a zone eventually gets it (with the assumption nobody goes down forever - weak fairness.) I had several bugs which it caught, until I finally arrived at a protocol that was proven correct (at least for a handful of workers on a handful of zones.) It took around a day from start to finish, and now I know my design is literally flawless. Sure, I didn't prove it in the general case, nor did I prove that my code implements the spec, but this was still extremely useful! Having the machine check your designs frees you from worrying if you've caught all the races and corner cases.

tptacek 7y ago
You can easily convince me that formal methods are more efficient for complex distributed systems problems, or for cryptographic protocols, or things like that. But even in systems whose whole premise is algorithmic, the hairy stuff provers are designed against are a small part of the overall coding task. And for the kind of security this article is talking about, it's not enough to have a proven core algorithm or protocol; your dumb input parsers and output renderers and all that other boring integration code also needs to be bug-free, because those kinds of joinery are where we tend to find vulnerabilities.
- danmaz74 7y ago
  Indeed. What is unbearably slow is creating the whole software with formal verification, not just the core algorithm.
drdrey 7y ago
TLA+ doesn't prove anything to be "correct" or "flawless", I find it extremely worrisome that you claim as much. It failed to exhibit traces that violated your invariants, which says something completely different.
- p0llard 7y ago
  I've never actually used TLA+, but my understanding is that it does exhaustive model checking (presumably using some suitable simulation relation), so in this case failure to find a violating trace indicates that no such trace exists, and the invariants always hold. Correctness might well be defined solely by a set of invariants, so I don't quite understand your point here?
  - hwayne 7y ago
    This is correct: the TLA+ model checker (TLC) will check all possible behaviors for the finite model. As the GP said, they were only working with a finite number of workers, but within those constraints it guarantees the spec always satisfies the invariants. (This is of course assuming that TLC doesn't have any bugs that would cause it to misreport. By contrast something like randomized testing doesn't guarantee the spec satisfies the invariants even if the tester is bug-free.)
    - sterlind 7y ago
      exactly. I've proven that in a scenario with a certain number of zones and workers, the invariants and temporal properties cannot be violated. With more work, I could prove the invariants for any number of workers and zones using TLAPS rather than TLC, though I couldn't prove the temporal properties in this way (since TLAPS doesn't support temporal logic, it can only prove invariants.)
  - drdrey 7y ago
    Imagine the following scenario, you have encountered an actual bug in concurrent code, and you think it would be great to work on a model and invariants that lets TLA+ find the bug (as an exercise). So you start writing a model, and a set of invariants, you run the tool and... it finds nothing. Does that mean you just proved the bug does not exist? No, you _know_ the bug exists, what it means is that you didn't write a correct model on your first try. So you iterate on it, add a few things you missed, put some extra labels, read the docs a bit more, maybe refine your invariants, make them stronger, work through a couple traces that don't actually make sense in practice (e.g. actors just never taking any action whatsoever). During all this time, you either found nothing or things that were not interesting. At no time have you ever proved anything correct, you just iterated on your model until you managed to capture a real life scenario. It takes some convincing to make the jump from "this model does not violate my invariants" to "I think this model and the invariants are close enough to what I care about that I think it's good enough"... I don't know how to go from there to things like "proven correct" and "flawless".

tptacek 7y ago

You can easily convince me that formal methods are more efficient for complex distributed systems problems, or for cryptographic protocols, or things like that. But even in systems whose whole premise is algorithmic, the hairy stuff provers are designed against are a small part of the overall coding task. And for the kind of security this article is talking about, it's not enough to have a proven core algorithm or protocol; your dumb input parsers and output renderers and all that other boring integration code also needs to be bug-free, because those kinds of joinery are where we tend to find vulnerabilities.

danmaz74 7y ago
Indeed. What is unbearably slow is creating the whole software with formal verification, not just the core algorithm.

drdrey 7y ago

TLA+ doesn't prove anything to be "correct" or "flawless", I find it extremely worrisome that you claim as much. It failed to exhibit traces that violated your invariants, which says something completely different.

p0llard 7y ago
I've never actually used TLA+, but my understanding is that it does exhaustive model checking (presumably using some suitable simulation relation), so in this case failure to find a violating trace indicates that no such trace exists, and the invariants always hold. Correctness might well be defined solely by a set of invariants, so I don't quite understand your point here?
- hwayne 7y ago
  This is correct: the TLA+ model checker (TLC) will check all possible behaviors for the finite model. As the GP said, they were only working with a finite number of workers, but within those constraints it guarantees the spec always satisfies the invariants. (This is of course assuming that TLC doesn't have any bugs that would cause it to misreport. By contrast something like randomized testing doesn't guarantee the spec satisfies the invariants even if the tester is bug-free.)
  - sterlind 7y ago
    exactly. I've proven that in a scenario with a certain number of zones and workers, the invariants and temporal properties cannot be violated. With more work, I could prove the invariants for any number of workers and zones using TLAPS rather than TLC, though I couldn't prove the temporal properties in this way (since TLAPS doesn't support temporal logic, it can only prove invariants.)
- drdrey 7y ago
  Imagine the following scenario, you have encountered an actual bug in concurrent code, and you think it would be great to work on a model and invariants that lets TLA+ find the bug (as an exercise). So you start writing a model, and a set of invariants, you run the tool and... it finds nothing. Does that mean you just proved the bug does not exist? No, you _know_ the bug exists, what it means is that you didn't write a correct model on your first try. So you iterate on it, add a few things you missed, put some extra labels, read the docs a bit more, maybe refine your invariants, make them stronger, work through a couple traces that don't actually make sense in practice (e.g. actors just never taking any action whatsoever). During all this time, you either found nothing or things that were not interesting. At no time have you ever proved anything correct, you just iterated on your model until you managed to capture a real life scenario. It takes some convincing to make the jump from "this model does not violate my invariants" to "I think this model and the invariants are close enough to what I care about that I think it's good enough"... I don't know how to go from there to things like "proven correct" and "flawless".