src/HOL/Unix/document/root.tex
changeset 10966 8f2c27041a8e
child 10968 4882d65cc716
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Unix/document/root.tex	Tue Jan 23 18:05:53 2001 +0100
     1.3 @@ -0,0 +1,223 @@
     1.4 +
     1.5 +\documentclass[11pt,a4paper]{article}
     1.6 +\usepackage{isabelle,isabellesym,pdfsetup}
     1.7 +
     1.8 +%for best-style documents ...
     1.9 +\urlstyle{rm}
    1.10 +\isabellestyle{it}
    1.11 +
    1.12 +\renewcommand{\isabeginpar}{\par\smallskip}
    1.13 +\renewcommand{\isamarkupcmt}[1]{{\isastylecmt---~~#1}}
    1.14 +
    1.15 +\newcommand{\secref}[1]{\S\ref{#1}}
    1.16 +
    1.17 +
    1.18 +\begin{document}
    1.19 +
    1.20 +\title{Some aspects of Unix file-system security}
    1.21 +\author{Markus Wenzel \\ TU M\"unchen}
    1.22 +\maketitle
    1.23 +
    1.24 +\begin{abstract}
    1.25 +  Unix is a simple but powerful system where everything is either a process or
    1.26 +  a file.  Access to system resources works mainly via the file-system,
    1.27 +  including special files and devices.  Most Unix security issues are
    1.28 +  reflected directly within the file-system.  We give a mathematical model of
    1.29 +  the main aspects of the Unix file-system including its security model, but
    1.30 +  ignoring processes.  Within this formal model we discuss some aspects of
    1.31 +  Unix security, including a few odd effects caused by the general
    1.32 +  ``worse-is-better'' approach followed in Unix.
    1.33 +  
    1.34 +  Our formal specifications will be giving in simply-typed classical
    1.35 +  set-theory as provided by Isabelle/HOL.  Formal proofs are expressed in a
    1.36 +  human-readable fashion using the structured proof language of Isabelle/Isar,
    1.37 +  which is a system intended to support intelligible semi-automated reasoning
    1.38 +  over a wide range of application domains.  Thus the present development also
    1.39 +  demonstrates that Isabelle/Isar is sufficiently flexible to cover typical
    1.40 +  abstract verification tasks as well.  So far this has been the classical
    1.41 +  domain of interactive theorem proving systems based on unstructured tactic
    1.42 +  languages.
    1.43 +\end{abstract}
    1.44 +
    1.45 +\tableofcontents
    1.46 +\newpage
    1.47 +
    1.48 +\parindent 0pt\parskip 0.5ex
    1.49 +
    1.50 +
    1.51 +\section{Introduction}\label{sec:unix-intro}
    1.52 +
    1.53 +\subsection{The Unix philosophy}
    1.54 +
    1.55 +Over the last 2 or 3 decades the Unix community has collected a certain amount
    1.56 +of folklore wisdom on building systems that actually work, see
    1.57 +\cite{Unix-heritage} for further historical background information.  Here is a
    1.58 +recent account of the philosophical principles behind the Unix way of software
    1.59 +and systems engineering.\footnote{This has appeared on \emph{Slashdot} on
    1.60 +  25-March-2000, see \url{http://slashdot.com}, as well as
    1.61 +  \url{http://www.cix.co.uk/~dunnp/unix-philosophy.html}.}
    1.62 +
    1.63 +{\small
    1.64 +\begin{verbatim}
    1.65 +The UNIX Philosophy (Score:2, Insightful)
    1.66 +by yebb on Saturday March 25, @11:06AM EST (#69)
    1.67 +(User Info) 
    1.68 +
    1.69 +The philosophy is a result of more than twenty years of software
    1.70 +development and has grown from the UNIX community instead of being
    1.71 +enforced upon it. It is a defacto-style of software development. The
    1.72 +nine major tenets of the UNIX Philosophy are:
    1.73 +
    1.74 +  1. small is beautiful 
    1.75 +  2. make each program do one thing well 
    1.76 +  3. build a prototype as soon as possible 
    1.77 +  4. choose portability over efficiency 
    1.78 +  5. store numerical data in flat files 
    1.79 +  6. use software leverage to your advantage 
    1.80 +  7. use shell scripts to increase leverage and portability 
    1.81 +  8. avoid captive user interfaces 
    1.82 +  9. make every program a filter 
    1.83 +
    1.84 +The Ten Lesser Tenets 
    1.85 +
    1.86 +  1. allow the user to tailor the environment 
    1.87 +  2. make operating system kernels small and lightweight 
    1.88 +  3. use lower case and keep it short 
    1.89 +  4. save trees 
    1.90 +  5. silence is golden 
    1.91 +  6. think parallel 
    1.92 +  7. the sum of the parts if greater than the whole 
    1.93 +  8. look for the ninety percent solution 
    1.94 +  9. worse is better 
    1.95 + 10. think hierarchically 
    1.96 +\end{verbatim}
    1.97 +}
    1.98 +
    1.99 +The ``worse-is-better'' approach quoted above is particularly interesting.  It
   1.100 +basically means that \emph{relevant} concepts have to be implemented in the
   1.101 +right way, while \emph{irrelevant} issues are simply ignored in order to avoid
   1.102 +unnecessary complication of the design and implementation.  Certainly, the
   1.103 +overall quality of the resulting system heavily depends on the virtue of
   1.104 +distinction between the two categories of ``relevant'' and ``irrelevant''.
   1.105 +
   1.106 +
   1.107 +\subsection{Unix security}
   1.108 +
   1.109 +The main entities of a Unix system are \emph{files} and \emph{processes}
   1.110 +\cite{Tanenbaum:1992}.  Files subsume any persistent ``static'' entity managed
   1.111 +by the system --- ranging from plain files and directories, to more special
   1.112 +ones such device nodes, pipes etc.  On the other hand, processes are
   1.113 +``dynamic'' entities that may perform certain operations while being run by
   1.114 +the system.
   1.115 +
   1.116 +The security model of classic Unix systems is centered around the file system.
   1.117 +The operations permitted by a process that is run by a certain user are
   1.118 +determined from information stored within the file system.  This includes any
   1.119 +kind of access control, such as read/write access to some plain file, or
   1.120 +read-only access to a certain global device node etc.  Thus proper arrangement
   1.121 +of the main Unix file-system is very critical for overall
   1.122 +security.\footnote{Incidently, this is why the operation of mounting new
   1.123 +  volumes into the existing file space is usually restricted to the
   1.124 +  super-user.}
   1.125 +
   1.126 +\medskip Generally speaking, the Unix security model is a very simplistic one.
   1.127 +The original designers did not have maximum security in mind, but wanted to
   1.128 +get a decent system working for typical multi-user environments.  Contemporary
   1.129 +Unix implementations still follow the basic security model of the original
   1.130 +versions from the early 1970's \cite{Unix-heritage}.  Even back then there
   1.131 +would have been better approaches available, albeit with more complexity
   1.132 +involved both for implementers and users.
   1.133 +
   1.134 +On the other hand, even in the 2000's many computer systems are run with
   1.135 +little or no file-system security at all, even though virtually any system is
   1.136 +exposed to the net in one way or the other.  Even ``personal'' computer
   1.137 +systems have long left the comfortable home environment and entered the
   1.138 +wilderness of the open net sphere.
   1.139 +
   1.140 +\medskip This treatment of file-system security is a typical example of the
   1.141 +``worse-is-better'' principle introduced above.  The simplistic security model
   1.142 +of Unix got widely accepted within a large user community, while the more
   1.143 +innovative (and cumbersome) ones are only used very reluctantly and even tend
   1.144 +to be disabled by default in order to avoid confusion of beginners.
   1.145 +
   1.146 +
   1.147 +\subsection{Odd effects}
   1.148 +
   1.149 +Simplistic systems usually work very well in typical situations, but tend to
   1.150 +exhibit some odd features in non-typical ones.  As far as Unix file-system
   1.151 +security is concerned, there are many such features that are well-known to
   1.152 +experts, but may surprise naive users.
   1.153 +
   1.154 +Subsequently, we consider an example that is not so exotic after all.  As may
   1.155 +be easily experienced on a running Unix system, the following sequence of
   1.156 +commands may put a user's file-system into an uncouth state.  Below we assume
   1.157 +that \texttt{user1} and \texttt{user2} are working within the same directory
   1.158 +(e.g.\ somewhere within the home of \texttt{user1}).
   1.159 +
   1.160 +{\small
   1.161 +\begin{verbatim}
   1.162 +  user1> umask 000; mkdir foo; umask 022
   1.163 +  user2> mkdir foo/bar
   1.164 +  user2> touch foo/bar/baz
   1.165 +\end{verbatim}
   1.166 +}
   1.167 +  
   1.168 +That is, \texttt{user1} creates a directory that is writable for everyone, and
   1.169 +\texttt{user2} puts there a non-empty directory without write-access for
   1.170 +others.
   1.171 +
   1.172 +In this situation it has become impossible for \texttt{user1} to remove his
   1.173 +very own directory \texttt{foo} without the cooperation of either
   1.174 +\texttt{user2}, since \texttt{foo} contains another non-empty and non-writable
   1.175 +directory, which cannot be removed.
   1.176 +
   1.177 +{\small
   1.178 +\begin{verbatim}
   1.179 +  user1> rmdir foo
   1.180 +  rmdir: directory "foo": Directory not empty
   1.181 +  user1> rmdir foo/bar
   1.182 +  rmdir: directory "bar": Directory not empty
   1.183 +  user1> rm foo/bar/baz
   1.184 +  rm not removed: Permission denied
   1.185 +\end{verbatim}
   1.186 +}
   1.187 +
   1.188 +Only after \texttt{user2} has cleaned up his directory \texttt{bar}, is
   1.189 +\texttt{user1} enabled to remove both \texttt{foo/bar} and \texttt{foo}.
   1.190 +Alternatively \texttt{user2} could remove \texttt{foo/bar} as well.  In the
   1.191 +unfortunate case that \texttt{user2} does not cooperate or is presently
   1.192 +unavailable, \texttt{user1} would have to find the super user (\texttt{root})
   1.193 +to clean up the situation.  In Unix \texttt{root} may perform any file-system
   1.194 +operation without any access control limitations.\footnote{This is the typical
   1.195 +  Unix way of handling abnormal situations: while it is easy to run into odd
   1.196 +  cases due to simplistic policies it as well quite easy to get out.  There
   1.197 +  are other well-known systems that make it somewhat harder to get into a fix,
   1.198 +  but almost impossible to get out again!}
   1.199 +
   1.200 +\bigskip Is there really no other way out for \texttt{user1} in the above
   1.201 +situation?  Experiments can only show possible ways, but never demonstrate the
   1.202 +absence of other means exhaustively.  This is a typical situation where
   1.203 +(formal) proof may help.  Subsequently, we model the main aspects Unix
   1.204 +file-system security within Isabelle/HOL \cite{Nipkow-et-al:2000:HOL} and
   1.205 +prove that there is indeed no way for \texttt{user1} to get rid of his
   1.206 +directory \texttt{foo} without help by others (see
   1.207 +\secref{sec:unix-main-result} for the main theorem stating this).
   1.208 +
   1.209 +\medskip The formal techniques employed in this development are the typical
   1.210 +ones for abstract ``verification'' tasks, namely induction and case analysis
   1.211 +over the structure of file-systems and possible system transitions.
   1.212 +Isabelle/HOL \cite{Nipkow-et-al:2000:HOL} is particularly well-suited for this
   1.213 +kind of application.  By the present development we also demonstrate that the
   1.214 +Isabelle/Isar environment \cite{Wenzel:1999:TPHOL,Wenzel:2000:isar-ref} for
   1.215 +readable formal proofs is sufficiently flexible to cover non-trivial
   1.216 +verification tasks as well.  So far this has been the classical domain of
   1.217 +``interactive'' theorem proving systems based on unstructured tactic
   1.218 +languages.
   1.219 +
   1.220 +
   1.221 +\input{Unix}
   1.222 +
   1.223 +\bibliographystyle{abbrv}
   1.224 +\bibliography{root}
   1.225 +
   1.226 +\end{document}