Hacker News Reader

Comment by lawfulcactus | Hacker News Reader

So, I think what you're missing here is that the 'verification' is a formal specification about the behavior of the kernel, along with a set of proofs about that specification. This is vastly simplified (there are multiple levels of specification, last I checked), but that's the general idea. It's possible to have your compiler automatically derive the specification from your code (and, indeed, the seL4 people have written a Rust-like language called Cogent that does this), but formal verification inherently involves an understanding of what your code is /intended/ to do, and proving that it /does/. The compiler only has information about what it /does/, so it can only generate a specification that describes this. Information about your high-level intentions for the code has to be concretized somewhere, while ensuring that the spec conforms to it-- that's the job of the proof engineers.

View on HN

How does this formal specification look like?

From my naive standpoint: input, output, side-effect, time

  [no_sideffect, 1ms]
  fn increment(int i) -> int:
      return i + 1

What this is missing is a formal statement that says "increases the value of the input by one" -> except you accept the function body as formal statement.

Thanks for all the answers here, I guess I'm going to look for some more reading material.

Here's a specification of an increment function in Isabelle/HOL, the theorem prover used for SeL4, plus some other random lemmas about it:

    theory Scratch
      imports Main
    begin

    fun increment :: "int ⇒ int" where 
    "increment x = x + 1"

    lemma increment_increments:
      shows "increment x = x + 1"
      by simp

    lemma double_increment_adds_two:
      shows "increment (increment x) = x + 2"
      by simp

    lemma increment_sub_1_is_x:
      shows "increment x - 1 = x"
      by simp

If you take the original code as the formal statement, how could it ever be wrong?

To add to logicchains' answer:

Normally, you wouldn't take the function body as a formal statement, and would have a separate formal specification instead. In the example of increment, the formal specification is no simpler and no more useful than the implementation itself, but this is usually not the case.

Imagine e.g. that the following specification describes the desired behavior of a function f:

    f(x) <= √x  and  (f(x) + 1) > √x

The OS developer would write something the code below to implement this specification.

  int f(int x) {
    int r1 = 0;
    int r2 = 1;
    while (x >= r2) {
      r1++;
      r2 = r2 + r1 + r1 + 1;
    }
    return r1;
  }

Does this C implementation conform to the specification? It's not all that easy to tell. But if the program is actually correct, then Floyd-Hoare logic [1] allows you to go through the program line-by-line and produce a proof that for any integer i and variable x', the following holds:

  lemma f_implements_spec: "
    { valueOf(x') = i \<and> i > 0 }
    x' = f(x')
    { valueOf(x') <= \<sqrt>(i) \<and> valueOf(x') - 1 > \<sqrt>(i) }"

meaning that if the statement x'=f(x') is ever executed in an environment where x' has an integer value i > 0, then after this line is executed, the result stored in x' will satisfy the specification above.

[1] https://en.wikipedia.org/wiki/Hoare_logic

Reply on news.ycombinator.com