abstract ;;Quote: setuid is poorly designed and widely misused; causes security vulnerabilities

abstract+;;Quote: develop finite state model of user ids; uncover pitfalls in setuid, define proper usage, and propose a high-level API

6 ;;Quote: model userids as a finite state automata; each process tracks its privilege level with a real, effective, and saved uid; transitions are system calls

6 ;;Quote: build a finite state model by 1) identifying states as kernel variables and 2) finding transitions by trying every system call; collapse equivalent states

7 ;;Quote: double check the finite state model by setting and getting the user ids

8 ;;Quote: build model-extraction algorithm from getstate(), setstate(), and getallstates(); for each state, determine effect of each system call

11 ;;Quote: the operating system must behave deterministically relative to its finite state model; if not, add global variables to state; each state represented by an equivalence class

12 ;;Quote: verifying a finite state model is much easier that fully understanding a system's behavior; e.g., only four operations on user IDs

13 ;;Quote: use finite state model to check proper usage of uid-setting system calls; build a finite state model of the program; check for privileged regions

18 ;;Quote: setuid API for temporary and permanent privileges; works for OpenSSH; does not handle group privileges