4 ms·

The question I always have is "why would the formal verification be any more correct than the program it is verifying?", Note: not bugs in the verification engi

by somat 2mo ago

The question I always have is "why would the formal verification be any more correct than the program it is verifying?", Note: not bugs in the verification engine, but the spec made for the program. It is not a big deal, I think formal verification is a very useful tool to help one approach correctness, but let me explain myself. When a program is written it is trying to solve a problem, when it solves that problem correctly it has no bugs, and when it solves that problem incorrectly those are bugs. For complex problems it turns out to be very difficult(impossible) to solve them correctly. Why is there an assumption that the formal verification spec will be any more correct than the program itself? They are both trying to solve very complex problems. I was trying to get a feel for this by reading through the sel4 git changes trying to figure out how many bug fixes were for the OS and how many were for the spec. No real conclusion unfortunately. because they almost always have to fix both at the same time. a bug found in the OS means you have a bad spec and a bug found in the spec means your OS probably has a bug.

pfdietz 2mo ago
Empirically, we can look at something like CompCert, which formally verified a substantial section of a C compiler. Subsequent high volume random testing with Csmith found no bugs in the formally verified section (unlike in every other C compiler tested with Csmith). It should be noted that the verification performed was specifically about whether the compiler would produce incorrect code; cases where it would crash or error and not produce code would not be considered errors of verification. This would enable (for example) a coloring register allocator to be adjoined with some code that checked whether the coloring was correct and abort if not.
- pseudohadamard 2mo ago
  The problem with CompCert is that it produces really bad code, below the level of gcc -O0, about the level of the eternally-in-progress compiler project you worked on in your Programming Languages 370 course. So you can get most of the benefits of CompCert by running a standard compiler with -O0.
  - pfdietz 2mo ago
    Nevertheless, this is a demonstration that verification can produced apparently bug-free code.
ivanbakel 2mo ago
>why would the formal verification be any more correct than the program it is verifying? It is quite believable that it's easier to describe what a program should result in versus actually programming it to produce that result - especially in the most common settings targeted by verification, which is to say imperative, stateful programs or algortihms with a high degree of non-obvious optimisations. The simplest example is a sorting algorithm, which normally has a trivial spec but a non-trivial state at each step. Interestingly, some specs are actually programs themselves, as has also been true for many on-paper specs which are actually reference implementations. Research using programs-as-specs is still pretty valuable, since in some domains a simpler program is actually the right and useful way to talk about a messier one.
- makeitdouble 2mo ago
  > It is quite believable that it's easier to describe what a program should result in versus actually programming it to produce that result This is obvious for the central cases of a program. It becomes less and less true when going toward the edge cases, especially for a wide array of input. Complex specs becoming programs is IMHO the direct effect of that (defining what we want is just that burdensome, and special cases we haven't though of will still have a coherent definition in the spec), and we fall back to the base "is this spec even correct" issue the parent points out.
  - deterministic 1mo ago
    The trick is to start with the smallest possible implementation of a spec and proving it correct. You then add a more advanced and faster implementation and prove that the 2nd implementation implements the 1st. Etc. etc. It's called refinement and it's a great way to prove really complex software correct. You basically have a formally proven correct chain of software from simple to advanced. CompCert is an example of how to do this.
- Veserv 2mo ago
  Huh? Sorting does not have a trivial specification. In fact, it is usually used as the first example of how easy it is to make specification errors because it seems trivial, but is actually not.
nylonstrung 2mo ago
This is valid and my take is that domain modelling becomes extremely important in this context More then theorem proving what attracts to Lean is that it's type system is insanely powerful, indexed dependant inductive and quotient types allow the realization of "making invalid states unrepresentable" to a degree no other language can, except perhaps a custom DSL built with Racket One must remember that Lean wasn't made for math, it ended up succeeding in that vertical because it was expressive enough to represent the extensive design space mathematicians were dealing with And I think that's equally applicable to specs and business logic
- jkhdigital 2mo ago
  Yeah I feel like the hype around “formal methods” is really just a growing interest in expressive type systems that enable more and more program semantics to be declared in code rather than in comments. Correctness is good, but so are portability and modularity and extensibility.
  - deterministic 1mo ago
    LEAN is exactly an expressive type system. Nothing more. The amazing thing is that the type system is so powerful that you can express cutting-edge mathematics with it and prove it correct. In other words, proving something is essentially the same thing as type checking. It absolutely blew my mind when I finally understood how it works. For that reason alone, LEAN is worth diving into. :)
