19 ms·

Make formal verification and provably correct software practical and mainstream

204 points by _pyqs 4y ago

nimmer 4y ago
While this is a very ambitious goal, Nim implements formal proof for invariants using a theorem prover: https://nim-lang.org/docs/drnim.html https://nim-lang.org/docs/drnim.html
pid-1 4y ago
I've started watching Lamport's TLA+ course in YT and it totally blew my mind. What are other good resources in formal verification?
- dqpb 4y ago
  State Machines are the natural paradigm in TLA+. OOP is just poorly organized state machines. Try rewriting an OO program with state machines and you’ll have something that directly maps to TLA+, and it should demystify much of formal verification.
- homodeus 4y ago
  The Bible of formal software logic, free of charge: https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/
  - practal 4y ago
    If you are more practical than religious, try this: https://functional-algorithms-verified.org https://functional-algorithms-verified.org
- picardo 4y ago
  I found TLA+ syntax unapproachable as a beginner. I did more digging and discovered Alloy[0], a "lightweight" formal verification system, which is much simpler, and has industry adoption as well. It's working nicely for me so far. ----------- [0] http://alloytools.org/ http://alloytools.org/
eurasiantiger 4y ago
Can we formally verify the software cannot be used for evil?
- naniwaduni 4y ago
  gonna have to formally define evil
  - sharkbot 4y ago
    The constructivist in me thinks we could define it inductively :)
  - michaelsbradley 4y ago
    Evil: the privation of a good that should be present. It is the lack of a good that essentially belongs to a nature; the absence of a good that is natural and due to a being. Evil is therefore the absence of what ought to be there. https://www.catholicculture.org/culture/library/dictionary/index.cfm?id=33437&randomterm=false https://www.catholicculture.org/culture/library/dictionary/i... https://en.m.wikisource.org/wiki/Catholic_Encyclopedia_(1913)/Evil https://en.m.wikisource.org/wiki/Catholic_Encyclopedia_(1913...
    - moeris 4y ago
      - yjftsjthsd-h 4y ago
        > Like much of Christian thought, this is lazy to the extreme. > But it nonetheless fits this idiotic definition. Your personal bias is showing, to the point of going against the site guidelines; both 'When disagreeing, please reply to the argument instead of calling names. "That is idiotic; 1 + 1 is 2, not 3" can be shortened to "1 + 1 is 2, not 3."' and, y'know, literal religious flame warring. Also, you're either wrong or at least not correct; > Is ice cream that has thawed evil? No, rather obviously. You are of course welcome to argue that it's not, but yes, there are Christians who would/do make this exact argument; they might not claim that ice cream has the capacity to be willfully evil, but they would absolutely argue that ice cream melting is Wrong and a symptom of a Fallen world (in the sense of "fallen creation"), and that in a Good world ice cream would not melt.
Buttons840 4y ago
I applaud the research. Of course, those organizations creating and suffering from the most bugs will be the least able to utilize such a language.
daenz 4y ago
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.
- KSteffensen 4y ago
  Why does it always have to be all or nothing? Is your codebase 100% covered by unit tests? You don't have to make sure all the angles of your house are perfect right angles, but there's probably a couple that really have to be. Formally verify those and live with manageable imperfection for the rest.
  - daenz 4y ago
    "All or nothing" is not the point I'm making, it's "any or nothing." Unittests frequently have justifiable value for their effort, even when only providing partial coverage. I'm arguing that the effort involved in creating formal proofs for any part of your software is almost never worth the benefits, outside of mission critical applications, when a dozen simple unittests could provide 99.99% confidence. And certainly not worth it enough to become "mainstream", which is the title of the post.
- guerrilla 4y ago
  > if the cost involved to make software "provably correct" (time, salaries) is greater than the cost of the bugs, it will never be adopted. It may already be. Where's the research? It may not be happening just because of quarterly cycles, other misaligned incentives, culture or all kinds of other reasons. > 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. The difference is that those things are all within tolerances and serve their purposes and function correctly. Software often doesn't.
  - 4y ago
88913527 4y ago
For functional stuff, sure, but I don't think this is achievable within the UI domain. CSS rules have implementation details that change how you write it (some problems have workarounds), for example there's a documented set of issues in flex implementations maintained here: https://github.com/philipwalton/flexbugs https://github.com/philipwalton/flexbugs It might be practical and possible to become mainstream for some domains, but it's doubtful for others. The most practical solution for UI is visual regression testing across browsers.
- blainehansen 4y ago
  Hi, maintainer/author of Magmide here: https://github.com/magmide/magmide#isnt-most-software-too-fuzzy-or-quickly-evolving-to-make-verification-worth-the-effort https://github.com/magmide/magmide#isnt-most-software-too-fu...
Animats 4y ago
"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 writing reliable computer programs. More than anything else, verifying a program requires that one have a very clear understanding of the program’s desired behavior. It is not verification that is hard to understand; verification is fundamentally simple. It is really understanding programs that can be hard."[1] What typically goes wrong is one or more of the following: 1) The verification statements are in a totally different syntax than the code. 2) The verification statements are in different files than the code. 3) The basic syntax and semantics of the verification statements are not checked by the regular compiler. In too many systems, it's a comment to the compiler. 4) The verification toolchain and compile toolchain are completely separate. None of this is theory. It's all tooling and ergonomics. Then, there's 5) Too much gratuitous abstraction. The old version was "everything is predicate calculus". The new version is "everything is a type" and "everything is functional". [1] http://www.animats.com/papers/verifier/verifiermanual.pdf http://www.animats.com/papers/verifier/verifiermanual.pdf
- practal 4y ago
  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 order to come up with a notion of correctness for it, and actually prove it, might require something significantly more complicated. Infatuation with Hoare-Logic is part of the problem (that's what the paper you link uses, I think?). Thinking that verifying programs is easier than doing proper math on the computer is a dead end. First get mathematicians to actually like doing proofs with the help of a computer. THEN you might have a chance of tackling more practical applications like program verification without using an insane amount of resources.
csande17 4y ago
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'm not sure formal techniques will be as useful when expanded to other areas. Most of the bugs I encounter day-to-day happen because the programmer had the wrong goal in mind -- if you asked them to create a formal proof that their code worked, they would be able to do that, but it would be a proof that their function did a thing which was not actually the thing we wanted. (Similarly to, e.g., unit tests that do not actually test anything because they're just line-by-line reproductions of the original code but with every function call mocked out.) Has anyone successfully applied proof techniques to reduce defects in UI development, "business logic", or similarly fuzzy disciplines?
- er4hn 4y ago
  I would love to see a fuzzer applied to business logic. It should take design requests from PMs and execucritters and ask pointed questions about edge cases.
  - Transfinity 4y ago
    I love this idea. I bet you could get surprisingly useful results just using a language model like GPT-3.
