42

I recommend reading Pollack's How to believe a machine-checked proof. It explains how proof assistants are designed to minimize the amount of critical code. There are many levels of formal verification (that's the phrase you're looking for in place of "proven") of a proof assistant: Verify that the algorithms used by the proof assistant are correct. Verify ...


36

I'll try to give a succinct answer to some of your questions. Please bear in mind that this is not strictly my field of research, so some of my info may be outdated/incorrect. There are many tools that are specifically designed to formally prove properties of Java and C++. However I need to make a small digression here: what does it mean to prove ...


30

First off, you're absolutely right: you're on to a real concern. Formal verification transfers the problem of confidence in program correctness to the problem of confidence in specification correctness, so it is not a silver bullet. There are several reasons why this process can still be useful, though. Specifications are often simpler than the code ...


19

D.W.'s answer is great, but I'd like to expand on one point. A specification is not just a reference against which the code is verified. One of the reasons to have a formal specification is to validate it by proving some fundamental properties. Of course, the specification cannot be completely validated — the validation would be as complex as the ...


15

I would like to mention three remarkable applications of formal methods/formal verification tools in industry or non-trivial real systems. Note that I have little experience on this topic and I only learn them from reading papers. The open-source tool Java Pathfinder (JPF for short) released by NASA in 2005 is a system to verify executable Java bytecode ...


11

I am not in a position to tell how much more research should be done on the topic, but I can tell you that there is research being done, for example the Verisoft XT program funded by the german government. The concepts which I think you are looking for are called formal verification and contract based programming, where the latter is a programmer-friendly ...


10

Ignoring exceptions is unsound. Example: let g = { raise E; } let f = { x := interesting_stuff(); g(); x := 0; } When analyzing f, you need to take into account the fact that g raises an exception, otherwise you would incorrectly conclude that x is always 0 on return from f. I don't know that there is a “standard” technique for dealing ...


10

What you need is the idea of "the trusted core". Quoting "A verified runtime for a verified theorem prover": In many theorem provers, the trusted core—the code that must be right to ensure faithfulness—is quite small. As examples, HOL Light is an LCF-style system whose trusted core is 400 lines of Objective Caml, and Milawa is a Boyer-Moore style prover ...


7

Dataflow analysis works on sets of facts. GEN points are points in the graph where one of the facts you care about becomes true, and KILL points are points in the graph where one of the facts you care about becomes false. The GEN and KILL points thus depend on the facts you care about. For example: if you were doing a constant propagation analysis you ...


7

Disclaimer: I'm not sure how useful any of this is for getting this done practically since you have a program, not a Turing Machine. The Cook-Levin Theorem essentially states that you can translate the execution of a Turing Machine into a boolean formula that is polynomial in the length of the TM's execution such that the formula is satisfiable iff the TM ...


6