- inigyou 2mo ago
  Is a type like "fixed-size list of 3 integers" really more useful than a type like "list of integers" plus a constraint "size must be 3"? I feel like the latter is more flexible. Does Lean have a type for "list containing only prime powers"?
  - samus 2mo ago
    To some degree these are the same things, depending on the type system. But it might be easier to write a function accepting a list of size 3 than matching on a constraint, which might get separated from the variable it annotates.
sunir 2mo ago
From a computer science point of view, it's the same argument as why NP-complete problems are hard to solve, and easy to check. From a practical point of view, however, it's the same argument we write unit and integration tests. We accept error rates in the program under test, the test, the test harness, the programming language, the operating system, the hardware, and the universe. The goal is reduce the error rates enough you can ship something you can get paid for and won't get sued for later before you starve to death.
andrewchambers 2mo ago
Often the spec can be simpler than the original. The easiest way to demonstrate this is to write two implementations of an algorithm. One with no optimizations, the other with optimizations. The formal verification can then be a proof the optimizations maintain the semantics of the simpler version and you can focus your review on the simpler version.
syphia 2mo ago
Verification is sometimes less conceptually difficult than solving. I'd say for most well-defined problems, verifying is simpler. E.g. finding a general solution for a cubic polynomial is difficult. Proving that a solution is correct is conceptually trivial: substitute a solution for x, and simplify. Many mathematical problems are well-defined in this way. In the case of a compiler (CompCert), the program is already, in part, being written according to the language spec. So that definition can be used in verifying a compiler. In a domain where there is no standard specification or required properties, then coming up with a spec is hard (probably as hard as coming up with a solution).
inigyou 2mo ago
Formal verification doesn't have to verify the entire functionality of the program to be useful; Rust's type system is supposed to formally verify that your program has no memory safety bugs. (It doesn't. Because formal verification is hard. See cve-rs for how to corrupt memory without unsafe. Rust has stated they do not intend to fix cve-rs.)
- yencabulator 2mo ago
  > Rust has stated they do not intend to fix cve-rs. Huh? That joke repo seemed to ride on https://github.com/rust-lang/rust/issues/25860 https://github.com/rust-lang/rust/issues/25860 which is certainly considered a bug. Here's an actually useful list of known soundness issues, all of which are bugs waiting to be fixed, no stupid snark needed: https://github.com/rust-lang/rust/issues?q=state%3Aopen%20label%3A%22I-unsound%22 https://github.com/rust-lang/rust/issues?q=state%3Aopen%20la...
samus 2mo ago
> The question I always have is "why would the formal verification be any more correct than the program it is verifying?", Note: not bugs in the verification engine, but the spec made for the program. It is a nothingburger problem because one is going to have that problem as well even when not employing formal methods. Except without FM the spec will be in natural language and therefore it will be impossible to mechanically verify the end product with it. And since natural language specs are highly liable to be ambiguous or contain unintended holes, LLMs won't save us either.

by somat 2mo ago

pfdietz 2mo ago

Empirically, we can look at something like CompCert, which formally verified a substantial section of a C compiler. Subsequent high volume random testing with Csmith found no bugs in the formally verified section (unlike in every other C compiler tested with Csmith). It should be noted that the verification performed was specifically about whether the compiler would produce incorrect code; cases where it would crash or error and not produce code would not be considered errors of verification. This would enable (for example) a coloring register allocator to be adjoined with some code that checked whether the coloring was correct and abort if not.

pseudohadamard 2mo ago
The problem with CompCert is that it produces really bad code, below the level of gcc -O0, about the level of the eternally-in-progress compiler project you worked on in your Programming Languages 370 course. So you can get most of the benefits of CompCert by running a standard compiler with -O0.
- pfdietz 2mo ago
  Nevertheless, this is a demonstration that verification can produced apparently bug-free code.

ivanbakel 2mo ago

>why would the formal verification be any more correct than the program it is verifying? It is quite believable that it's easier to describe what a program should result in versus actually programming it to produce that result - especially in the most common settings targeted by verification, which is to say imperative, stateful programs or algortihms with a high degree of non-obvious optimisations. The simplest example is a sorting algorithm, which normally has a trivial spec but a non-trivial state at each step. Interestingly, some specs are actually programs themselves, as has also been true for many on-paper specs which are actually reference implementations. Research using programs-as-specs is still pretty valuable, since in some domains a simpler program is actually the right and useful way to talk about a messier one.

makeitdouble 2mo ago
> It is quite believable that it's easier to describe what a program should result in versus actually programming it to produce that result This is obvious for the central cases of a program. It becomes less and less true when going toward the edge cases, especially for a wide array of input. Complex specs becoming programs is IMHO the direct effect of that (defining what we want is just that burdensome, and special cases we haven't though of will still have a coherent definition in the spec), and we fall back to the base "is this spec even correct" issue the parent points out.
- deterministic 1mo ago
  The trick is to start with the smallest possible implementation of a spec and proving it correct. You then add a more advanced and faster implementation and prove that the 2nd implementation implements the 1st. Etc. etc. It's called refinement and it's a great way to prove really complex software correct. You basically have a formally proven correct chain of software from simple to advanced. CompCert is an example of how to do this.
