seacomb 0.1.0

A formally verified seccomp compiler.
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
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114

//! The 32-bit words a filter compares, and the `seccomp_data` image they come from.

use vstd::prelude::*;
#[allow(unused_imports)]
use crate::spec::{policy::*, cbpf::*};
#[allow(unused_imports)]
use super::builder::Builder;

verus! {

impl Policy {
    /// Byte offset of `seccomp_data.nr`.
    pub(super) const OFFSET_EVENT_NR: u32 = 0;

    /// Byte offset of `seccomp_data.arch`.
    pub(super) const OFFSET_EVENT_ARCH: u32 = 4;

    /// Byte offset of the low half of `seccomp_data.args[0]`.
    pub(super) const OFFSET_EVENT_ARGS: u32 = 16;
}

impl Event {
    /// The event the 64-byte image `data` describes.
    pub(super) open spec fn of(data: &[u8]) -> Event {
        Event::parse(data)->Some_0
    }

    /// The filter's loads read back the fields of a successfully parsed event.
    pub(super) proof fn lemma_image(data: &[u8])
        requires Event::parse(data) is Some
        ensures
            Self::of(data).args.len() == Rule::ARG_COUNT_MAX,
            Builder::word(data, Policy::OFFSET_EVENT_NR) == Self::of(data).nr as u32,
            Builder::word(data, Policy::OFFSET_EVENT_ARCH) == Self::of(data).arch,
            forall |k: u32| k < Rule::ARG_COUNT_MAX ==>
                #[trigger] Builder::word(data, (Policy::OFFSET_EVENT_ARGS + 8 * k) as u32)
                    == (Self::of(data).args[k as int] & 0xFFFF_FFFF) as u32,
            forall |k: u32| k < Rule::ARG_COUNT_MAX ==>
                #[trigger] Builder::word(data, (Policy::OFFSET_EVENT_ARGS + 8 * k + 4) as u32)
                    == (Self::of(data).args[k as int] >> 32) as u32,
    {
        let ev = Self::of(data);
        // `nr` is the word at offset 0, put through the `i32` round trip `parse` writes.
        let w = Builder::word(data, Policy::OFFSET_EVENT_NR);
        assert((w as i32) as u32 == w) by (bit_vector);
        // Each argument spans two words: the low one at `16 + 8 * k`, the high one four on.
        assert forall |k: u32|
            #![trigger Builder::word(data, (Policy::OFFSET_EVENT_ARGS + 8 * k) as u32)]
            #![trigger Builder::word(data, (Policy::OFFSET_EVENT_ARGS + 8 * k + 4) as u32)]
            k < Rule::ARG_COUNT_MAX implies
            Builder::word(data, (Policy::OFFSET_EVENT_ARGS + 8 * k) as u32)
                == (ev.args[k as int] & 0xFFFF_FFFF) as u32
            && Builder::word(data, (Policy::OFFSET_EVENT_ARGS + 8 * k + 4) as u32)
                == (ev.args[k as int] >> 32) as u32
        by {
            let i = Policy::OFFSET_EVENT_ARGS + 8 * (k as int);
            let c0 = data@[i];
            let c1 = data@[i + 1];
            let c2 = data@[i + 2];
            let c3 = data@[i + 3];
            let c4 = data@[i + 4];
            let c5 = data@[i + 5];
            let c6 = data@[i + 6];
            let c7 = data@[i + 7];
            assert((((c0 as u64) | ((c1 as u64) << 8) | ((c2 as u64) << 16) | ((c3 as u64) << 24)
                | ((c4 as u64) << 32) | ((c5 as u64) << 40) | ((c6 as u64) << 48)
                | ((c7 as u64) << 56)) & 0xFFFF_FFFF) as u32
                == (c0 as u32) | ((c1 as u32) << 8) | ((c2 as u32) << 16) | ((c3 as u32) << 24))
                by (bit_vector);
            assert((((c0 as u64) | ((c1 as u64) << 8) | ((c2 as u64) << 16) | ((c3 as u64) << 24)
                | ((c4 as u64) << 32) | ((c5 as u64) << 40) | ((c6 as u64) << 48)
                | ((c7 as u64) << 56)) >> 32) as u32
                == (c4 as u32) | ((c5 as u32) << 8) | ((c6 as u32) << 16) | ((c7 as u32) << 24))
                by (bit_vector);
        }
    }

    /// Unsigned filter comparisons preserve syscall-number equality.
    pub(super) proof fn lemma_nr(self)
        ensures
            forall |nr: i32| #[trigger] (nr as u32) == self.nr as u32 ==> nr == self.nr,
    {
        let m = self.nr;
        assert forall |nr: i32| #[trigger] (nr as u32) == m as u32 implies nr == m by {
            assert((nr as u32) == (m as u32) ==> nr == m) by (bit_vector);
        }
    }
}

impl ArgCmp {
    /// A 64-bit value seen as two 32-bit words: comparisons settle on the high word
    /// unless the two are equal, and a mask applies to each word on its own.
    pub(super) proof fn lemma_words(x: u64, y: u64)
        ensures
            x & u64::MAX == x,
            x & 0xFFFF_FFFF == (x as u32) as u64,
            (x == y) <==> (((x >> 32) as u32) == ((y >> 32) as u32) && (x as u32) == (y as u32)),
            (x < y) <==> (((x >> 32) as u32) < ((y >> 32) as u32)
                || (((x >> 32) as u32) == ((y >> 32) as u32) && (x as u32) < (y as u32))),
            ((x & y) as u32) == ((x as u32) & (y as u32)),
            (((x & y) >> 32) as u32) == (((x >> 32) as u32) & ((y >> 32) as u32)),
    {
        assert(x & u64::MAX == x) by (bit_vector);
        assert(x & 0xFFFF_FFFF == (x as u32) as u64) by (bit_vector);
        assert(((x & y) as u32) == ((x as u32) & (y as u32))) by (bit_vector);
        assert((((x & y) >> 32) as u32) == (((x >> 32) as u32) & ((y >> 32) as u32))) by (bit_vector);
        assert((x == y) <==> (((x >> 32) as u32) == ((y >> 32) as u32) && (x as u32) == (y as u32)))
            by (bit_vector);
        assert((x < y) <==> (((x >> 32) as u32) < ((y >> 32) as u32)
            || (((x >> 32) as u32) == ((y >> 32) as u32) && (x as u32) < (y as u32)))) by (bit_vector);
    }
}

} // verus!