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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
//! Abstract syntax and semantics of the libseccomp policy language.
use vstd::prelude::*;
use super::syscall::*;
// Syntax
verus! {
/// Architecture tokens `SCMP_ARCH_*` (excluding `SCMP_ARCH_NATIVE`).
#[derive(Debug, Clone, Copy, PartialEq, Eq, Structural)]
pub enum Arch { X86, X86_64, Arm, Aarch64 }
/// Filter actions (`SCMP_ACT_*`).
#[derive(Debug, Clone, Copy, PartialEq, Eq, Structural)]
pub enum Action {
KillProcess,
KillThread,
Trap(u16),
Errno(u16),
Trace(u16),
Log,
Allow,
Notify,
}
/// Comparison operators `scmp_compare`.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Structural)]
pub enum Compare { Ne, Lt, Le, Eq, Ge, Gt, MaskedEq }
/// One argument test `scmp_arg_cmp`.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Structural)]
pub struct ArgCmp {
pub arg: u32,
pub op: Compare,
pub a: u64,
/// For MaskedEq only: `a` is the mask, `b` the value.
pub b: u64,
}
/// One policy rule
#[derive(Debug, Clone, PartialEq, Eq)]
// Verus does not yet model non-Copy Clone derives.
#[verifier::external_derive(Clone)]
pub struct Rule {
pub action: Action,
pub syscall: Syscall,
pub conds: Vec<ArgCmp>,
/// Prevents multiplexing syscalls. For example, a rule for `bind`
/// should not match `socketcall(2, ...)`.
pub no_mux: bool,
}
/// A set of rules with default actions for no-match and bad-arch cases.
#[derive(Debug, Clone, PartialEq, Eq)]
// Verus does not yet model non-Copy Clone derives.
#[verifier::external_derive(Clone)]
pub struct Policy {
pub archs: Vec<Arch>,
pub rules: Vec<Rule>,
/// Default action when the arch is supported but no rule matches.
pub act_no_match: Action,
/// Default action when the arch is not supported.
pub act_bad_arch: Action,
}
impl Action {
/// Largest errno Linux returns for `SECCOMP_RET_ERRNO` (`include/linux/err.h`).
pub const MAX_ERRNO: u32 = 4095;
/// Whether the action's payload can be returned without kernel clamping.
pub open spec fn wf(self) -> bool {
match self {
Action::Errno(e) => (e as u32) <= Self::MAX_ERRNO,
_ => true,
}
}
/// Higher-precedence actions override lower ones.
/// This behavior is similar to when we install multiple filters:
/// <https://docs.kernel.org/userspace-api/seccomp_filter.html#return-values>.
///
/// NOTE that, e.g., `Errno(1)` and `Error(2)` are not ordered.
pub open spec fn precedence(self) -> nat {
match self {
Action::KillProcess => 7,
Action::KillThread => 6,
Action::Trap(_) => 5,
Action::Errno(_) => 4,
Action::Notify => 3,
Action::Trace(_) => 2,
Action::Log => 1,
Action::Allow => 0,
}
}
}
impl Rule {
/// `src/arch.h`.
pub const ARG_COUNT_MAX: u32 = 6;
/// Conditions required to validate and compile a rule.
pub open spec fn wf(self) -> bool {
&&& self.action.wf()
&&& forall |i: int| #![trigger self.conds@[i]]
0 <= i < self.conds@.len() ==> self.conds@[i].arg < Self::ARG_COUNT_MAX
// When allowing mux, the rule should not have any conditions
// since the multiplexed call may have different argument positions.
// TODO: Ideally, we should only check this if x86 is enabled
&&& !self.no_mux && self.syscall.can_mux() ==> self.conds@.len() == 0
}
}
impl Policy {
pub open spec fn wf(self) -> bool {
&&& self.act_no_match.wf()
&&& self.act_bad_arch.wf()
&&& forall |i: int, j: int| #![trigger self.archs@[i], self.archs@[j]]
0 <= i < j < self.archs@.len() ==> self.archs@[i] != self.archs@[j]
&&& forall |i: int| #![trigger self.rules@[i]]
0 <= i < self.rules@.len() ==> self.rules@[i].wf()
}
}
} // verus!
// Semantics
verus! {
/// `seccomp_data` without the instruction pointer.
pub struct Event {
pub arch: u32,
pub nr: i32,
pub args: Seq<u64>,
}
/// Results of matching a syscall name against an event.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Structural)]
pub enum SyscallMatch {
Exact,
/// Matches a `socketcall` or `ipc` call.
Mux,
None,
}
impl Arch {
// `AUDIT_ARCH_*` in `linux/audit.h`.
pub const TOKEN_X86: u32 = 0x4000_0003;
pub const TOKEN_X86_64: u32 = 0xC000_003E;
pub const TOKEN_ARM: u32 = 0x4000_0028;
pub const TOKEN_AARCH64: u32 = 0xC000_00B7;
/// Mask for the syscall number and arguments, depending on the architecture word size.
pub open spec fn mask(self) -> u64 {
if self == Arch::X86_64 || self == Arch::Aarch64 {
u64::MAX
} else {
0xFFFF_FFFF
}
}
/// Returns the arch token reported by the kernel (`linux/audit.h`).
pub open spec fn token(self) -> u32 {
match self {
Arch::X86 => Self::TOKEN_X86,
Arch::X86_64 => Self::TOKEN_X86_64,
Arch::Arm => Self::TOKEN_ARM,
Arch::Aarch64 => Self::TOKEN_AARCH64,
}
}
}
impl Event {
/// Whether the syscall name matches the event and if it is an exact match or a multiplexed match.
pub open spec fn matches_syscall(self, arch: Arch, name: Syscall) -> SyscallMatch {
if name.nr(arch) == Some(self.nr) {
SyscallMatch::Exact
} else if arch == Arch::X86 && {
// Matching against multiplexed `socketcall` or `ipc` on x86.
||| Syscall::Socketcall.nr(arch) == Some(self.nr)
&& name.to_socketcall_arg() == Some(self.args[0] & arch.mask())
||| Syscall::Ipc.nr(arch) == Some(self.nr)
// The kernel dispatches on the low 16 bits of the call number.
&& name.to_ipc_arg() == Some(self.args[0] & 0xFFFF)
} {
SyscallMatch::Mux
} else {
SyscallMatch::None
}
}
/// Parses a (little-endian) `seccomp_data` from the kernel into an `Event`.
pub open spec fn parse(data: &[u8]) -> Option<Event> {
if data@.len() != 64 {
None
} else {
Some(Event {
nr: ((data@[0] as u32) | (data@[1] as u32) << 8 | (data@[2] as u32) << 16 | (data@[3] as u32) << 24) as i32,
arch: (data@[4] as u32) | (data@[5] as u32) << 8 | (data@[6] as u32) << 16 | (data@[7] as u32) << 24,
// Offset 8 is `instruction_pointer`, which `Event` drops.
args: Seq::new(
Rule::ARG_COUNT_MAX as nat,
|k: int| (data@[16 + 8 * k] as u64)
| (data@[17 + 8 * k] as u64) << 8
| (data@[18 + 8 * k] as u64) << 16
| (data@[19 + 8 * k] as u64) << 24
| (data@[20 + 8 * k] as u64) << 32
| (data@[21 + 8 * k] as u64) << 40
| (data@[22 + 8 * k] as u64) << 48
| (data@[23 + 8 * k] as u64) << 56,
),
})
}
}
}
impl Action {
pub const RET_ACTION: u32 = 0xffff_0000;
pub const RET_DATA: u32 = 0x0000_ffff;
pub const RET_KILL_PROCESS: u32 = 0x8000_0000;
pub const RET_KILL_THREAD: u32 = 0x0000_0000;
pub const RET_TRAP: u32 = 0x0003_0000;
pub const RET_ERRNO: u32 = 0x0005_0000;
pub const RET_USER_NOTIF: u32 = 0x7fc0_0000;
pub const RET_TRACE: u32 = 0x7ff0_0000;
pub const RET_LOG: u32 = 0x7ffc_0000;
pub const RET_ALLOW: u32 = 0x7fff_0000;
/// Converts to the raw return value used in the BPF program.
pub open spec fn to_ret(&self) -> u32 {
match self {
Action::KillProcess => Self::RET_KILL_PROCESS,
Action::KillThread => Self::RET_KILL_THREAD,
Action::Trap(data) => Self::RET_TRAP | *data as u32,
Action::Errno(data) => Self::RET_ERRNO | *data as u32,
Action::Trace(data) => Self::RET_TRACE | *data as u32,
Action::Log => Self::RET_LOG,
Action::Allow => Self::RET_ALLOW,
Action::Notify => Self::RET_USER_NOTIF,
}
}
}
impl ArgCmp {
/// `_db_rule_gen_64` / `_db_rule_gen_32`.
pub open spec fn eval(self, arch: Arch, args: Seq<u64>) -> bool {
let x = args[self.arg as int] & arch.mask();
let a = self.a & arch.mask();
let b = self.b & arch.mask();
match self.op {
Compare::Ne => x != a,
Compare::Lt => x < a,
Compare::Le => x <= a,
Compare::Eq => x == a,
Compare::Ge => x >= a,
Compare::Gt => x > a,
Compare::MaskedEq => x & a == b & a,
}
}
}
impl Rule {
/// Whether this rule matches event `ev` on `arch`.
pub open spec fn eval(self, arch: Arch, ev: Event) -> bool {
let conds_hold = forall |i: int| #![trigger self.conds@[i]]
0 <= i < self.conds@.len() ==> self.conds@[i].eval(arch, ev.args);
match ev.matches_syscall(arch, self.syscall) {
SyscallMatch::Exact => conds_hold,
// NOTE: `Rule::wf` already enforces `self.conds@.len() == 0` if `!self.no_mux`
SyscallMatch::Mux => !self.no_mux,
SyscallMatch::None => false,
}
}
}
impl Policy {
pub open spec fn is_active_arch(self, arch: Arch, ev: Event) -> bool {
&&& self.archs@.contains(arch)
&&& ev.arch == arch.token()
// Reject x32 syscall numbers, except -1, which a tracer uses to skip a syscall.
&&& arch == Arch::X86_64 ==> ev.nr & 0x40000000 == 0 || Some(ev.nr) == Syscall::Skip.nr(arch)
}
/// Defines whether evaluating the policy on event `ev`
/// results in the action `act`, which may not be unique.
pub open spec fn eval(self, ev: Event, act: Action) -> bool
recommends self.wf(),
{
// The event is not from an active arch.
||| act == self.act_bad_arch && forall |a: Arch| !self.is_active_arch(a, ev)
// Exists a rule that, when evaluated on an active arch, matches the event and has the action `act`.
||| exists |a: Arch, i: int| {
&&& self.is_active_arch(a, ev)
&&& 0 <= i < self.rules@.len()
&&& #[trigger] self.rules@[i].eval(a, ev)
&&& self.rules@[i].action == act
// A disambiguation rule following kernel's behavior:
// 1. Higher precedence actions win.
// 2. If two actions have the same precedence (e.g. `Errno(1)` and `Errno(2)`),
// the rule that was added last wins.
//
// In particular, this makes installing multiple filters more well-behaved
// see for example [`crate::prop::theorem_eval_chain_compiled`].
&&& forall |j: int| #![trigger self.rules@[j]]
0 <= j < self.rules@.len() && j != i && self.rules@[j].eval(a, ev)
==> {
||| self.rules@[j].action.precedence() < act.precedence()
||| j < i && self.rules@[j].action.precedence() == act.precedence()
}
}
// Take the default action when no rule matches on any active arch.
||| {
&&& act == self.act_no_match
&&& exists |a: Arch| #[trigger] self.is_active_arch(a, ev)
&&& forall |a: Arch, i: int|
self.is_active_arch(a, ev) && 0 <= i < self.rules@.len()
==> !#[trigger] self.rules@[i].eval(a, ev)
}
}
}
} // verus!