Veserv 2mo ago
Huh? Sorting does not have a trivial specification. In fact, it is usually used as the first example of how easy it is to make specification errors because it seems trivial, but is actually not.

nylonstrung 2mo ago

This is valid and my take is that domain modelling becomes extremely important in this context More then theorem proving what attracts to Lean is that it's type system is insanely powerful, indexed dependant inductive and quotient types allow the realization of "making invalid states unrepresentable" to a degree no other language can, except perhaps a custom DSL built with Racket One must remember that Lean wasn't made for math, it ended up succeeding in that vertical because it was expressive enough to represent the extensive design space mathematicians were dealing with And I think that's equally applicable to specs and business logic

jkhdigital 2mo ago
Yeah I feel like the hype around “formal methods” is really just a growing interest in expressive type systems that enable more and more program semantics to be declared in code rather than in comments. Correctness is good, but so are portability and modularity and extensibility.
- deterministic 1mo ago
  LEAN is exactly an expressive type system. Nothing more. The amazing thing is that the type system is so powerful that you can express cutting-edge mathematics with it and prove it correct. In other words, proving something is essentially the same thing as type checking. It absolutely blew my mind when I finally understood how it works. For that reason alone, LEAN is worth diving into. :)
inigyou 2mo ago
Is a type like "fixed-size list of 3 integers" really more useful than a type like "list of integers" plus a constraint "size must be 3"? I feel like the latter is more flexible. Does Lean have a type for "list containing only prime powers"?
- samus 2mo ago
  To some degree these are the same things, depending on the type system. But it might be easier to write a function accepting a list of size 3 than matching on a constraint, which might get separated from the variable it annotates.

sunir 2mo ago

From a computer science point of view, it's the same argument as why NP-complete problems are hard to solve, and easy to check. From a practical point of view, however, it's the same argument we write unit and integration tests. We accept error rates in the program under test, the test, the test harness, the programming language, the operating system, the hardware, and the universe. The goal is reduce the error rates enough you can ship something you can get paid for and won't get sued for later before you starve to death.

andrewchambers 2mo ago

Often the spec can be simpler than the original. The easiest way to demonstrate this is to write two implementations of an algorithm. One with no optimizations, the other with optimizations. The formal verification can then be a proof the optimizations maintain the semantics of the simpler version and you can focus your review on the simpler version.

syphia 2mo ago

Verification is sometimes less conceptually difficult than solving. I'd say for most well-defined problems, verifying is simpler. E.g. finding a general solution for a cubic polynomial is difficult. Proving that a solution is correct is conceptually trivial: substitute a solution for x, and simplify. Many mathematical problems are well-defined in this way. In the case of a compiler (CompCert), the program is already, in part, being written according to the language spec. So that definition can be used in verifying a compiler. In a domain where there is no standard specification or required properties, then coming up with a spec is hard (probably as hard as coming up with a solution).

inigyou 2mo ago

Formal verification doesn't have to verify the entire functionality of the program to be useful; Rust's type system is supposed to formally verify that your program has no memory safety bugs. (It doesn't. Because formal verification is hard. See cve-rs for how to corrupt memory without unsafe. Rust has stated they do not intend to fix cve-rs.)

yencabulator 2mo ago
> Rust has stated they do not intend to fix cve-rs. Huh? That joke repo seemed to ride on https://github.com/rust-lang/rust/issues/25860 https://github.com/rust-lang/rust/issues/25860 which is certainly considered a bug. Here's an actually useful list of known soundness issues, all of which are bugs waiting to be fixed, no stupid snark needed: https://github.com/rust-lang/rust/issues?q=state%3Aopen%20label%3A%22I-unsound%22 https://github.com/rust-lang/rust/issues?q=state%3Aopen%20la...

samus 2mo ago

> The question I always have is "why would the formal verification be any more correct than the program it is verifying?", Note: not bugs in the verification engine, but the spec made for the program. It is a nothingburger problem because one is going to have that problem as well even when not employing formal methods. Except without FM the spec will be in natural language and therefore it will be impossible to mechanically verify the end product with it. And since natural language specs are highly liable to be ambiguous or contain unintended holes, LLMs won't save us either.