- johnbender 4y ago
  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.
  - pydry 4y ago
yourapostasy 4y ago
> ...existing uses of Iris perform the proofs "on the side" using transcribed syntax tree versions of the target code rather than directly reading the original source. I'm a formal verification dummy, so can someone please confirm if this means these uses of Iris are creating an Abstract Syntax Tree (AST) of the source, then operating upon that AST? If so, can I please get an ELI5 why there is a salient formal verification outcomes difference between using the AST and "directly reading the original source"?
toast0 4y ago
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.
- _vdpp 4y ago
  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.
muglug 4y ago
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't know enough about the area to pursuade skeptical managers. Unless a big company comes forward with a bunch of case studies about how they used formal verification successfully I can't see the developer mindset changing.
- _vdpp 4y ago
  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).
  - muglug 4y ago
    I meant to say "this hopes to build on the success of Rust" — Rust is explicitly called out in the readme.
- deleted 4y ago
  [deleted]
AlotOfReading 4y ago
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-magmide.md https://github.com/magmide/magmide/blob/main/posts/design-of...
- joek1301 4y ago
  Could you elaborate / share resources on "downfall of the Java sandbox as a security boundary"? Sounds interesting.
  - AlotOfReading 4y ago
    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 http://phrack.org/issues/70/7.html#article [2] https://www.reuters.com/article/oracle-security/oracle-fixes-42-holes-in-java-to-revive-security-confidence-idUKL2N0D32C620130416 https://www.reuters.com/article/oracle-security/oracle-fixes... [3] https://openjdk.java.net/jeps/411 https://openjdk.java.net/jeps/411
_vdpp 4y ago
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.
hn_urbit_thr123 4y ago
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.
- AnimalMuppet 4y ago
  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 essentially the same problem. In fact, perhaps all of formal verification has this kind of problem. How do you prove the benefits to someone who doesn't know the tools?
  - hn_urbit_thr123 4y ago
    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.
  - blainehansen 4y ago
    Hi, maintainer/author of Magmide here: https://github.com/magmide/magmide#is-it-actually-useful-to-prove-code-meets-some-specification-if-we-still-have-to-trust-the-specification https://github.com/magmide/magmide#is-it-actually-useful-to-...
- milkey_mouse 4y ago
  Urbit has not put much effort into security, for some reason. To be fair, they don't claim their runtime is secure (yet)[1]. The process downloading and executing code from the network is not sandboxed with seccomp or anything similar, and its "jets" are unverified C libraries which any of this code is allowed to call into. They could sandbox it pretty easily (the worker process which runs third-party code only talks to a host process and not the rest of the world, so it could probably be run under seccomp, not even seccomp-bpf) which makes it all the more surprising that they haven't. Urbit has also had (and almost certainly still has) bugs where jets give different results than the code they're supposed to accelerate (a "jet mismatch") [2]. I agree that its "axiomatic" bytecode would lend itself well to verification theoretically, but Urbit as she is spoke is not anywhere close. They also at least historically seemed somewhat hostile towards academic CS research (including formal methods) probably for weird Moldbug reasons. [1]: https://urbit.org/faq#:~:text=The%20security%20of%20the%20runtime%2C%20Vere%2C%20has%20not%20yet%20been%20adequately%20assessed%20or%20systematically%20hardened https://urbit.org/faq#:~:text=The%20security%20of%20the%20ru.... [2]: https://urbit.org/blog/common-objections-to-urbit#:~:text=Yes%2C%20formal%20verification%20of%20jet%20equivalence%20is%20desirable.%20However https://urbit.org/blog/common-objections-to-urbit#:~:text=Ye...
digitalice 4y ago
Been following the development of Dafny: https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/ https://www.microsoft.com/en-us/research/project/dafny-a-lan...
- tgv 4y ago
  Looks interesting, perhaps because it seems to be a bit more down to earth than some of the other proposals where you have to derive Whitehead&Russell before you're allowed to use the + operator. But it also seems quite dead. The latest link is from 2012.
  - hath995 4y ago
    It is still alive, it has just moved to github! It is a big language and it can prove useful programs. Apparently, part of the Ethereum 2 specification was verified using it. https://github.com/dafny-lang/dafny https://github.com/dafny-lang/dafny I have been learning it and the syntax is close to most C style programming languages. As a software developer this makes it much more approachable than Coq. The proof statements also feel more like the math I learned in college rather than the weird magic keywords of Coq.
    - tgv 4y ago
      Thanks. Pretty cool.
Cloudef 4y ago
Do we have formal verification for formal verification yet? I want to make sure my verification does not have bugs.
- mjb 4y ago
  Yes, it's an active area of research. One very recent example, focusing on Dafny: https://www.amazon.science/publications/testing-dafny-experience-paper https://www.amazon.science/publications/testing-dafny-experi...
akomtu 4y ago
I 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%.
- blainehansen 4y ago
  Hi, maintainer/author of Magmide here: https://github.com/magmide/magmide#isnt-is-undecidable-to-prove-a-program-terminates-or-is-correct https://github.com/magmide/magmide#isnt-is-undecidable-to-pr...
- warkdarrior 4y ago
  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.
  - mbrodersen 4y ago
    Termination is undecidable in general but that is not a problem in practice. Proof assistants like Coq, LEAN etc. can automatically prove termination for most practical code. And if not, the developer has to prove termination by hand. Which is not hard in most cases I have encountered. And if you still can’t do it you simply add a “fuel” natural number counter that guarantees termination (exit when out of fuel).
- mbrodersen 4y ago
  It turns out that you can write proven correct C compilers (CompCert), proven correct Operating Systems (seL4), and proven correct secure network protocols using proof assistants like Coq and F*. All of those proof assistants are using languages that are not Turing complete. You have to prove termination if the proof assistants can’t automatically prove it. So being Turing complete is not really necessary for writing complex software.
