sudo-rs 0.1.0-dev.20230620

A memory safe implementation of sudo and su.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74

(* Why3 specification file for selected code in the sudoers crate.
   All proof goals generated by Why3 1.5.1 can be discharged using CVC4 1.8 *)

module Sudoers

use array.Array
use option.Option
use ref.Ref
use int.Int

(* loose models for the types in sudoers::Ast *)
type metavar 'a = All | Only 'a
type qualified 'tag 'a = Yes 'a 'tag | No 'a
type spec 'tag 'a = (qualified 'tag (metavar 'a))

predicate contains (pred: 'a -> bool) (a: array 'a)
  = exists i. 0 <= i < length a /\ pred a[i]

function who (item: spec 'tag 'a): metavar 'a
  = match item with
    | Yes x _ -> x
    | No x -> x
    end

function condition (item: spec 'tag 'a): option 'tag
  = match item with
    | Yes _ tag -> Some tag
    | No _ -> None
    end

function matched_by (pred: 'a -> bool) (item: spec 'tag 'a): bool
  = match who item with
    | All -> true
    | Only x -> pred x
    end

predicate final_match (pred: 'a -> bool) (a: array 'a) (f: 'a -> 'b) (x: 'b)
  = exists i. 0 <= i < length a /\ pred a[i] /\ f a[i] = x /\ forall k. i < k < length a -> not pred a[k]

(* Why3 model of the sudoers::find_item function *)
let find_item (items: array (spec 'tag 'a)) (pred: 'a -> bool): option 'tag
    returns {
      | Some tag -> final_match (matched_by pred) items condition (Some tag)
      | None     -> not contains (matched_by pred) items \/ final_match (matched_by pred) items condition None
    }

= let result = ref None in

  for i = 0 to items.length - 1 do
    invariant { forall tag. !result = Some tag <->
                  exists j.  0 <= j < i /\ matched_by pred items[j] /\ Some tag = condition items[j] /\
                  forall k. j < k < i -> not matched_by pred items[k] }
    let (qualifiedment, who) = match items[i] with
      | No x -> (None, x)
      | Yes x tag -> (Some tag, x)
    end in
    match who with
      | All -> result := qualifiedment
      | Only id -> if pred id then result := qualifiedment;
    end;
  done;

  (* perform a "virtual loop" to strength the case !result = None;
     this could also be solved by adding a ghost variable above *)
  ghost if is_none !result && contains (matched_by pred) items then
    for i = items.length - 1 downto 0 do
      invariant { forall k. i < k < items.length -> not matched_by pred items[k] }
      invariant { exists k. 0 <= k <= i /\ matched_by pred items[k] }
      if matched_by pred items[i] then break
    done;

  !result;

end