bend-osdev-caps

Releases (1)

• 0.1.0.0 indexed

Definitions (282)

LAWS.bend

• law execve_result
• law execve_effective_within_permitted
• law execve_ambient_within_permitted
• law execve_ambient_within_inheritable
• law execve_valid
• law execve_bounding_unchanged
• law execve_inheritable_unchanged
• law execve_permitted_boundeda capability that is in none of the bounding, inheritable and ambient sets never becomes permitted (the bounding set does not mask the inheritable set: capabilities(7), "Capability bounding set")
• law execve_permitted_bounded_validwith the ambient invariant, the bound is the bounding and inheritable sets
• law execve_root_permitted"when a process whose real and effective UIDs are zero execve(2)s a program": P'(permitted) = P(inheritable) | P(bounding), and P'(effective) = P'(permitted).
• law execve_root_effective
• law execve_nonroot_permitted"if a process with nonzero user IDs performs an execve(2) then any capabilities that are present in its permitted and effective sets will be cleared": of a file without set-ID bits or capabilities, only the ambient set remains, as both permitted and effective.
• law execve_nonroot_effective
• law capset_permitted_never_grows
• law capset_bounding_unchanged
• law capset_valid
• law bset_drop_never_grows
• law bset_drop_rest_unchangeddropping from the bounding set changes no other set (in particular, not the inheritable set)
• law ambient_raise_valid
• law ambient_lower_valid
• law ambient_raise_rest_unchanged
• law ambient_lower_rest_unchanged
• law ambient_clear_all_empty
• law name_first
• law name_last
• law name_beyond
• law of_name_sys_admin
• law show_fullthe full set, as /proc/<pid>/status shows it on Linux 5.9 and later
• law show_twoCAP_NET_RAW (13) and CAP_NET_BIND_SERVICE (10): 0x2400
• law vector_dumb_binaryA capability-dumb binary (cap_net_raw=ep) run by a non-root user whose bounding set lacks CAP_NET_RAW: execve fails with EPERM.
• law vector_suid_root_with_capsA set-user-ID-root program with file capabilities (cap_net_bind_service=ep) run by user 1000: the effective and saved UIDs become 0, and the process gains just the file's capabilities.
• law vector_suid_root_plainThe same program without file capabilities gains every capability in the bounding set.
• law vector_suid_ignoredWith no_new_privs (ign), the set-user-ID bit is ignored: nothing is gained.
• law vector_capset_growscapset may not add to the permitted set
• law vector_ambient_not_inheritablean ambient capability must be permitted and inheritable
• law vector_drop_invalid41 is beyond CAP_CHECKPOINT_RESTORE
• law witness_validWitnesses: every hypothesis of the laws above holds for some input, so no law is vacuous.
• law witness_ambient_inheritableambient within inheritable, for a credential's sets and for a state
• law witness_ambient_inheritable_state
• law witness_nonzero_uida nonzero user ID (the non-root laws' hypotheses on the real and effective user IDs)

PROOF.bend

• def bits.disc
• def bits.disc2
• def bits.ft
• def bits.tf
• def bits.absurd
• def bits.absurd_eq
• def bits.absurd_tf
• def bool.and_l
• def bool.and_r
• def bool.and3
• def valid.intro
• def valid.ep
• def valid.ap
• def valid.ai
• def bool.and2
• def set.fin_ff
• def set.fin_tf
• def set.bridge
• def set.sub_introa set within another, from its parts within theirs, and back
• def set.sub_lo
• def set.sub_hi
• def set.eq_introtwo sets are equal when their parts are
• def bits.sub_refl
• def bits.sub_zero
• def bits.sub_or_r
• def bits.sub_minus
• def bits.bound_a
• def bits.bound_z
• def bits.bound_va
• def bits.bound_vz
• def bits.amb_p
• def bits.amb_i
• def bits.lub
• def bits.minus_within
• def bits.root_a
• def bits.root_z
• def bits.nonroot
• def set.sub_refl
• def set.sub_zero
• def set.sub_or_r
• def set.sub_minus
• def set.bound_a
• def set.bound_z
• def set.bound_va
• def set.bound_vz
• def set.amb_p
• def set.amb_i
• def set.lub
• def set.minus_within
• def set.root_a
• def set.root_z
• def set.nonroot
• def caps.has_ofa set that has capability k contains the set {k} (has is that subset test)
• def ex.eff
• def ex.ap
• def ex.ai
• def ex.bnd
• def ex.inh
• def ex.bound
• def ex.bound_v