seacomb 0.3.2

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

//! The syscall numbers and multiplexer arguments a filter compares against.

use vstd::prelude::*;
use crate::spec::policy::*;
use crate::spec::syscall::*;

verus! {

impl Syscall {
    /// Executable version of [`Syscall::to_socketcall_arg`].
    pub(crate) fn socketcall_arg(&self) -> (res: Option<u64>)
        ensures res == self.to_socketcall_arg()
    {
        match self {
            Syscall::Socket       => Some(1),
            Syscall::Bind         => Some(2),
            Syscall::Connect      => Some(3),
            Syscall::Listen       => Some(4),
            Syscall::Accept       => Some(5),
            Syscall::Getsockname  => Some(6),
            Syscall::Getpeername  => Some(7),
            Syscall::Socketpair   => Some(8),
            Syscall::Send         => Some(9),
            Syscall::Recv         => Some(10),
            Syscall::Sendto       => Some(11),
            Syscall::Recvfrom     => Some(12),
            Syscall::Shutdown     => Some(13),
            Syscall::Setsockopt   => Some(14),
            Syscall::Getsockopt   => Some(15),
            Syscall::Sendmsg      => Some(16),
            Syscall::Recvmsg      => Some(17),
            Syscall::Accept4      => Some(18),
            Syscall::Recvmmsg     => Some(19),
            Syscall::Sendmmsg     => Some(20),
            _ => None,
        }
    }

    /// Executable version of [`Syscall::to_ipc_arg`].
    pub(crate) fn ipc_arg(&self) -> (res: Option<u64>)
        ensures res == self.to_ipc_arg()
    {
        match self {
            Syscall::Semop        => Some(1),
            Syscall::Semget       => Some(2),
            Syscall::Semctl       => Some(3),
            Syscall::Semtimedop   => Some(4),
            Syscall::Msgsnd       => Some(11),
            Syscall::Msgrcv       => Some(12),
            Syscall::Msgget       => Some(13),
            Syscall::Msgctl       => Some(14),
            Syscall::Shmat        => Some(21),
            Syscall::Shmdt        => Some(22),
            Syscall::Shmget       => Some(23),
            Syscall::Shmctl       => Some(24),
            _ => None,
        }
    }
}

impl Syscall {
    /// The syscall number at which `arch` reaches this syscall, as the filter's
    /// unsigned comparisons see it, if it reaches it at all.
    pub(super) open spec fn spec_bpf_nr(&self, arch: Arch) -> Option<u32> {
        match self.spec_nr(arch) {
            Some(nr) => Some(nr as u32),
            None => None,
        }
    }

    /// Executable version of [`Syscall::spec_bpf_nr`].
    #[verifier::when_used_as_spec(spec_bpf_nr)]
    pub(super) fn bpf_nr(&self, arch: Arch) -> (res: Option<u32>)
        ensures res == self.spec_bpf_nr(arch)
    {
        self.nr(arch).map(|nr: i32| -> (res: u32)
            ensures res == nr as u32
        { nr as u32 })
    }
}

} // verus!