Personnes présentes

• Frédéric Boulanger
• Chantal Keller
• Hai Nguyen Van
• Safouan Taha
• Vassil Todorov
• Benoit Valiron
• Burkhart Wolff
• Lina Ye

Verifying C Programs with Isabelle/Simpl/AutoCorres

Burkhart presents how to verify a C program in Isabelle/Simpl/AutoCorres. Burkhart presents his solution to an exercise that Timothy Bourke gave at the ENS (course page, seL4 lecture, exercise).

AutoCorres is a tool that attempts to simplify the formal verification of C programs in Isabelle/HOL. AutoCorres relies on SIMPL framework to produce an automatically abstracted ”monadic” specification hiding the memory model and other hardware implementation aspects. This way the proofs are easier to handle.

Exercise

Consider the following C code computing primeness:

unsigned int is_prime(unsigned int n)
{
    /* Les nombres plus petits que 2 ne sont pas premiers. */
    if (n < 2)
        return 0;

    /* Trouver le premier non insignifiant facteur de 'n'. */
    unsigned int i = 2;
    while (n % i != 0) {
        i++;
    }

    /* Si le premier facteur est 'n' lui-meme, 'n' est premier. */
    return (i == n);
}

Using the install-C-file command in Isabelle we obtain the following SIMPL representation:

TRY
   IF ´n < scast 2 THEN 
        creturn global_exn_var_'_update ret__unsigned_'_update (λs. scast 0)
   FI;;
   ´i :== scast 2;;
   Guard Div_0 ⦃´i ≠ 0⦄ (WHILE ´n mod ´i ≠ scast 0 DO
                            ´i :== ´i + scast 1;;
                             Guard Div_0 ⦃´i ≠ 0⦄ SKIP
                          OD);;
   creturn global_exn_var_'_update ret__unsigned_'_update (λs. scast (if i_' s = n_' s then 1 else 0));;
   Guard DontReach {} SKIP
CATCH SKIP
END

Under SIMPL form, the functional aspect of the code is polluted by the constructs handling the memory model (casts) and exceptions (Guards, try/catches). After running Autocorres we obtain a much clean form:

?n ≡    condition (λs. ?n < 2)
        (return 0)
        (do i ← whileLoop (λi s. 0 < ?n mod i)
                 (λi. do guard (λ:001. Suc i ≤ UINT_MAX);
                          return (Suc i)
                       od)
                2;
          return (if i = ?n then 1 else 0)
        od)

In this abstracted form, we can see that AutoCorres has abstracted/simplified/removed many of the C-specific constructs to focus on the functional aspect. We can now apply a Weakest-Precondition verification using the "wp" tactic after annotating the loop with the adequate invariant:

lemma is_prime_correct:
  "⦃λs. n ≤ UINT_MAX ⦄ is_prime' n ⦃λr s. r = (if prime n then 1 else 0) ⦄!"
  (* Move the precondition into the assumptions. *)
  apply (rule validNF_assume_pre)
  (* Unfold the program body. *)
  apply (unfold is_prime'_def)

  (* Annotate the loop with an invariant and measure. *)
  apply (subst whileLoop_add_inv [
               where I="λr s. is_prime_inv r n"
               and M="(λ(r, s). Suc n - r)"])

  (*
   * Run "wp" to generate verification conditions.
   *)
proof (wp, intro conjI, elim conjE,simp_all)
  (* 1. The loop body obeys the invariant; *)
  fix s r 
  assume "n ≤ UINT_MAX"  and "is_prime_inv r n" and "0 < n mod r"  
  then show "is_prime_inv (Suc r) n"
       using is_prime_body_obeys_inv by auto
next
  (* 2. The loop body causes the measure to decrease; *)
  fix r fix sa sb::lifted_globals
    assume "n ≤ UINT_MAX" and "is_prime_inv r n ∧ 0 < n mod r ∧ sb = sa"
  then show "n - r < Suc n - r"
       by (simp add: Suc_diff_le tp06a.is_prime_inv_def)
next
  (* The loop counter never exceeds UINT_MAX. *) 
  fix r fix sa sb::lifted_globals  (* very ugly that this pops up ... *)
    assume "n ≤ UINT_MAX" and "is_prime_inv r n ∧ 0 < n mod r ∧ sb = sa"
  then show "Suc r ≤ UINT_MAX"
       by (metis Suc_eq_plus1 dual_order.trans gr_implies_not0 is_prime_body_obeys_inv 
                 tp06a.is_prime_inv_def)
next
  fix r 
    assume "n ≤ UINT_MAX" and "is_prime_inv r n" and "n mod r = 0"
  then show " (r = n ⟶ prime n) ∧ (r ≠ n ⟶ ¬ prime n)"   
       by (simp add: tp06a.is_prime_inv_implies_postcondition)
next
  (* The invariant implies the post-condition of the function. *) 
  assume " n ≤ UINT_MAX"
  then show " (n < 2 ⟶ ¬ prime n) ∧ (¬ n < 2 ⟶ is_prime_inv 2 n)"
    by (metis le_antisym nat_le_linear nat_less_le prime_ge_2_nat 
              tp06a.is_prime_precond_implies_inv)
qed  

At the end of the talk, Burkhart gave a link to L3 that is a language for specifying instruction set architectures where ARM, MIPS and x86 are already modeled.

Previous meeting -- Next meeting