markisus 4y ago
I think there is a project quite similar to this one called Verifiable Software Toolchain (VST) in which you can write a C program, convert it into a massive Coq expression, and then write theorems about that expression in Coq. The Software Foundations series has a volume about it [1], which I found to be an order of magnitude harder to understand than the other volumes. It feels like the magmide project aims to the same goal as VST. It's unclear how it will improve on what VST has done. It may just be that formal verification of real world languages is inherently complex. [1] https://softwarefoundations.cis.upenn.edu/vc-current/index.html https://softwarefoundations.cis.upenn.edu/vc-current/index.h...
jandrewrogers 4y ago
I 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.
yjftsjthsd-h 4y ago
So this actually looks really neat if it works. However, hopefully in the spirit of constructive criticism, I would be very nervous about sticking this in big letters at the top of the introduction: > Software can literally be perfect because that is a wonderful way to get people to invest in really robust, excellent, high-quality software - and then trust it blindly and ignore that even if everything goes well and the software is itself perfect, and the verification has no bugs, and the model that it perfectly implements actually maps the problem space correctly, it will still run on fallible hardware, interfacing with other software that is imperfect, taking direction and data from humans who can make mistakes. Now to the author's credit! Further down, under "Do you think this language will make all software perfectly secure?" and "Is logically verifying code even useful if that code relies on possibly faulty software/hardware?", this is discussed. And I think the writer actually does appreciate the limits of what this can actually do, and I very much appreciate them explaining that in what I'd call clear terms. Just... maybe don't headline with a claim like that when it has caveats and people are liable to read the claim and ignore the caveats?
jbaba101 4y ago
I want to understand what is verification process? How would programming will take new step forward if this is achieved? I have been programmer for a while but I don't understand context and discussion around verification. Please point me any useful resources which can give me deep understanding of what's being discussed here.
xavxav 4y ago
Honestly, to me this project is a means seeking an end, the same way JS devs love to play around with frontend frameworks, the author saw a bunch of shiny powerful (highly complex) tools and decided that combining them all was the solution to our problems. I don't want to discourage them from learning Iris, or designing a dependently typed language, but I really think that's missing the difficulty in formal verification. I think the two areas that need focus are: ease of specification and automation. In short, we need to lower the cost of verifying a line of code, by at least an order of magnitude. These two objectives are also directly opposed to the direction Magmide sets as the goal. Ease of specification means we want to use the least amount of seperation logic possible, and hide it from the user if possible. Doing proofs / writing specs in seperation logic sucks and not for interesting reasons. Automation means favoring simpler logics, specifically we want to stick as much as possible to FOL since that's where we have good automation. By doing everything in a rich dependently typed language from the start it also makes it harder to do incremental verification, I think there is a lot of value in having a 'pyramid of trust' with more and more powerful tools which take you up a level of trust and verification, potentially requiring more input from engineers as they go up. Finally, I think there's a lot of potential to explore in the interfaces we use to write, read, and debug proofs. I don't think tactic languages (as exist today) are the last word, and I think we should be doing a lot more interesting things to interface with and explore the proofs.
- blainehansen 4y ago
  Hi, maintainer/author of Magmide here: https://github.com/magmide/magmide#gradually-verifiable https://github.com/magmide/magmide#gradually-verifiable https://github.com/magmide/magmide#fully-reusable https://github.com/magmide/magmide#fully-reusable https://github.com/magmide/magmide#isnt-formal-verification-impractical-in-practice https://github.com/magmide/magmide#isnt-formal-verification-...
mkleczek 4y ago
“Complexity is the business we are in, and complexity is what limits us.” Yet, just as Turski recognized, some people seem to be philosophically offended by this notion, and try to fight the proven limitations. They are under the impression that the world — and I’m not just talking about computing now — is essentially simple, and it the stupidity of people and institution that needlessly complicate it (or, in the case of software, “stupid” programming languages). If we apply careful mathematical reasoning, we could find solutions to anything. Computer science is the very discipline that proved that essential complexity can arise even in the smallest of systems. Yet sometimes it is computer scientists and software developers who attempt to challenge the very foundation of their own discipline. Complexity is essential. It cannot be tamed, and there is no one big answer. The quote is from excellent https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity and it would be really good if the authors read it carefully first.
vivegi 4y ago
One of the approaches for formal program verification is to convert an unrestricted grammar G_1 into a context-sensitive grammar G_2 subject to some constraints C. We then derive a linear bounded automaton A_2 that accepts the language L(G_2). We then transform the input program i.e., a string S_1 in L(G_1) to a modified program i.e., a string S_2 in L(G_2). If A_2 halts on S_2 then A_1 halts on S_1. By definition, A_2 accepts S_2. Therefore, A_1 accepts S_1. Of course, L(G_2) is a subset of L(G_1) which means that many programs written in G_1 that do not meet the constraints C cannot be verified. But the benefit is that programs that do meet the constraints C are provably verified. The tension lies in keeping C small and maximizing utility of the approach for a wide class of programs/libraries/programming paradigms etc.,
namibj 4y ago
I've been looking at writing a code generator, which spits out vectorized code for multi-way joins (kind of like "dynamic programming" to not suffer from being locked in a specific order of binary joins), with the additional complications of being for the incremental/difference-based "Differential Dataflow"[0], the multi-temporal aspect DDFlow needs to handle it's iterative/fixpoint operator, and dynamically adjusting IO concurrency (the asymptotics of part of the "dynamic programming" index traversal suffer when squeezing concurrency out of it, as it's pretty much cache prefetching). It's been about a year since I realized the impact of a JIT-like query compiler for these kinds of join-project queries, but needing to balance IOPS, vectorization, and likely even applying (vectorized) B-tree tactics within a 4k page, on top of the weirdness from multi-temporal (not just bi-temporal) delta-based records (~change-data-capture stream; needs to be integrated/materialized to get a point-in-time view)... sounds like a recipe for logic bugs/off-by-one errors. They are already hard-to-impossible to notice if it'd be used in production, it being a code generator allows situations with only edge case queries having data-dependent edge case bugs, and the addition of dynamic/adaptive IO concurrency makes reproducing/debugging a detected error next to impossible. I wouldn't dare to trust the code generator I'd write, if not formally verified. Not because I don't have faith in my skills, but because it's extremely complex code that has to be fast and fall out of a JIT and it's nature makes off-by-one errors in index access unusually likely. And debugging a known error might well be harder than formally verifying to find the bug. [0]: https://news.ycombinator.com/item?id=25867693 https://news.ycombinator.com/item?id=25867693 https://news.ycombinator.com/item?id=27512224 https://news.ycombinator.com/item?id=27512224 TL;DR: There is code that would be useful if written, but is so complex and neigh-impossible to debug that formally verifying it might be easier than debugging it to "production-grade". I hope this project makes that kind of approach practical for those engineers who could write the code and make it pass integration tests.
mkl95 4y ago
Many engineers and teams are aware that they write bad code, and they love it. You can get very far as a clumsy code vendor. Even if formal verification was practical, it would be pretty difficult to make it mainstream.
deleted 4y ago
[deleted]
nottorp 4y ago
You can prove that an algorithm is correct most of the time (yes, halting and decidability but for practical purposes you mostly can). How do you prove an event driven application is correct?
- Thiez 4y ago
  Modelling your application as a state machine will allow you to use model checking to prove various properties about your model. Proving that your program is equivalent (for some chosen definition of equivalence) to the state machine is left as an exercise for the reader.
  - nottorp 4y ago
    > Proving that your program is equivalent (for some chosen definition of equivalence) to the state machine is left as an exercise for the reader. "It's obvious" :)
