Make formal verification and provably correct software practical and mainstream • Hacker News Board

Re: Make formal verification and provably correct software practical and mainstream

#31

Post by AlotOfReading » Sat, May 28, 2022, 11:15 PM UTC

I really want to like this, but it really comes across as more of a wishful thinking project without a lot of experience or intuition about how to solve the very real problems that formal methods run into in this domain. Like, the design goals literally include "verify any program" [1], which is almost certainly impossible.

Important questions like how you implement the design pillars without running smack into the issue of decidability seem entirely ignored. They have a whole section on how "this idea exists in an incentive no man's land" without seemingly being aware of the rich history of formal methods in low level programming, from Ada through Java through formal C through Rust itself. The common issues these encountered like decidability, holes in the formal model (which contributed to the downfall of the Java sandbox as a security boundary), and the combinatorial explosion inherent in verification tools are all huge looming questions that should at least be mentioned.

Maybe I'm being overly critical here and partial improvements are still improvements, but it'd be nice to see more moderate claims from authors tackling such an ambitious project.

[1] https://github.com/magmide/magmide/blob/main/posts/design-of...

Re: Make formal verification and provably correct software practical and mainstream

#32

Post by _vdpp » Sat, May 28, 2022, 11:16 PM UTC

muglug wrote: post #17

This builds on the success of Rust, but Rust has not been a success when it comes to [number of engineers writing professional code in the language]. By that measure it's still incredibly niche compared to interpreted languages. The main reason why formal verification has not had even the success of Rust is that most developers (myself included) don't know enough about the area to take an interest, and certainly don'…

Formal verification predates Rust by decades. The addition of lifetimes and the borrow checker are worthwhile contributions to the field of provably-safe software, but there are a lot of other soundness properties that Rust doesn’t check (though people are working on it).

Re: Make formal verification and provably correct software practical and mainstream

#33

Post by _vdpp » Sat, May 28, 2022, 11:21 PM UTC

toast0 wrote: post #16

Formal verification needs machine readible formal specifications, but any kind of written specification, informal or not was pretty hard to find in my career at internet giants. Maybe you can get a formal spec in aerospace or FDA regulated implanted devices, but cost to write the spec, let alone to follow the spec is way too high when the spec needs to change at the whim of a hat.

In the SPARK subset of Ada, the specifications and contracts live alongside your code in the same language, then you can prove that the specs are satisfied.

You can also leave out the contracts and just prove absence of behaviors like divide by zero, out-of-bounds array access and integer overflow. Proving that code meets the specification can be really difficult but proving absence of bad behavior is usually a straightforward endeavor.

Re: Make formal verification and provably correct software practical and mainstream

#34

Post by pydry » Sat, May 28, 2022, 11:23 PM UTC

johnbender wrote: post #29

csande17 wrote: post #21

As the article mentions, formal verification techniques are primarily used today for two things: - Creating secure "core" code -- library functions and kernels and stuff, where the things they're supposed to do are very well-defined. - Verifying specific, narrowly defined properties, like how Rust's borrow checker guarantees that your program doesn't try to write to the same value from two different threads at once.…

I think this sharply discounts the value of the step before the proof which is writing the specification in a formal language/logic. This often surfaces these misunderstandings before a proof is even necessary. That doesn’t guarantee that the spec will be the right one (as you say) but it’s astounding how often just writing it down formally improves the implementation through rigorous thought.

I've only done a bit of formal verification but I'd estimate that writing that spec was 7-10x harder than writing the actual program and was more complicated than the code.

In the end I had lower confidence that the spec lacked bugs than the program. This was after expending a huge amount of effort on a pretty tiny program.

I dont think this was a tooling thing. I think it spoke to the fundamental limits of formal verification. I think it'll always remain kinda niche.

Re: Make formal verification and provably correct software practical and mainstream

#35

Post by _vdpp » Sat, May 28, 2022, 11:26 PM UTC

One thing that will help drive adoption is the ability to run SMT solvers more quickly so the proof stage of your design/build has a faster feedback loop.

I ran some experiments with the Z3 and alt-ergo solvers (verifying SPARK/Ada code using GNATprove) on a base M1 Mini and it absolutely screamed, I’m not normally a Mac fan-boy but new chips like the M1 Ultra might have the possibility of driving a mini-renaissance in FV.

I’d like to see more attention being given to GPU accelerated SMT solvers too but haven’t seen much movement outside of a handful of research papers.