To answer your question in the most concise way - yes, this bug could have potentially been caught by formal verification tools. Indeed, the property "never send a block which is bigger than the size of the hearbeat that was sent" is fairly simple to formalize in most specification languages (e.g. LTL). The problem (which is a common criticism against ...


6

You can start with Software Foundations by Benjamin C. Pierce et al. Topics include basic concepts of logic, computer-assisted theorem proving, the Coq proof assistant, functional programming, operational semantics, Hoare logic, and static type systems. The exposition is intended for a broad range of readers, from advanced undergraduates to PhD students ...


6

$x:A$ is a statement about objects in the formal system, like, for example, $\vdash 2+4:\texttt{int}$, whereas $x\Xi A$ is an expression in the formal system, like $\texttt{if}~ 2 + 4 ~\texttt{==}~5 ~\texttt{then}~ e_1~ \texttt{else} ~e_2$.


6

Look into tools like Frama-C, SPARK, Astrée, etc... They have their use in very specific cases, notably software verification of small to medium sized embedded safety critical software (e.g. inside aircrafts, per DO-178C, or nuclear power plants, etc...). Such software have a few dozen thousands lines (or perhaps two hundred thousands at most of C or Ada ...


6

I am not very sure what you are asking, and I am also not sure that you have the background to understand CompCert. It seems that you are still confused by some basic concepts in Coq. I would suggest you start with Software Foundations. Most of your questions would be answered there. But, basically: Definition and Fixpoint are like OCaml's let and let rec,...


6

While this may trend close to self-advertisement, this is essentially the topic of my recent paper Metamath Zero: The Cartesian Theorem Prover (video), and the analogy with bootstrapping compilers is spot on. The introduction of the paper lays out what is needed to make this happen, and it's only a problem of engineering. As Andrej says, there are several ...


5

Symbolic model checking can be very useful for verifying the correctness of communications and security protocols. For example: A symbolic model of an OAUTH2 implementation could help check for unintended consequences where an adversary obtains secret authentication tokens or related circumstantial data that could help them contravene the process. A ...


5

Partial correctness does not mean that not all statements of a specification are met by an algorithm. Have a look at the Wikipedia article about correctness: Partial correctness of an algorithm means that it returns the correct answer if it terminates. Total correctness means that is it additionally guaranteed that the algorithm terminates. Such a proof ...


5

Commercial program checkers like Klocwork or Coverity might have been able to find Heartbleed since it is a relatively simple "forgot to do a bounds check error," which is one of the main problems they are designed to check for. But there is a much simpler way: use opaque abstract data types that are well tested to be free from buffer overrun. There are a ...


5

You have an intended postcondition for a loop, and you're looking for an interesting invariant. In this scenario, try taking the intended postcondition, and replacing the total number of iterations (here N) by the number of iterations so far (here i). There's no guarantee that this is an invariant: that's only the case if the way the postcondition is somehow ...


5

One of the de facto methods for proving results in functional programming is via Richard Bird's group. In particular, you ask for an in-depth or at least more comprehensive approach to equational reasoning and list induction and this is provided in Lectures on Constructive Functional Programming. More generally, the text "Algebra of Programming", by Bird ...


5

It turns out that an excellent source of proof techniques and examples for proving things about pure functional languages is proof assistants which usually include as part of their specification language a pure functional language on which it is possible to reason equationally. One might want to consult a book like Certified Programing with Dependent Types ...


5

The SoftwareEngineering.SE link gives the wrong answer for the right reasons. You can only ever prove anything with respect to a formal model. Verifying that that formal model accurately captures reality (or at least accurately captures the parts you care about for your purposes) is an informal process. In many applications of formal methods, one of the most ...


5

Quite a lot of things can and have been formally verified with formal methods. Compilers. We want to prove that a compiler preserves the semantics of its source program. For example, if we write a int x = 3; x++; in C, we mean that. But the compiler might not produce correct assembly and machine code. It is known to be difficult to debug compilers, so a ...


5

I think Turing's method is probably fine, but you are mistaken about why exactly the code you wrote, "terminates." First, note that this is not really (written as) a function at all. It is a self-referential value. And the reason the program terminates even though it's defined in it is that the program does not attempt to evaluate it fully. In this case, ...


4

A formal specification of a program is (more or less) a program written in another programming language. As a result, the specification will certainly include its own bugs. The advantage of formal verification is that, as the program and the specification are two separate implementations, their bugs will be different. But not always: one common source of ...


4

Using a tighter language doesn't just move goal posts around from getting implementation correct to getting the spec right. It is hard to make something that is very wrong yet consistent logically; which is why compilers catch so many bugs. Pointer Arithmetic as it is normally formulated is unsound because the type system doesn't actually mean what it is ...


4

If you count as a " program verification technique " the combination of runtime bound-checking and fuzzing, yes this particular bug could have been caught. Proper fuzzing will cause the now infamous memcpy(bp, pl, payload); to read across the limit of the memory block pl belongs to. Runtime bound-checking can in principle catch any such access, ...


4

In a nutshell: Partial correctness is an issue of termination, not ot correctness of what is computed. A function is partially correct with respect to a specification iff whatever it computes is correct, when it terminates. This idea can be extended to the computation of incomplete (partial) answers. Whatever is computed of the answer is correct, but the ...


4

Symbolic Model Checking is Model Checking that works on symbolic states. That is, they encode the states into symbolic representations, typically Ordered Binary Decision Diagrams (OBDDs). The question is what do they do and how do they work. You first have your source code for some application. You then transform your source code into some state-transition ...


Only top voted, non community-wiki answers of a minimum length are eligible