IngoBlechschmid 4y ago
Try the proof assistant Agda without installation directly in your browser: https://agdapad.quasicoherent.io/ https://agdapad.quasicoherent.io/ Or Lean: https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_g...
ChrisMarshallNY 4y ago
While I laud the goals, I am skeptical of the ability to met them. I very much believe that there is an industry-wide crisis of terrible software, but I don't believe that it's practical to go directly from "garbage to gold." The path is long, and far from straight. Best Practices are how engineering disciplines, throughout history, have achieved progress in Quality. Currently, Best Practices aren't really a "thing," in software development, and it shows. People like Steve McConnell are not really respected, and a general culture of "move fast and break things" is still pervasive. Engineers flit around companies like mayflies, techniques and libraries come and go, and there's an enormous reliance on dependencies with very little vetting. We spend so much time, trying to perfect our tools, without trying to perfect ourselves. Academics and theorists have been proposing languages, libraries, infrastructure, and management practices that are designed to change lead into gold for decades, yet it never seems to happen. I have always been a fan of self-Discipline, and the apprenticeship model. That requires a lot of social infrastructure that does not currently exist. It's as old as human history, and absolutely proven to achieve results. "In theory, there is no difference between theory and practice; while in practice, there is." -Benjamin Brewster "It is not enough to do your best; you must know what to do, and THEN do your best." -W. Edwards Deming "The significant problems we face cannot be solved by the same level of thinking that created them." -Albert Einstein "Everyone thinks of changing the world, but not one thinks of changing himself." -Tolstoy https://xkcd.com/2030/ https://xkcd.com/2030/
- zozbot234 4y ago
  > While I laud the goals, I am skeptical of the ability to met them. Let's start with the easiest part, and rewrite everything in Rust (or a comparably safe language). We'll need something like this anyway to give our software a workable semantics that's free of UB (at least wrt. the "safe" checked subset). Then we can work on the harder problem of using proof to establish that the unchecked parts do not invoke UB, and that intended specifications are not violated even in the "safe" parts.
  - formerly_proven 4y ago
    Tons of, if not most, "move fast and break things" software is written in safe languages, not C or C++.
Genbox 4y ago
Microsoft developed the excellent Code Contracts[1] project. From the user's perpective, tt was a simple class called Contracts with a few methods such as Require(), Ensure() and Invariant() Underneath the hood it used the Z3 Solver[2], which is both intuitive, flexible and fast. It validated the contracts while coding and highlighted in the Visual Studio IDE when a contract was broken. You could write something like: Contracts.Requires(x > 5 && y > x); Which would get translated to a compile time check as well. Unfortunately, Code Contracts has been dead for years now, and it was even removed entirely from .NET[3] due to being hard to maintain, and the verifier stopped working in newer versions of VS. Luckily, C# developers now have a small taste of contracts due to nullability analysis[4], but even more exciting is that contracts is making its way into C# as a first-level standard[5]. [1] https://www.microsoft.com/en-us/research/project/code-contracts/ https://www.microsoft.com/en-us/research/project/code-contra... [2] https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3 [3] https://github.com/dotnet/runtime/issues/20006 https://github.com/dotnet/runtime/issues/20006 [4] https://docs.microsoft.com/en-us/dotnet/csharp/nullable-references https://docs.microsoft.com/en-us/dotnet/csharp/nullable-refe... [5] https://github.com/dotnet/csharplang/issues/105 https://github.com/dotnet/csharplang/issues/105
pron 4y ago
Wow, the language here is even more optimisitc than the rosiest descriptions you see from young researchers, which prompted me to check if the author has had much experience deductively verifying interesting "deep" functional properties of non-trivial programs. The answer seems to be no. Like a newcomer to the field, he focuses on "first-day" problems such as language convenience, but the answer to his question of why this hasn't been done before is because that's not the hard problem, something he'll know once he obtains more experience. One of the biggest issues — indeed, the problem separation logic tries to address, but does so successfully only for relatively simple properties — is that "correctness" does not feasibly (affordably) compose. The difficulty of proving the correctness of a program made out of components, each of which has already been proven correct for any desired property is not easier than proving the correctness of the program from scratch, without concern for its decomposition. I.e. proving the correctness of a program made of ten provably-correct 500-line components is no easier than proving the correctness of all 5000 lines at once. This has been shown to be the case not only in the theoretical worst case, but also in practice. Here's an example to make things concrete. Suppose we have the following (Java) method, calling some unknown, pure, `bar` method: long foo(long x) { if (x <= 2 || (x & 1) != 0) return 0; for (long i = x; i > 0; i--) if (bar(i) && bar(x - i)) return i; throw new Error(); } It is very easy to describe exactly under what conditions an error would be thrown. Similarly, it is easy to describe the operation of the following method, and prove that it performs its function correctly: boolean bar(long x) { for (long i = x - 1; i >= 2; i--) for (long s = x; s >= 0; s -= i) if (s == 0) return false; return true; } However, it is not easy to determine which inputs, if any, would cause foo to throw an error using that particular bar. In fact, we only happen to know that this particular question is extremely hard because it is one that has interested mathematicians for 300 years and remains unanswered. While most verification tasks don't neatly correspond to well-known mathematical problems, and most require far less than 300 years to figure out, this kind of difficulty is encountered by anyone who tries to deductively verify non-trivial programs for anything but very specific properties (such as "there's no memory corruption", which separation logic does help with). Various kinds of non-determinism, such as the result of concurrency or any kind of interaction, only makes the possible compositions more complex. In short, the effort it takes to verify a program does not scale nicely with its size, even when it is neatly decomposed, and it is this practical affordability — which is not a result of the elegance of the tools used — that makes this subject so challenging (and interesting), and requires some humility and lowering of expectations even when it is useful (and it can be certainly useful when yielded properly and at the right scope). Another problem is an incorrect model of how programs are constructed. One might think that if a programmer has written a program, then they must have some informal (but deductive) model of it in their mind, and all that's missing is "just" formally specifying it. But that is not how programs are constructed over time when many people are involved. In practice, programmers often depend on inductive properties in their assumptions, such as "if the software survived for many years, then local changes are unlikely to have global effects that aren't caught by existing tests." Those assumptions are good enough for providing the (often sufficient) level of correctness we already reach, but insufficient for constructing software that can be formally specified, let alone deductively proven correct. That is why much of the contemporary research focuses on less sound approaches, that aren't fully deductive, such as concolic testing (e.g. Klee), that allow better scaling for both specification and verification at the cost of "perfection". The reason why both research and industry don't all do what is proposed here is because they know that's not where to real problems are. There are bigger issues to tackle before making the languages more beginner-friendly.
dgb23 4y ago
I recently came across Ur/web. It makes some promises that are quite attractive. One of the benefits of having a DSL rather than something general purpose is that it can make these promises in a more comprehensive and focused manner. But despite being around for a while now it didn’t get adopted very widely.
deleted 4y ago
[deleted]

