Why3: trace but effects

Real world example. I was asked: will the application make some insecure call if some special setting was set in the configuration file? I was sure, it won't. I thought the application followed this policy and that this setting allowed you to prevent the execution of unsafe code. I was wrong. How to check it?

Why3 has not effects system. But they can be modeled - with a ghost effect log. The idea is simple: effectful (or insecure, or the ones that interest you) functions will "log" when they are called. In some special "ghost log", then we can check the log - if it was changed then they were called. It's called "ghost" bcs it is not planned to exist in the real code (for example after extraction of C, Ocaml, etc from the model). The log can be very simple record with mutable fields: one per a function:

type trace = { mutable f1_calls: int }

Here we trace/log only one function: f1. I made it integer, bcs I wanted to be able to check the fact of call many times: it any particular function (so, it is not just bool).

The whole code is:

 1   module Call1
 2     use int.Int
 3   
 4     type trace = { mutable f1_calls: int }
 5   
 6     let ghost trace : trace = { f1_calls = 0 }
 7   
 8     predicate f1_was_called (before after: int) = after = before + 1
 9     predicate f1_was_not_called (before after: int) = after = before  
10   
11     let ghost f1 () : unit
12       writes { trace.f1_calls }
13       ensures { f1_was_called (old trace.f1_calls) trace.f1_calls }
14     =
15       trace.f1_calls <- trace.f1_calls + 1
16   
17     let f2 (a1: int) : int
18       ensures { a1 = 0 -> f1_was_not_called (old trace.f1_calls) trace.f1_calls }
19       ensures { a1 <> 0 -> f1_was_called (old trace.f1_calls) trace.f1_calls }
20     =
21       if a1 = 0 then 100
22       else begin
23         f1 ();
24         101
25       end
26   
27     let main () : unit
28       requires { trace.f1_calls = 0 }
29       ensures { trace.f1_calls > 0 }
30     =
31       let _ = f2 2 in
32       ()
33   
34   end

I added 2 predicates: f1_was_called and f1_was_not_called. They check the ghost and mutable counter in the ghost trace (log).

The idea of this simple example is to demonstrate that you can check the fact that some interesting function f1 was (or was not) called. See at main: we check exactly this with its ensures {..}, we just need to provide some help to Why3, for example, that the initial value of the counter was 0.

We simulate nested function calls with additional function f2. So, ensures {..} on 29 line tells - "the main has f1 effect". You can check the opposite as well (that it has not f1 effect):

 let main () : unit
   requires { trace.f1_calls = 0 }
   ensures { trace.f1_calls = 0 }
 =
   let _ = f2 0 in
   ()

Why did we need ensures {..} postconditions on f2 for example? IT does not look as a black box, yes?

Why3 verification is modular.

When proving a caller of f2, Why3 uses the contract of f2, not its implementation!

So if we have:

let main () : unit
  requires { trace.f1_calls = 0 }
  ensures {
    f1_was_called (old trace.f1_calls) trace.f1_calls
  }
=
  let _ = f2 1 in
  ()

and f2 has no relevant postcondition, Why3 has no reason to believe that calling f2 1 changes the counter!

Even though it can see the implementation while verifying f2 itself, that implementation is not automatically propagated into callers.

To reason about f2, Why3 needs its contract, call it "a passport" - what is it? What does it do? Well... f2 can be... a BLACK BOX! It can be "abstract", to be only a contract! We introduce such a function not with let ... but with val ...! And it has not a body.

See:

 1   module Call1
 2     use int.Int
 3   
 4     type trace = { mutable f1_calls: int }
 5   
 6     let ghost trace : trace = { f1_calls = 0 }
 7   
 8     predicate f1_was_called (before after: int) = after = before + 1
 9     predicate f1_was_not_called (before after: int) = after = before  
10   
11     let ghost f1 () : unit
12       writes { trace.f1_calls }
13       ensures { f1_was_called (old trace.f1_calls) trace.f1_calls }
14     =
15       trace.f1_calls <- trace.f1_calls + 1
16   
17     val f2 (a1: int) : int
18       writes { trace.f1_calls }
19       ensures { result = if a1 = 0 then 100 else 101 }
20       ensures { a1 = 0 -> f1_was_not_called (old trace.f1_calls) trace.f1_calls }
21       ensures { a1 <> 0 -> f1_was_called (old trace.f1_calls) trace.f1_calls }
22   
23     let main () : unit
24       requires { trace.f1_calls = 0 }
25       ensures { trace.f1_calls = 0 }
26     =
27       let _ = f2 0 in
28       ()
29   
30   end

Look at f2 now: it specifies when f1 effect happens. Also it specifies (and it's important to avoid a warning that trace actually is not changed) that f2 MAY CHANGE trace.f1_calls.

OK. Now lets return to the original task: main embodies such a function that should be verified about an effect, but we can do it with f2 too:

 1   let f2 (a1: int) : int
 2     writes { trace.f1_calls }
 3     ensures { result = if a1 = 0 then 100 else 101 }
 4     ensures { a1 = 0 -> f1_was_not_called (old trace.f1_calls) trace.f1_calls }
 5     ensures { a1 <> 0 -> f1_was_called (old trace.f1_calls) trace.f1_calls }
 6   = if a1 = 0 then begin
 7      f1 ();        (* DENIES THE CONTRACT ! *)
 8      100
 9     end
10     else begin
11       f1 ();
12       101
13     end

And this demonstrate the original task ideally! Look - we are sure that:

• if the setting (a1) is 0 then f1 effect will not happen
• else f1 effect will happen

this is our expectation. This is what we think about the function f2.

The result of our proving :

$ why3 prove Call1.mlw -P z3 
File Call1.mlw:
Goal f1'vc.
Prover result is: Valid (0.01s, 38 steps).

File Call1.mlw:
Goal f2'vc.
Prover result is: Unknown (sat) (0.00s, 258 steps).

File Call1.mlw:
Goal main'vc.
Prover result is: Valid (0.00s, 40 steps).

and it happens bcs the body modeled the behavior of some real existing function denies its contract - our expectation about the behavior of f2: when the setting a1 is 0 which means "don't call the insecure function f1", the body actually calls it.

We modeled our task as:

• a1 is our setting from the configuration file
• f1 is our insecure function
• trace is ghost and it is used only for verification
• verified functions can be represented abstractly

If we mean "one or more calls" (to check that f1 effect happened somewhere in the depth of nested calls), then the predicate could be:

predicate f1_was_called (before after: int) = after > before

Similar technique is used in many other Proof Assistants.