Can we formally verify the software cannot be used for evil?
gonna have to formally define evil
How about: skeptical of formal verification?
Make formal verification and provably correct software practical and mainstream
61–70 of 203 posts
Re: Make formal verification and provably correct software practical and mainstream
#62I suspect that verifying software is a lot like the termination problem of Turing machines: the more useful properties you want to verify, the closer it is to NP completeness. So a practical verifier should limit its scope to a modest subset of software and settle on verifying sonething with a sufficient degree of confidence, which is lower than 100%.
Both termination and verification go beyond NP completess, in that they are undecidable. Also, "verifying so[m]ething with... confidence... lower than 100%" is known as testing.
Re: Make formal verification and provably correct software practical and mainstream
#63Earlier quoted context omitted.
>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…
> Software can still be provably correct and have security holes resulting from an insecure definition of "correct." Formal verification does not solve security. Nirvana fallacy. The point is that it can be much better and eliminate ALL non-design bugs. > 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 th…
> Nirvana fallacy. The point is that it can be much better and eliminate ALL non-design bugs.
Serious question: do you really believe that?
> That's just stupid. Show me the studies.
There is a kind of HAL-9000 quality to many of these arguments. Formal verification is perfect by definition. The fact that it hasn't had very much impact in the real world is all the more evidence of the world being full of wicked people.
Re: Make formal verification and provably correct software practical and mainstream
#64I 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 i…
I agree it sounds like pretty naive enthusiasm. Not just about how hard the formal verification problem is, but about how hard it is to get ANY kind of programming system up to the point where it's actually usable.
However, every time somebody starts going negative on formal verification by talking about decidability, I get itchy. Sure, we know, all interesting properties of programs in all interesting languages are undecidable in general. Rice's theorem, blah, blah, blah. For any given property and any given language, I can show you a program in that language such that you cannot determine whether that program has that property.
... but it turns out that most actually INTERESTING PROGRAMS aren't like that. When you really write code to get something done, you you generally have a reason to believe that code is going to work. That means that the code is least approximately correct by construction, and correct in a way that's comprehensible and locatable. Often the machine will be able to find a proof that it's correct. If not, you'll often be able to provide hints. And if neither you nor your computer can find a proof, that probably means you don't understand the code enough to want to use it to begin with.
Oh, and on computational cost of verification, you can get some relief by passing around precomputed proofs along with the source code, so they only have to be checked on installation, or incrementally recomputed when the code is modified, rather than being rebuilt from scratch every time.
Re: Make formal verification and provably correct software practical and mainstream
#65I 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 i…
It is wishful thinking. Iris is cool and all but extracting useful programs from proofs is still an open research area. I don’t want to discourage someone from trying but it would help to be pragmatic. At least the author seems somewhat aware of this when they describe the repo as a collection of earnings and ravings. I’ve been interested in this since 2015 or so and even then the cost of doing formal verification ha…
> One of the major challenges will be teaching industry programmers how to write proofs and convincing them that they want to do this.
"Industry programmers" are pretty far from being a monolith. There are a myriad of different approaches to testing, many of which are domain specific, for all kinds of reasons.
Usually the way that a new testing tool gets adapted is that individual programmers or companies that adapt the tool appear to have a competitive advantage over those that don't. The results generally speak for themselves, at least after a time.
Practically everybody that might use formal verification has already chosen to not go to certain lengths to increase reliability. They're already making an economic trade-off -- even with safety critical systems, or in domains where the cost of bugs is extraordinarily high. Why shouldn't formal verification be assessed in the same way?
Re: Make formal verification and provably correct software practical and mainstream
#66I 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 i…
I agree it sounds like pretty naive enthusiasm. Not just about how hard the formal verification problem is, but about how hard it is to get ANY kind of programming system up to the point where it's actually usable. However, every time somebody starts going negative on formal verification by talking about decidability, I get itchy. Sure, we know, all interesting properties of programs in all interesting languages are…
A lot of people take undecidability to mean “no program can be proven to terminate” when in reality it means “there exist programs which are impossible to prove termination,” and like you said most of the useful programs we write can be shown to terminate just fine.
Re: Make formal verification and provably correct software practical and mainstream
#67Earlier 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've used formal verification in anger, as well as working with a vendor to formaly verify some critical code for us. This rings very true. It is extraordinarily difficult to write correct rules. It ends up being the same problem as wishing against an evil genie.
Most rules that you come up with at first end up having a class of obvious exceptions in the real world, which the verifier finds, and then even more unobvious exceptions, and soon your logic around the exceptions to the rules become at least as complicated as the code you are attempting to verify. And in this any wrong assumptions that falsely allow bad behavior are not caught or flagged because they pass.
Even giving perfect proving software, it's still a far harder challenge to write rules than to write code. And current software is still far from perfect - you are likely to spend a lot of your rules time fighting with your prover.
Re: Make formal verification and provably correct software practical and mainstream
#68Is it even realistic to make a provably secure/stable applications on an OS like windows or linux? This (provable correctness of programs, at the expense of performance) is one of the explicit design goals or urbit. I know HN hates urbit and don't want to rehash that, but it seems like a good goal for some use cases and I'm not sure it's possible to achieve without building the OS around it.
Let's say that Urbit claims to be formally, provably secure. But approximately nobody actually understands Urbit, which means that nobody knows whether the proof is solid. So as an outsider, I have to either take it on faith that it's secure, or I have to spend a fair amount of time immersing myself in this hard-to-learn system to see if the claimed benefits are really there. But it's not just Urbit. Rust has essenti…
You don't have to understand the linux kernel to buffer overlow a linux application; If they do something like "Here's the IP of a running urbit with 100BTC in it, good luck!" and it's still up in a few years, that'd be compelling.
But more generally, if it's true that the only way to make a provably secure app is to design the OS and language around that purpose, then the problem you describe is general too - it will always be a challenge to find auditors.
Re: Make formal verification and provably correct software practical and mainstream
#69I 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 i…
I agree it sounds like pretty naive enthusiasm. Not just about how hard the formal verification problem is, but about how hard it is to get ANY kind of programming system up to the point where it's actually usable. However, every time somebody starts going negative on formal verification by talking about decidability, I get itchy. Sure, we know, all interesting properties of programs in all interesting languages are…
I disagree that most interesting programs don't need things that are Hard to Verify. For instance, approximately every C program would benefit from correct pointer analysis, yet this remains an open research question.
For a personal example, I had a recent lunch interaction with our security team about some work I wanted to do formally verifying bits of a bootloader we have. Halfway through the conversation, one of them pulls up a report they made about how susceptible our specific CPU is to power-glitching. This is something the system design ought to be resistant to, so now my "straightforward idea" has a bunch of thesis-sized holes in it unless I either cut that out of the proof (what will probably happen) or I can make it someone else's problem.
Formal methods are just hard, and open research questions lurk in every slightly dark corner.
Re: Make formal verification and provably correct software practical and mainstream
#70I am strongly inclined toward verifying my software to the extent possible but there are many practical challenges. I think academic formal verification methods look elegant, which appeals to me, but are extremely human intensive when what I really want to do is throw machines at the problem to the extent possible. There are also some important types of software correctness that are still difficult to capture with these methods, though the state-of-the-art has improved with time.
I've toyed with many methods, tools, techniques, and approaches to get a sense of where the ROI maxima is for my own purposes. In practice, I've found that sophisticated and comprehensive application of less elegant methods amenable to throwing hardware at them, like exhaustive functional testing, thorough fuzzing infrastructure, systematic fault injection coverage, various types of longevity testing, etc when done well often found all the same design flaws as a tractable level of more academic formal verification. Also easier to maintain as code evolves. Furthermore, these less elegant approaches also found the occasional compiler and hardware bug that more elegant formal verification methods typically do not.
I have wondered if developing and standardizing this less elegant tooling to a high level, so that it is easier to be lazy and throw hardware at the problem, would have at least as much impact on software quality as trying to get everyone to apply very academic formal verification methods, with their current limitations and theoretical constraints. As much as I like the concept of very pure formal verification, I lean toward whatever makes maximizing software quality practical and economic.