204 points by _pyqs 4y ago

While this is a very ambitious goal, Nim implements formal proof for invariants using a theorem prover: https://nim-lang.org/docs/drnim.html https://nim-lang.org/docs/drnim.html

pid-1 4y ago

I've started watching Lamport's TLA+ course in YT and it totally blew my mind. What are other good resources in formal verification?

dqpb 4y ago
State Machines are the natural paradigm in TLA+. OOP is just poorly organized state machines. Try rewriting an OO program with state machines and you’ll have something that directly maps to TLA+, and it should demystify much of formal verification.
homodeus 4y ago
The Bible of formal software logic, free of charge: https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/
- practal 4y ago
  If you are more practical than religious, try this: https://functional-algorithms-verified.org https://functional-algorithms-verified.org
picardo 4y ago
I found TLA+ syntax unapproachable as a beginner. I did more digging and discovered Alloy[0], a "lightweight" formal verification system, which is much simpler, and has industry adoption as well. It's working nicely for me so far. ----------- [0] http://alloytools.org/ http://alloytools.org/

eurasiantiger 4y ago

Can we formally verify the software cannot be used for evil?

naniwaduni 4y ago
gonna have to formally define evil
- sharkbot 4y ago
  The constructivist in me thinks we could define it inductively :)
- michaelsbradley 4y ago
  Evil: the privation of a good that should be present. It is the lack of a good that essentially belongs to a nature; the absence of a good that is natural and due to a being. Evil is therefore the absence of what ought to be there. https://www.catholicculture.org/culture/library/dictionary/index.cfm?id=33437&randomterm=false https://www.catholicculture.org/culture/library/dictionary/i... https://en.m.wikisource.org/wiki/Catholic_Encyclopedia_(1913)/Evil https://en.m.wikisource.org/wiki/Catholic_Encyclopedia_(1913...
  - moeris 4y ago
    - yjftsjthsd-h 4y ago
      > Like much of Christian thought, this is lazy to the extreme. > But it nonetheless fits this idiotic definition. Your personal bias is showing, to the point of going against the site guidelines; both 'When disagreeing, please reply to the argument instead of calling names. "That is idiotic; 1 + 1 is 2, not 3" can be shortened to "1 + 1 is 2, not 3."' and, y'know, literal religious flame warring. Also, you're either wrong or at least not correct; > Is ice cream that has thawed evil? No, rather obviously. You are of course welcome to argue that it's not, but yes, there are Christians who would/do make this exact argument; they might not claim that ice cream has the capacity to be willfully evil, but they would absolutely argue that ice cream melting is Wrong and a symptom of a Fallen world (in the sense of "fallen creation"), and that in a Good world ice cream would not melt.

Buttons840 4y ago

I applaud the research. Of course, those organizations creating and suffering from the most bugs will be the least able to utilize such a language.

daenz 4y ago

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.

KSteffensen 4y ago
Why does it always have to be all or nothing? Is your codebase 100% covered by unit tests? You don't have to make sure all the angles of your house are perfect right angles, but there's probably a couple that really have to be. Formally verify those and live with manageable imperfection for the rest.
- daenz 4y ago
  "All or nothing" is not the point I'm making, it's "any or nothing." Unittests frequently have justifiable value for their effort, even when only providing partial coverage. I'm arguing that the effort involved in creating formal proofs for any part of your software is almost never worth the benefits, outside of mission critical applications, when a dozen simple unittests could provide 99.99% confidence. And certainly not worth it enough to become "mainstream", which is the title of the post.
guerrilla 4y ago
> if the cost involved to make software "provably correct" (time, salaries) is greater than the cost of the bugs, it will never be adopted. It may already be. Where's the research? It may not be happening just because of quarterly cycles, other misaligned incentives, culture or all kinds of other reasons. > 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. The difference is that those things are all within tolerances and serve their purposes and function correctly. Software often doesn't.
- 4y ago

88913527 4y ago

For functional stuff, sure, but I don't think this is achievable within the UI domain. CSS rules have implementation details that change how you write it (some problems have workarounds), for example there's a documented set of issues in flex implementations maintained here: https://github.com/philipwalton/flexbugs https://github.com/philipwalton/flexbugs It might be practical and possible to become mainstream for some domains, but it's doubtful for others. The most practical solution for UI is visual regression testing across browsers.

blainehansen 4y ago
Hi, maintainer/author of Magmide here: https://github.com/magmide/magmide#isnt-most-software-too-fuzzy-or-quickly-evolving-to-make-verification-worth-the-effort https://github.com/magmide/magmide#isnt-most-software-too-fu...

Animats 4y ago

"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 writing reliable computer programs. More than anything else, verifying a program requires that one have a very clear understanding of the program’s desired behavior. It is not verification that is hard to understand; verification is fundamentally simple. It is really understanding programs that can be hard."[1] What typically goes wrong is one or more of the following: 1) The verification statements are in a totally different syntax than the code. 2) The verification statements are in different files than the code. 3) The basic syntax and semantics of the verification statements are not checked by the regular compiler. In too many systems, it's a comment to the compiler. 4) The verification toolchain and compile toolchain are completely separate. None of this is theory. It's all tooling and ergonomics. Then, there's 5) Too much gratuitous abstraction. The old version was "everything is predicate calculus". The new version is "everything is a type" and "everything is functional". [1] http://www.animats.com/papers/verifier/verifiermanual.pdf http://www.animats.com/papers/verifier/verifiermanual.pdf

practal 4y ago
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 order to come up with a notion of correctness for it, and actually prove it, might require something significantly more complicated. Infatuation with Hoare-Logic is part of the problem (that's what the paper you link uses, I think?). Thinking that verifying programs is easier than doing proper math on the computer is a dead end. First get mathematicians to actually like doing proofs with the help of a computer. THEN you might have a chance of tackling more practical applications like program verification without using an insane amount of resources.

csande17 4y ago

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'm not sure formal techniques will be as useful when expanded to other areas. Most of the bugs I encounter day-to-day happen because the programmer had the wrong goal in mind -- if you asked them to create a formal proof that their code worked, they would be able to do that, but it would be a proof that their function did a thing which was not actually the thing we wanted. (Similarly to, e.g., unit tests that do not actually test anything because they're just line-by-line reproductions of the original code but with every function call mocked out.) Has anyone successfully applied proof techniques to reduce defects in UI development, "business logic", or similarly fuzzy disciplines?

er4hn 4y ago
I would love to see a fuzzer applied to business logic. It should take design requests from PMs and execucritters and ask pointed questions about edge cases.
- Transfinity 4y ago
  I love this idea. I bet you could get surprisingly useful results just using a language model like GPT-3.
