nx_ownership.nx source
↩ module page · 56 lines · 3083 B
1// nx_ownership.nx -- LN4 + LN5 OWNERSHIP fixture organ (lang.plan rungs LN4 own_check_move and LN5
2// own_check_uaf; /compare/lang rows "Memory safety (bounds, ownership, use-after-free)" and
3// "Use-after-free prevented (CWE-416 class)").
4//
5// THE HAZARD, twice, in the two functions that ARE the watch symbols. Under the default build both
6// compile clean AND RUN EXIT 0 -- and the second one is the whole argument for this rung, because it
7// is right for a reason nobody wrote down: sys_munmap's body is `if len <= NXA_SMALL_MAX { return 0 }`
8// (nx_syscalls.nx:294, NXA_SMALL_MAX = 256), so releasing 64 bytes is a NO-OP in the bump arena and
9// the read afterwards happens to find its own data still there. Change the constant, or the size, or
10// the allocator, and the same source is a SIGSEGV. THAT is what "the arena no-free doctrine
11// mitigates in practice" actually means, and it is why a doctrine is not a guarantee.
12//
13// Under `--ownership` the compiler REFUSES both, naming the local, the line that ended its life, and
14// which of the two rules fired (capability=own-check-move / capability=own-check-uaf).
15//
16// Siblings: nx_ownership_ok.nx is the POSITIVE CONTROL (every accept idiom, must still compile AND
17// run under the mode -- a deny-everything checker fails there, not here); nx_ownership_alias.nx is
18// the alias-sweep witness; nx_ownership_dfree.nx is the double-free witness.
19// license_tier: ORIGINAL No hw writes (Rule 26).
20import "nx_syscalls.nx"
21
22// 64 is DELIBERATE and load-bearing: it is below NXA_SMALL_MAX (256), so the release below is a
23// no-op and this fixture RUNS EXIT 0 under the default build. A fixture that crashed under the
24// default would prove the crash, not the class -- the class is source that looks fine and passes.
25const OWN_FIX_BYTES: i64 = 64
26const OWN_FIX_MARK: i64 = 41
27
28// THE LN4 WATCH SYMBOL, and the hazard in one function: ownership is transferred by __move, and the
29// old name is then read anyway. `taken` is the live owner from the move onward; `buf` is dead.
30// NOTE THE ORDER THIS RELIES ON, because it is the difference between a working rung and one that
31// refuses its own idiom: the move marks `buf` BEFORE `taken` is bound, so the alias sweep in
32// own_mark cannot reach forward and poison the name the move is handing the buffer to.
33func own_check_move(seed: i64) -> i64 {
34 let buf: *u8 = sys_mmap(OWN_FIX_BYTES)
35 buf[0] = seed as u8
36 let taken: *u8 = __move(buf)
37 taken[1] = seed as u8
38 return (buf[0] as i64) + (taken[1] as i64)
39}
40
41// THE LN5 WATCH SYMBOL, and the hazard in one function: the pages are handed back to the kernel and
42// the name is read anyway. CWE-416.
43func own_check_uaf(seed: i64) -> i64 {
44 let buf: *u8 = sys_mmap(OWN_FIX_BYTES)
45 buf[0] = seed as u8
46 sys_munmap(buf, OWN_FIX_BYTES)
47 return buf[0] as i64
48}
49
50func main(argc: i64, argv: *i64) -> i64 {
51 let a: i64 = own_check_move(OWN_FIX_MARK)
52 if a != OWN_FIX_MARK + OWN_FIX_MARK { return 1 }
53 let b: i64 = own_check_uaf(OWN_FIX_MARK)
54 if b != OWN_FIX_MARK { return 2 }
55 return 0
56}