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.
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.
2. If you use the model checker, it's not about it "failing to find" a counter example. A model checker result is a proof that no such example exists. True, it is usually a proof about some finite instance of your system description.
3. There is just no such thing as proving a system flawless. Software systems are physical systems exhibiting probabilistic behaviors. At best you can prove things about a mathematical description of a system, which mean that as long as the physical system behaves according to the description, the result follows. Of course, the first part at best holds with some probability.
Correctness might well be defined solely by a set of invariants, so I don't quite understand your point here?
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".
1. \A z \in Zones: Active(z) => ~\E o \in Zones: z # o /\ Active(o) 2. \A w \in Workers: \A z \in Zones: WorkerWantsZone(w, z) ~> WorkerHasZone(w, z)
Unlike your scenario, I am checking the spec here. I know that code that properly implements the spec satisfies these two properties, therefore I've proven the spec correct. You can disagree on the importance of those two properties but I've mechanically checked that those properties are always preserved in my finite models, so I know the spec is correct, at least for the model size.
You know, it's really not too hard to get started with this stuff. You can always nit-pick but why not try it out and see if it's useful for you?
(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.)
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.)
Algorithmic invariants: Many optimizations rely on certain properties being always true, so specific checks can be left out or can be replaced by other, more efficient checks. A simple example is that the distinguished idle thread is always in thread state idle and therefore can never be blocked or otherwise waiting for I/O. This can be used to remove checks in the code paths that deal with the idle thread.
https://cacm.acm.org/magazines/2010/6/92498-sel4-formal-veri...
In each, TLA+ has added significant value,
either finding subtle bugs we are sure
we would not have found by other means,
or giving us enough understanding and
confidence to make aggressive performance
optimizations without sacrificing correctness.
There is a small subdiscipline of formal methods that comes from programming language theory (judging by conferences, it makes up no more than 10-20%) that does still have this 1970s "subtext", but actual researchers or practitioners are usually careful with what they actually say, and you'll most often find such claims explicitly made only by fans.
It's all statically-checked and you can incorporate it into your CI/CD: https://pyre-check.org/docs/pysa-basics.html
See also: Property-based testing, and TLA+
Anyways, i would say those are rather different from systems where you give an actual proof of correctness.
- There's no clear definition for formal methods. One of the fundamental problems with 'formal methods' is that it's a very fragmented community of researchers and practitioners (many who never built a real-world software systems). Formal methods depends very much of who you talk with: static analysis, dynamic analysis, type systems, writing specs in Z notation, writing code in a subset of C without malloc, etc.
- Formal methods doesn't produce code: humans produce code. A side note: people forget one of the major successes of 'formal methods' is actually hardware synthesis and verification.
- Security is about risk management. Attack surfaces is a classification of some types of risk but not all. Anyway, formal methods can only help you to protect against attacks that you are already aware. None of this has anything to do with the speed which with code is being produced.
Not sure exactly what you mean here but on its face it isn’t true. Formal Methods are arguably the single best way of protecting you against attacks that you are not already aware of, by eliminating entire classes of bugs, errors or attack vectors, without regard to what type of attacks may be used against them.
Look at how little functionality seL4 provides, compared to hobbyist operating systems.
"A talented programmer can write and verify 4 lines of code a day"
seL4 has some cool ideas, but I can't stress enough how miserable it is to develop for.
Note that formal methods don't get around this as they do nothing for the class of bugs where it works as specified but now that we see it in operation we know the specification was wrong. (once the spec is right though it is faster)
Whether you've proven the right thing still requires judgement - what you end up with is a provably correct implementation of what you thought you wanted. But that's a much smaller problem, and at a minimum you're guaranteed to have an unambiguous definition of what it is you actually built.
That's my point.
Formal methods don't make bugs or debugging disappear. They move it to different domain - the development of the proof.
> what you end up with is a provably correct implementation of what you thought you wanted.
You end up with a provably correct implementation of what you thought you stated on what you thought you wanted.
Serious proofs are highly non-trivial. I've seen experts debate the exact semantics of the most simple properties.
They make the thing we usually call bugs and usually experience as debugging disappear. The thing that remains is a very different activity with very different properties.
Do you write a correct formal spec the first time round? I don't. Proofs sometimes pass or fail when they shouldn't.
When these problem occur I call them bugs, and I call process of finding and fixing them debugging.
What do you find it has in common with the activities that we normally call debugging? For me debugging is characteristically about understanding how a system is behaving, essentially by bisecting: it's all about figuring out what should be the case at each point and identifying the point at which things start to go wrong. Whereas correcting a proof is very different: you immediately know where the problem is, and it's more about coming up with a new lemma or strategy - it's the same kind of activity as writing a new proof/program, whereas (traditional) debugging is very much a separate skill, IME.
A proof can fail for many reasons, and even in the simplest possible case, where the tool provides you with a counter example it could either be a real bug in the design/program/protocol, but there could also be something wrong with the specification you were given, or in your implementation of the specification, or in some assumptions you've made to simplify the proof, or there's ambiguity in the natural language description, or even some typo somewhere.
You now need to understand the domain and the system well enough to come up with an explanation of the phenomena. This is debugging.
Formal methods don't just make bugs and debugging disappear, they just move it to a different domain - the development of the proofs.
Are you referring to the possibility of errors in your model? That's not the same thing.
It is very easy to complete a proof on the wrong model, and there are always errors in the model, at least initially.
There's always an iterative process of refining the model until you are confident in its being good enough. When are you confident it is good enough? That's quite similar to asking "If you don't use formal methods, how do you know when your work is done?"
That doesn't sound right. Automatic proof assistants/verifiers won't approve your proof unless it really is a proof for the model, right?
> there are always errors in the model, at least initially
Agreed.
> There's always an iterative process of refining the model until you are confident in its being good enough. When are you confident it is good enough?
It's true that bugs in the model are a possibility.
More broadly, it's possible for defects to get through a formal software-development methodology. There was an interesting case study done on this. [0] Vastly fewer than if formal methods are not used, but you're still right that ultimately it's not a completely rock-solid guarantee. (And that's not counting things like bugs in the proof-assistant, or bugs in the non-verified compiler you end up using.)
[0] https://www.adacore.com/tokeneer ('Analysis' section is on page 59 of PDF)
See also https://blog.adacore.com/tokeneer-fully-verified-with-spark-... , https://github.com/AdaCore/spark2014/tree/master/testsuite/g...
I actually work in an agile environment that uses formal methods and it is possible!