johnbender 4y ago
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.
- pydry 4y ago

yourapostasy 4y ago

> ...existing uses of Iris perform the proofs "on the side" using transcribed syntax tree versions of the target code rather than directly reading the original source. I'm a formal verification dummy, so can someone please confirm if this means these uses of Iris are creating an Abstract Syntax Tree (AST) of the source, then operating upon that AST? If so, can I please get an ELI5 why there is a salient formal verification outcomes difference between using the AST and "directly reading the original source"?

toast0 4y ago

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.

_vdpp 4y ago
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.

muglug 4y ago

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't know enough about the area to pursuade skeptical managers. Unless a big company comes forward with a bunch of case studies about how they used formal verification successfully I can't see the developer mindset changing.

_vdpp 4y ago
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).
- muglug 4y ago
  I meant to say "this hopes to build on the success of Rust" — Rust is explicitly called out in the readme.
deleted 4y ago
[deleted]

AlotOfReading 4y ago

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-magmide.md https://github.com/magmide/magmide/blob/main/posts/design-of...

joek1301 4y ago
Could you elaborate / share resources on "downfall of the Java sandbox as a security boundary"? Sounds interesting.
- AlotOfReading 4y ago
  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 http://phrack.org/issues/70/7.html#article [2] https://www.reuters.com/article/oracle-security/oracle-fixes-42-holes-in-java-to-revive-security-confidence-idUKL2N0D32C620130416 https://www.reuters.com/article/oracle-security/oracle-fixes... [3] https://openjdk.java.net/jeps/411 https://openjdk.java.net/jeps/411

_vdpp 4y ago

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.

hn_urbit_thr123 4y ago

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.

AnimalMuppet 4y ago
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 essentially the same problem. In fact, perhaps all of formal verification has this kind of problem. How do you prove the benefits to someone who doesn't know the tools?
- hn_urbit_thr123 4y ago
  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.
- blainehansen 4y ago
  Hi, maintainer/author of Magmide here: https://github.com/magmide/magmide#is-it-actually-useful-to-prove-code-meets-some-specification-if-we-still-have-to-trust-the-specification https://github.com/magmide/magmide#is-it-actually-useful-to-...
milkey_mouse 4y ago
Urbit has not put much effort into security, for some reason. To be fair, they don't claim their runtime is secure (yet)[1]. The process downloading and executing code from the network is not sandboxed with seccomp or anything similar, and its "jets" are unverified C libraries which any of this code is allowed to call into. They could sandbox it pretty easily (the worker process which runs third-party code only talks to a host process and not the rest of the world, so it could probably be run under seccomp, not even seccomp-bpf) which makes it all the more surprising that they haven't. Urbit has also had (and almost certainly still has) bugs where jets give different results than the code they're supposed to accelerate (a "jet mismatch") [2]. I agree that its "axiomatic" bytecode would lend itself well to verification theoretically, but Urbit as she is spoke is not anywhere close. They also at least historically seemed somewhat hostile towards academic CS research (including formal methods) probably for weird Moldbug reasons. [1]: https://urbit.org/faq#:~:text=The%20security%20of%20the%20runtime%2C%20Vere%2C%20has%20not%20yet%20been%20adequately%20assessed%20or%20systematically%20hardened https://urbit.org/faq#:~:text=The%20security%20of%20the%20ru.... [2]: https://urbit.org/blog/common-objections-to-urbit#:~:text=Yes%2C%20formal%20verification%20of%20jet%20equivalence%20is%20desirable.%20However https://urbit.org/blog/common-objections-to-urbit#:~:text=Ye...

digitalice 4y ago

Been following the development of Dafny: https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/ https://www.microsoft.com/en-us/research/project/dafny-a-lan...

tgv 4y ago
Looks interesting, perhaps because it seems to be a bit more down to earth than some of the other proposals where you have to derive Whitehead&Russell before you're allowed to use the + operator. But it also seems quite dead. The latest link is from 2012.
- hath995 4y ago
  It is still alive, it has just moved to github! It is a big language and it can prove useful programs. Apparently, part of the Ethereum 2 specification was verified using it. https://github.com/dafny-lang/dafny https://github.com/dafny-lang/dafny I have been learning it and the syntax is close to most C style programming languages. As a software developer this makes it much more approachable than Coq. The proof statements also feel more like the math I learned in college rather than the weird magic keywords of Coq.
  - tgv 4y ago
    Thanks. Pretty cool.

Cloudef 4y ago

Do we have formal verification for formal verification yet? I want to make sure my verification does not have bugs.

mjb 4y ago
Yes, it's an active area of research. One very recent example, focusing on Dafny: https://www.amazon.science/publications/testing-dafny-experience-paper https://www.amazon.science/publications/testing-dafny-experi...

akomtu 4y ago

I 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%.

blainehansen 4y ago
Hi, maintainer/author of Magmide here: https://github.com/magmide/magmide#isnt-is-undecidable-to-prove-a-program-terminates-or-is-correct https://github.com/magmide/magmide#isnt-is-undecidable-to-pr...
warkdarrior 4y ago
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.
- mbrodersen 4y ago
  Termination is undecidable in general but that is not a problem in practice. Proof assistants like Coq, LEAN etc. can automatically prove termination for most practical code. And if not, the developer has to prove termination by hand. Which is not hard in most cases I have encountered. And if you still can’t do it you simply add a “fuel” natural number counter that guarantees termination (exit when out of fuel).
mbrodersen 4y ago
It turns out that you can write proven correct C compilers (CompCert), proven correct Operating Systems (seL4), and proven correct secure network protocols using proof assistants like Coq and F*. All of those proof assistants are using languages that are not Turing complete. You have to prove termination if the proof assistants can’t automatically prove it. So being Turing complete is not really necessary for writing complex software.

markisus 4y ago

I think there is a project quite similar to this one called Verifiable Software Toolchain (VST) in which you can write a C program, convert it into a massive Coq expression, and then write theorems about that expression in Coq. The Software Foundations series has a volume about it [1], which I found to be an order of magnitude harder to understand than the other volumes. It feels like the magmide project aims to the same goal as VST. It's unclear how it will improve on what VST has done. It may just be that formal verification of real world languages is inherently complex. [1] https://softwarefoundations.cis.upenn.edu/vc-current/index.html https://softwarefoundations.cis.upenn.edu/vc-current/index.h...

jandrewrogers 4y ago

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

yjftsjthsd-h 4y ago