Re: Make formal verification and provably correct software practical and mainstream

#36

Post by [deleted] » Sat, May 28, 2022, 11:33 PM UTC

guerrilla wrote: post #24

daenz wrote: post #14

Earlier quoted context omitted.

>Software often doesn't. And yet the world keeps turning, tech companies keep profiting, and customers are generally happy with the value provided, all without formally provable code bases. How does "provably correct" improve on this without extending timelines and costing more?

> tech companies keep profiting, and customers are generally happy with the value provided Obviously the answer is that they could profit more and be happier. Ever heard of this thing called ransomware, for example? Identity theft? And you must know, this stuff is only the beginning... Just wait until the day everyone's private Facebook chats are available on torrent.

[deleted]

Re: Make formal verification and provably correct software practical and mainstream

#37

Post by _vdpp » Sat, May 28, 2022, 11:34 PM UTC

daenz wrote: post #6

Outside of mission critical applications, if the cost involved to make software "provably correct" (time, salaries) is greater than the cost of the bugs, it will never be adopted. Believe me, I see the appeal, but it's kind of like demanding your house have all perfect right angles and completely level surfaces. Living with manageable imperfection is far more realistic.

I think the cost of provably correct software is actually much lower, but you pay more of it up front. The perceived incentives of being first to market are higher than that of quality software.

I suspect eventually there will be a big lawsuit where the blame can be laid on negligence in the software development and the incentives might change somewhat.

Re: Make formal verification and provably correct software practical and mainstream

#38

Post by yodsanklai » Sat, May 28, 2022, 11:34 PM UTC

daenz wrote: post #6

Outside of mission critical applications, if the cost involved to make software "provably correct" (time, salaries) is greater than the cost of the bugs, it will never be adopted. Believe me, I see the appeal, but it's kind of like demanding your house have all perfect right angles and completely level surfaces. Living with manageable imperfection is far more realistic.

Even regular static type-checking is seen as a burden by many programmers.

Re: Make formal verification and provably correct software practical and mainstream

#39

Post by daenz » Sat, May 28, 2022, 11:35 PM UTC

guerrilla wrote: post #24

daenz wrote: post #14

Earlier quoted context omitted.

>Software often doesn't. And yet the world keeps turning, tech companies keep profiting, and customers are generally happy with the value provided, all without formally provable code bases. How does "provably correct" improve on this without extending timelines and costing more?

> tech companies keep profiting, and customers are generally happy with the value provided Obviously the answer is that they could profit more and be happier. Ever heard of this thing called ransomware, for example? Identity theft? And you must know, this stuff is only the beginning... Just wait until the day everyone's private Facebook chats are available on torrent.

>Ever heard of this thing called ransomware, for example? Identity theft?

Software can still be provably correct and have security holes resulting from an insecure definition of "correct." Formal verification does not solve security.

>Obviously the answer is that they could profit more and be happier.

Please explain how a company could profit more if formal verification does not bring more revenue than it costs? You seem to be assuming that revenue will appear that is greater than the costs. Where is this revenue coming from, exactly?

Re: Make formal verification and provably correct software practical and mainstream

#40

Post by johnbender » Sat, May 28, 2022, 11:36 PM UTC

pydry wrote: post #34

johnbender wrote: post #29

Earlier quoted context omitted.

I think this sharply discounts the value of the step before the proof which is writing the specification in a formal language/logic. This often surfaces these misunderstandings before a proof is even necessary. That doesn’t guarantee that the spec will be the right one (as you say) but it’s astounding how often just writing it down formally improves the implementation through rigorous thought.

I've only done a bit of formal verification but I'd estimate that writing that spec was 7-10x harder than writing the actual program and was more complicated than the code. In the end I had lower confidence that the spec lacked bugs than the program. This was after expending a huge amount of effort on a pretty tiny program. I dont think this was a tooling thing. I think it spoke to the fundamental limits of formal ve…

I think this depends on the spec language and the target system. I’ve never encountered a spec more complicated than the program as the goal is always abstraction but I don’t mean to discount your experiences and complexity is affected by tooling familiarity and quality.

Separately the spec can often have its own properties which can be verified as a means to interrogate its correctness. For example state machines as spec, temporal logic properties and model checking where the state machine is the abstraction for a concrete system. Worth noting that proving state machines are an abstraction of a concrete system is a going research concern though.