31 ms·

"For a proof of correctness, you need to model the environment, and write a specification or a golden model. These are just as prone to bugs as the system you a

"For a proof of correctness, you need to model the environment, and write a specification or a golden model. These are just as prone to bugs as the system you are trying to verify (even assuming the tools are correct)." I disagree with the idea that a spec is as buggy as the implementation. Some examples. In hardware verification, a spec for a floating-point operation is typically a page or two long. The corresponding RTL implementations can be tens of thousands of lines, with many additional concerns (pipelining, clock gating, ...) that don't show up in the spec, and where the operation itself is fused together with dozens of other operations. The difference in complexity is striking. In simple software cases, say a sorting function, the spec can be as straightforward as "the answer is ordered and has the same elements as the input array." This same spec can be used with any number of implementations, including things like Timsort where there are multiple modes and optimizations that are interacting with one another. The spec says nothing about runs, galloping, etc., which the implementation uses. For more complex software, the spec can of course become complex. Even so, there are examples, e.g., the Jitawa Lisp runtime (https://www.cl.cam.ac.uk/~mom22/jitawa/ https://www.cl.cam.ac.uk/~mom22/jitawa/), where the spec is a relatively straightforward description of a programming language that is much, much simpler than the implementation. For instance, the spec here does not mention things like garbage collection and just-in-time compilation, which are fairly complex features of the implementation. Anyway, trusting a formal proof seems, to me, certainly no less sane than trusting a system without such a proof.

crdoconnor 9y ago
>I disagree with the idea that a spec is as buggy as the implementation. Some examples. It isn't necessarily as buggy as implementation, but I've worked on plenty of (non-formally verified) projects where the majority of bugs were spec bugs. If you're diligent about following the UNIX philosophy of assembling small self-contained, tightly specified (and test driven) components, this is pretty normal I think. Building the wrong thing is often the biggest problem. The one time I did do formal verification (at uni) that was certainly the case too, though that may partly have been because the language was an overcomplicated pile of crap (Z). One of my co-workers also told me a story about a formally verified program being translated into python and having a couple of bugs picked up on the way. I'm pretty credulous of this.
falcolas 9y ago
Here's a spec which was buggy and yet widely accepted and implemented: TLS 1.0 You could formally prove an implementation of it and had a dangerously buggy end product. The same could be said for many of the early encryption specs which have proven to be vulnerable against timing attacks, side channel attacks, and so forth. I've helped QA quite a few financial specs (namely those created to transform credit reports into decisions) which were inherently buggy, and these were written as almost pure mathematical formulas that just didn't take corner cases into account. A formal proof has value, but it's certainly not an absolute - relying on it blindly to indicate the correctness of a program is putting yourself at risk. EDIT: As a completely separate point, let's look at the potential problems with this sorting spec: "the answer is ordered and has the same elements as the input array." What does ordered mean? How do I compare a number and a string? A binary blob? A structure? Is there a restriction on the word "same" - do they have to be the existing object, or can it be a copy? Should the answer be in the same memory space as the original, or should it be a distinct memory object? Can the original be modified?
- user5994461 9y ago
  That's joining the correctness/safety vs security argument. Correctness/safety is to do what it's supposed to do. Security is to do what it's supposed to do when there is an intelligent third party that is actively trying to prevent that.
  - falcolas 9y ago
    To that, I would argue that security is (or should be) part of the spec; if it’s not secure, it’s not correct. Having it be a separate and lesser concern is how we end up tacking on security features as an afterthought. To borrow from the kernel devs: Security requirements are just like any other requirements.
- wizeman 9y ago
  > A formal proof has value, but it's certainly not an absolute - relying on it blindly to indicate the correctness of a program is putting yourself at risk. Indeed, I agree, but lots of people never ask themselves how much more at risk they are putting themselves when their implementation has no formal spec or proof at all! Like another commenter has argued, it seems that people seem to look at formal verification like it's an all-or-nothing approach (either it achieves zero bugs or it's completely worthless, or alternatively -- if it's formally verified then it MUST be bug free!), but it's really not, it simply gives higher (often, much much higher) assurances.

crdoconnor 9y ago

>I disagree with the idea that a spec is as buggy as the implementation. Some examples. It isn't necessarily as buggy as implementation, but I've worked on plenty of (non-formally verified) projects where the majority of bugs were spec bugs. If you're diligent about following the UNIX philosophy of assembling small self-contained, tightly specified (and test driven) components, this is pretty normal I think. Building the wrong thing is often the biggest problem. The one time I did do formal verification (at uni) that was certainly the case too, though that may partly have been because the language was an overcomplicated pile of crap (Z). One of my co-workers also told me a story about a formally verified program being translated into python and having a couple of bugs picked up on the way. I'm pretty credulous of this.

falcolas 9y ago

Here's a spec which was buggy and yet widely accepted and implemented: TLS 1.0 You could formally prove an implementation of it and had a dangerously buggy end product. The same could be said for many of the early encryption specs which have proven to be vulnerable against timing attacks, side channel attacks, and so forth. I've helped QA quite a few financial specs (namely those created to transform credit reports into decisions) which were inherently buggy, and these were written as almost pure mathematical formulas that just didn't take corner cases into account. A formal proof has value, but it's certainly not an absolute - relying on it blindly to indicate the correctness of a program is putting yourself at risk. EDIT: As a completely separate point, let's look at the potential problems with this sorting spec: "the answer is ordered and has the same elements as the input array." What does ordered mean? How do I compare a number and a string? A binary blob? A structure? Is there a restriction on the word "same" - do they have to be the existing object, or can it be a copy? Should the answer be in the same memory space as the original, or should it be a distinct memory object? Can the original be modified?

user5994461 9y ago
That's joining the correctness/safety vs security argument. Correctness/safety is to do what it's supposed to do. Security is to do what it's supposed to do when there is an intelligent third party that is actively trying to prevent that.
- falcolas 9y ago
  To that, I would argue that security is (or should be) part of the spec; if it’s not secure, it’s not correct. Having it be a separate and lesser concern is how we end up tacking on security features as an afterthought. To borrow from the kernel devs: Security requirements are just like any other requirements.
wizeman 9y ago
> A formal proof has value, but it's certainly not an absolute - relying on it blindly to indicate the correctness of a program is putting yourself at risk. Indeed, I agree, but lots of people never ask themselves how much more at risk they are putting themselves when their implementation has no formal spec or proof at all! Like another commenter has argued, it seems that people seem to look at formal verification like it's an all-or-nothing approach (either it achieves zero bugs or it's completely worthless, or alternatively -- if it's formally verified then it MUST be bug free!), but it's really not, it simply gives higher (often, much much higher) assurances.