So this actually looks really neat if it works. However, hopefully in the spirit of constructive criticism, I would be very nervous about sticking this in big letters at the top of the introduction: > Software can literally be perfect because that is a wonderful way to get people to invest in really robust, excellent, high-quality software - and then trust it blindly and ignore that even if everything goes well and the software is itself perfect, and the verification has no bugs, and the model that it perfectly implements actually maps the problem space correctly, it will still run on fallible hardware, interfacing with other software that is imperfect, taking direction and data from humans who can make mistakes. Now to the author's credit! Further down, under "Do you think this language will make all software perfectly secure?" and "Is logically verifying code even useful if that code relies on possibly faulty software/hardware?", this is discussed. And I think the writer actually does appreciate the limits of what this can actually do, and I very much appreciate them explaining that in what I'd call clear terms. Just... maybe don't headline with a claim like that when it has caveats and people are liable to read the claim and ignore the caveats?

jbaba101 4y ago

I want to understand what is verification process? How would programming will take new step forward if this is achieved? I have been programmer for a while but I don't understand context and discussion around verification. Please point me any useful resources which can give me deep understanding of what's being discussed here.

xavxav 4y ago

Honestly, to me this project is a means seeking an end, the same way JS devs love to play around with frontend frameworks, the author saw a bunch of shiny powerful (highly complex) tools and decided that combining them all was the solution to our problems. I don't want to discourage them from learning Iris, or designing a dependently typed language, but I really think that's missing the difficulty in formal verification. I think the two areas that need focus are: ease of specification and automation. In short, we need to lower the cost of verifying a line of code, by at least an order of magnitude. These two objectives are also directly opposed to the direction Magmide sets as the goal. Ease of specification means we want to use the least amount of seperation logic possible, and hide it from the user if possible. Doing proofs / writing specs in seperation logic sucks and not for interesting reasons. Automation means favoring simpler logics, specifically we want to stick as much as possible to FOL since that's where we have good automation. By doing everything in a rich dependently typed language from the start it also makes it harder to do incremental verification, I think there is a lot of value in having a 'pyramid of trust' with more and more powerful tools which take you up a level of trust and verification, potentially requiring more input from engineers as they go up. Finally, I think there's a lot of potential to explore in the interfaces we use to write, read, and debug proofs. I don't think tactic languages (as exist today) are the last word, and I think we should be doing a lot more interesting things to interface with and explore the proofs.

blainehansen 4y ago
Hi, maintainer/author of Magmide here: https://github.com/magmide/magmide#gradually-verifiable https://github.com/magmide/magmide#gradually-verifiable https://github.com/magmide/magmide#fully-reusable https://github.com/magmide/magmide#fully-reusable https://github.com/magmide/magmide#isnt-formal-verification-impractical-in-practice https://github.com/magmide/magmide#isnt-formal-verification-...

mkleczek 4y ago

“Complexity is the business we are in, and complexity is what limits us.” Yet, just as Turski recognized, some people seem to be philosophically offended by this notion, and try to fight the proven limitations. They are under the impression that the world — and I’m not just talking about computing now — is essentially simple, and it the stupidity of people and institution that needlessly complicate it (or, in the case of software, “stupid” programming languages). If we apply careful mathematical reasoning, we could find solutions to anything. Computer science is the very discipline that proved that essential complexity can arise even in the smallest of systems. Yet sometimes it is computer scientists and software developers who attempt to challenge the very foundation of their own discipline. Complexity is essential. It cannot be tamed, and there is no one big answer. The quote is from excellent https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity and it would be really good if the authors read it carefully first.

vivegi 4y ago

One of the approaches for formal program verification is to convert an unrestricted grammar G_1 into a context-sensitive grammar G_2 subject to some constraints C. We then derive a linear bounded automaton A_2 that accepts the language L(G_2). We then transform the input program i.e., a string S_1 in L(G_1) to a modified program i.e., a string S_2 in L(G_2). If A_2 halts on S_2 then A_1 halts on S_1. By definition, A_2 accepts S_2. Therefore, A_1 accepts S_1. Of course, L(G_2) is a subset of L(G_1) which means that many programs written in G_1 that do not meet the constraints C cannot be verified. But the benefit is that programs that do meet the constraints C are provably verified. The tension lies in keeping C small and maximizing utility of the approach for a wide class of programs/libraries/programming paradigms etc.,

namibj 4y ago

I've been looking at writing a code generator, which spits out vectorized code for multi-way joins (kind of like "dynamic programming" to not suffer from being locked in a specific order of binary joins), with the additional complications of being for the incremental/difference-based "Differential Dataflow"[0], the multi-temporal aspect DDFlow needs to handle it's iterative/fixpoint operator, and dynamically adjusting IO concurrency (the asymptotics of part of the "dynamic programming" index traversal suffer when squeezing concurrency out of it, as it's pretty much cache prefetching). It's been about a year since I realized the impact of a JIT-like query compiler for these kinds of join-project queries, but needing to balance IOPS, vectorization, and likely even applying (vectorized) B-tree tactics within a 4k page, on top of the weirdness from multi-temporal (not just bi-temporal) delta-based records (~change-data-capture stream; needs to be integrated/materialized to get a point-in-time view)... sounds like a recipe for logic bugs/off-by-one errors. They are already hard-to-impossible to notice if it'd be used in production, it being a code generator allows situations with only edge case queries having data-dependent edge case bugs, and the addition of dynamic/adaptive IO concurrency makes reproducing/debugging a detected error next to impossible. I wouldn't dare to trust the code generator I'd write, if not formally verified. Not because I don't have faith in my skills, but because it's extremely complex code that has to be fast and fall out of a JIT and it's nature makes off-by-one errors in index access unusually likely. And debugging a known error might well be harder than formally verifying to find the bug. [0]: https://news.ycombinator.com/item?id=25867693 https://news.ycombinator.com/item?id=25867693 https://news.ycombinator.com/item?id=27512224 https://news.ycombinator.com/item?id=27512224 TL;DR: There is code that would be useful if written, but is so complex and neigh-impossible to debug that formally verifying it might be easier than debugging it to "production-grade". I hope this project makes that kind of approach practical for those engineers who could write the code and make it pass integration tests.

mkl95 4y ago

Many engineers and teams are aware that they write bad code, and they love it. You can get very far as a clumsy code vendor. Even if formal verification was practical, it would be pretty difficult to make it mainstream.

deleted 4y ago

[deleted]

nottorp 4y ago

You can prove that an algorithm is correct most of the time (yes, halting and decidability but for practical purposes you mostly can). How do you prove an event driven application is correct?

Thiez 4y ago
Modelling your application as a state machine will allow you to use model checking to prove various properties about your model. Proving that your program is equivalent (for some chosen definition of equivalence) to the state machine is left as an exercise for the reader.
- nottorp 4y ago
  > Proving that your program is equivalent (for some chosen definition of equivalence) to the state machine is left as an exercise for the reader. "It's obvious" :)

IngoBlechschmid 4y ago

Try the proof assistant Agda without installation directly in your browser: https://agdapad.quasicoherent.io/ https://agdapad.quasicoherent.io/ Or Lean: https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_g...

