Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Make formal verification and provably correct software practical and mainstream

github.com

Post reply on HN
Print view View original

41–50 of 203 posts

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

#41

Post by joek1301 »

AlotOfReading wrote: post #31

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 i…

Could you elaborate / share resources on "downfall of the Java sandbox as a security boundary"? Sounds interesting.

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

#42

Post by johnbender »

AlotOfReading wrote: post #31

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 i…

To follow on this sentiment at a slight tangent, I am happy for the enthusiastic attempts from all quarters but folks seem to misunderstand that incremental progress in academia is often due to the problems being very hard. Formal verification in the presence of weak memory models is an ongoing problem that only recently has seemed tractable thanks to the hard work of the folks at MPI etc over more than a decade of publications and iterating on logics like Iris

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

#43

Post by hn_urbit_thr123 »

Is 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.

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

#44

Post by guerrilla »

daenz wrote: post #39
guerrilla wrote: post #24

Earlier quoted context omitted.

> 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…

> 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 that is greater than the costs. Where is this revenue coming from, exactly?

The revenue could come from savings on fixing bugs, paying for ransomed assets and all other costs that come from bugs. You're just assuming that doesn't add up and that there's no other reason that we don't do formal verification. That's just stupid. Show me the studies. Your claim is just as strong as the claim you think I'm making, but you missed my point entirely.

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

#45

Post by guerrilla »

practal wrote: post #30
Animats wrote: post #20

"And all existing proof languages are hopelessly mired in the obtuse and unapproachable fog of research debt created by the culture of academia." Yes. As I wrote 40 years ago: "There has been a certain mystique associated with verification. Verification is often viewed as either an academic curiosity or as a subject incomprehensible by mere programmers. It is neither. Verification is not easy, but then, neither is wr…

I am sure we can do better than predicate logic or types, but the code needs to change also. Code should be more abstract and reusable. If possible, it should be a subset of the logic. There is no point in verifying the same stuff in JavaScript, Java, Rust, Swift, ... Furthermore, something that looks simple might need a lot of abstraction to become provable. Something might be simple to write down in code, but in or…

> First get mathematicians to actually like doing proofs with the help of a computer.

Many are using type theoretic and HOL theorem proves already. What threshold do we need to reach? Isn't Lean HoTT? Isn't that pretty much good enough (modulo UI and tooling)? I ask the latter question because that was the original promise of HoTT but I haven't kept up to date on Lean, so I'm asking.

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

#48

Post by IncRnd »

joek1301 wrote: post #41
AlotOfReading wrote: post #31

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 i…

Could you elaborate / share resources on "downfall of the Java sandbox as a security boundary"? Sounds interesting.

Not the GP, but the Java Sandbox is now deprecated.

There is an already closed deprecation ticket at openjdk.java.net.[1] For a blog post at inside.java see here.[2] Both links have some explanatory information.

[1] https://openjdk.java.net/jeps/411

[2] https://inside.java/2021/04/23/security-and-sandboxing-post-...

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

#49

Post by AlotOfReading »

joek1301 wrote: post #41
AlotOfReading wrote: post #31

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 i…

Could you elaborate / share resources on "downfall of the Java sandbox as a security boundary"? Sounds interesting.

This all dates from the old days of Java 1.x and applets. The original idea was that the JVM could perfectly sandbox applications from hardware resources, so the smart people at Sun came up a very forward thinking architecture: Untrusted code could be cryptographically signed by a root of trust. Then, bytecode would be formally verified to prove the absence of certain kinds of bad behavior. Then JVM would take care of various low level details like memory management. Finally, for any high level behavior there was something called the Security Manager that allowed 'fine grained' permissions for so-called dangerous APIs. All of this was the sandbox.

What happened in practice:

* The bytecode verifier ended up being accidentally quadratic, leading to straightforward DoS attacks

* The verifier kept having bugs, some of which stood for years

* It was impossible to enforce resource usage policies like "don't use all of my CPU". Since cryptocurrency is now a thing, this problem has become somewhat more severe than it was 20 years ago.

* The security model was useless in practice, because unverified or native code broke the entire thing. This remains an research open question under most conditions.

* Oh god the bugs. They were endless and the practical result was that the sandbox was never secure. [1] recapped 20 years of exploits, if you're curious about examples.

By the tail end of the system's life, even the public was completely fed up with it and mainstream media was publishing articles like [2]. Eventually even Oracle gave up and just deprecated both Applets and the SecurityManager system entirely [3].

[1] http://phrack.org/issues/70/7.html#article

[2] https://www.reuters.com/article/oracle-security/oracle-fixes...

[3] https://openjdk.java.net/jeps/411

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

#50

Post by AnimalMuppet »

_vdpp wrote: post #37
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.

The first such successful lawsuit is going to change the landscape. Not just "somewhat" - it's going to be a massive change.
Post reply on HN