src/HOL/Unix/document/root.tex
changeset 11102 5ceaa79c220d
parent 10968 4882d65cc716
child 11862 03801fd2f8fc
equal deleted inserted replaced
11101:014e7b5c77ba 11102:5ceaa79c220d
   187 unfortunate case that \texttt{user2} does not cooperate or is presently
   187 unfortunate case that \texttt{user2} does not cooperate or is presently
   188 unavailable, \texttt{user1} would have to find the super user (\texttt{root})
   188 unavailable, \texttt{user1} would have to find the super user (\texttt{root})
   189 to clean up the situation.  In Unix \texttt{root} may perform any file-system
   189 to clean up the situation.  In Unix \texttt{root} may perform any file-system
   190 operation without any access control limitations.\footnote{This is the typical
   190 operation without any access control limitations.\footnote{This is the typical
   191   Unix way of handling abnormal situations: while it is easy to run into odd
   191   Unix way of handling abnormal situations: while it is easy to run into odd
   192   cases due to simplistic policies it as well quite easy to get out.  There
   192   cases due to simplistic policies it is as well quite easy to get out.  There
   193   are other well-known systems that make it somewhat harder to get into a fix,
   193   are other well-known systems that make it somewhat harder to get into a fix,
   194   but almost impossible to get out again!}
   194   but almost impossible to get out again!}
   195 
   195 
   196 \bigskip Is there really no other way out for \texttt{user1} in the above
   196 \bigskip Is there really no other way out for \texttt{user1} in the above
   197 situation?  Experiments can only show possible ways, but never demonstrate the
   197 situation?  Experiments can only show possible ways, but never demonstrate the