ChrisMarshallNY 4y ago

While I laud the goals, I am skeptical of the ability to met them. I very much believe that there is an industry-wide crisis of terrible software, but I don't believe that it's practical to go directly from "garbage to gold." The path is long, and far from straight. Best Practices are how engineering disciplines, throughout history, have achieved progress in Quality. Currently, Best Practices aren't really a "thing," in software development, and it shows. People like Steve McConnell are not really respected, and a general culture of "move fast and break things" is still pervasive. Engineers flit around companies like mayflies, techniques and libraries come and go, and there's an enormous reliance on dependencies with very little vetting. We spend so much time, trying to perfect our tools, without trying to perfect ourselves. Academics and theorists have been proposing languages, libraries, infrastructure, and management practices that are designed to change lead into gold for decades, yet it never seems to happen. I have always been a fan of self-Discipline, and the apprenticeship model. That requires a lot of social infrastructure that does not currently exist. It's as old as human history, and absolutely proven to achieve results. "In theory, there is no difference between theory and practice; while in practice, there is." -Benjamin Brewster "It is not enough to do your best; you must know what to do, and THEN do your best." -W. Edwards Deming "The significant problems we face cannot be solved by the same level of thinking that created them." -Albert Einstein "Everyone thinks of changing the world, but not one thinks of changing himself." -Tolstoy https://xkcd.com/2030/ https://xkcd.com/2030/

zozbot234 4y ago
> While I laud the goals, I am skeptical of the ability to met them. Let's start with the easiest part, and rewrite everything in Rust (or a comparably safe language). We'll need something like this anyway to give our software a workable semantics that's free of UB (at least wrt. the "safe" checked subset). Then we can work on the harder problem of using proof to establish that the unchecked parts do not invoke UB, and that intended specifications are not violated even in the "safe" parts.
- formerly_proven 4y ago
  Tons of, if not most, "move fast and break things" software is written in safe languages, not C or C++.

Genbox 4y ago

Microsoft developed the excellent Code Contracts[1] project. From the user's perpective, tt was a simple class called Contracts with a few methods such as Require(), Ensure() and Invariant() Underneath the hood it used the Z3 Solver[2], which is both intuitive, flexible and fast. It validated the contracts while coding and highlighted in the Visual Studio IDE when a contract was broken. You could write something like: Contracts.Requires(x > 5 && y > x); Which would get translated to a compile time check as well. Unfortunately, Code Contracts has been dead for years now, and it was even removed entirely from .NET[3] due to being hard to maintain, and the verifier stopped working in newer versions of VS. Luckily, C# developers now have a small taste of contracts due to nullability analysis[4], but even more exciting is that contracts is making its way into C# as a first-level standard[5]. [1] https://www.microsoft.com/en-us/research/project/code-contracts/ https://www.microsoft.com/en-us/research/project/code-contra... [2] https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3 [3] https://github.com/dotnet/runtime/issues/20006 https://github.com/dotnet/runtime/issues/20006 [4] https://docs.microsoft.com/en-us/dotnet/csharp/nullable-references https://docs.microsoft.com/en-us/dotnet/csharp/nullable-refe... [5] https://github.com/dotnet/csharplang/issues/105 https://github.com/dotnet/csharplang/issues/105

pron 4y ago

Wow, the language here is even more optimisitc than the rosiest descriptions you see from young researchers, which prompted me to check if the author has had much experience deductively verifying interesting "deep" functional properties of non-trivial programs. The answer seems to be no. Like a newcomer to the field, he focuses on "first-day" problems such as language convenience, but the answer to his question of why this hasn't been done before is because that's not the hard problem, something he'll know once he obtains more experience. One of the biggest issues — indeed, the problem separation logic tries to address, but does so successfully only for relatively simple properties — is that "correctness" does not feasibly (affordably) compose. The difficulty of proving the correctness of a program made out of components, each of which has already been proven correct for any desired property is not easier than proving the correctness of the program from scratch, without concern for its decomposition. I.e. proving the correctness of a program made of ten provably-correct 500-line components is no easier than proving the correctness of all 5000 lines at once. This has been shown to be the case not only in the theoretical worst case, but also in practice. Here's an example to make things concrete. Suppose we have the following (Java) method, calling some unknown, pure, `bar` method: long foo(long x) { if (x <= 2 || (x & 1) != 0) return 0; for (long i = x; i > 0; i--) if (bar(i) && bar(x - i)) return i; throw new Error(); } It is very easy to describe exactly under what conditions an error would be thrown. Similarly, it is easy to describe the operation of the following method, and prove that it performs its function correctly: boolean bar(long x) { for (long i = x - 1; i >= 2; i--) for (long s = x; s >= 0; s -= i) if (s == 0) return false; return true; } However, it is not easy to determine which inputs, if any, would cause foo to throw an error using that particular bar. In fact, we only happen to know that this particular question is extremely hard because it is one that has interested mathematicians for 300 years and remains unanswered. While most verification tasks don't neatly correspond to well-known mathematical problems, and most require far less than 300 years to figure out, this kind of difficulty is encountered by anyone who tries to deductively verify non-trivial programs for anything but very specific properties (such as "there's no memory corruption", which separation logic does help with). Various kinds of non-determinism, such as the result of concurrency or any kind of interaction, only makes the possible compositions more complex. In short, the effort it takes to verify a program does not scale nicely with its size, even when it is neatly decomposed, and it is this practical affordability — which is not a result of the elegance of the tools used — that makes this subject so challenging (and interesting), and requires some humility and lowering of expectations even when it is useful (and it can be certainly useful when yielded properly and at the right scope). Another problem is an incorrect model of how programs are constructed. One might think that if a programmer has written a program, then they must have some informal (but deductive) model of it in their mind, and all that's missing is "just" formally specifying it. But that is not how programs are constructed over time when many people are involved. In practice, programmers often depend on inductive properties in their assumptions, such as "if the software survived for many years, then local changes are unlikely to have global effects that aren't caught by existing tests." Those assumptions are good enough for providing the (often sufficient) level of correctness we already reach, but insufficient for constructing software that can be formally specified, let alone deductively proven correct. That is why much of the contemporary research focuses on less sound approaches, that aren't fully deductive, such as concolic testing (e.g. Klee), that allow better scaling for both specification and verification at the cost of "perfection". The reason why both research and industry don't all do what is proposed here is because they know that's not where to real problems are. There are bigger issues to tackle before making the languages more beginner-friendly.

dgb23 4y ago

I recently came across Ur/web. It makes some promises that are quite attractive. One of the benefits of having a DSL rather than something general purpose is that it can make these promises in a more comprehensive and focused manner. But despite being around for a while now it didn’t get adopted very widely.

deleted 4y ago

[deleted]