src/HOL/Unix/document/root.tex
author wenzelm
Tue Jan 23 18:05:53 2001 +0100 (2001-01-23)
changeset 10966 8f2c27041a8e
child 10968 4882d65cc716
permissions -rw-r--r--
added HOL-Unix example;
     1 
     2 \documentclass[11pt,a4paper]{article}
     3 \usepackage{isabelle,isabellesym,pdfsetup}
     4 
     5 %for best-style documents ...
     6 \urlstyle{rm}
     7 \isabellestyle{it}
     8 
     9 \renewcommand{\isabeginpar}{\par\smallskip}
    10 \renewcommand{\isamarkupcmt}[1]{{\isastylecmt---~~#1}}
    11 
    12 \newcommand{\secref}[1]{\S\ref{#1}}
    13 
    14 
    15 \begin{document}
    16 
    17 \title{Some aspects of Unix file-system security}
    18 \author{Markus Wenzel \\ TU M\"unchen}
    19 \maketitle
    20 
    21 \begin{abstract}
    22   Unix is a simple but powerful system where everything is either a process or
    23   a file.  Access to system resources works mainly via the file-system,
    24   including special files and devices.  Most Unix security issues are
    25   reflected directly within the file-system.  We give a mathematical model of
    26   the main aspects of the Unix file-system including its security model, but
    27   ignoring processes.  Within this formal model we discuss some aspects of
    28   Unix security, including a few odd effects caused by the general
    29   ``worse-is-better'' approach followed in Unix.
    30   
    31   Our formal specifications will be giving in simply-typed classical
    32   set-theory as provided by Isabelle/HOL.  Formal proofs are expressed in a
    33   human-readable fashion using the structured proof language of Isabelle/Isar,
    34   which is a system intended to support intelligible semi-automated reasoning
    35   over a wide range of application domains.  Thus the present development also
    36   demonstrates that Isabelle/Isar is sufficiently flexible to cover typical
    37   abstract verification tasks as well.  So far this has been the classical
    38   domain of interactive theorem proving systems based on unstructured tactic
    39   languages.
    40 \end{abstract}
    41 
    42 \tableofcontents
    43 \newpage
    44 
    45 \parindent 0pt\parskip 0.5ex
    46 
    47 
    48 \section{Introduction}\label{sec:unix-intro}
    49 
    50 \subsection{The Unix philosophy}
    51 
    52 Over the last 2 or 3 decades the Unix community has collected a certain amount
    53 of folklore wisdom on building systems that actually work, see
    54 \cite{Unix-heritage} for further historical background information.  Here is a
    55 recent account of the philosophical principles behind the Unix way of software
    56 and systems engineering.\footnote{This has appeared on \emph{Slashdot} on
    57   25-March-2000, see \url{http://slashdot.com}, as well as
    58   \url{http://www.cix.co.uk/~dunnp/unix-philosophy.html}.}
    59 
    60 {\small
    61 \begin{verbatim}
    62 The UNIX Philosophy (Score:2, Insightful)
    63 by yebb on Saturday March 25, @11:06AM EST (#69)
    64 (User Info) 
    65 
    66 The philosophy is a result of more than twenty years of software
    67 development and has grown from the UNIX community instead of being
    68 enforced upon it. It is a defacto-style of software development. The
    69 nine major tenets of the UNIX Philosophy are:
    70 
    71   1. small is beautiful 
    72   2. make each program do one thing well 
    73   3. build a prototype as soon as possible 
    74   4. choose portability over efficiency 
    75   5. store numerical data in flat files 
    76   6. use software leverage to your advantage 
    77   7. use shell scripts to increase leverage and portability 
    78   8. avoid captive user interfaces 
    79   9. make every program a filter 
    80 
    81 The Ten Lesser Tenets 
    82 
    83   1. allow the user to tailor the environment 
    84   2. make operating system kernels small and lightweight 
    85   3. use lower case and keep it short 
    86   4. save trees 
    87   5. silence is golden 
    88   6. think parallel 
    89   7. the sum of the parts if greater than the whole 
    90   8. look for the ninety percent solution 
    91   9. worse is better 
    92  10. think hierarchically 
    93 \end{verbatim}
    94 }
    95 
    96 The ``worse-is-better'' approach quoted above is particularly interesting.  It
    97 basically means that \emph{relevant} concepts have to be implemented in the
    98 right way, while \emph{irrelevant} issues are simply ignored in order to avoid
    99 unnecessary complication of the design and implementation.  Certainly, the
   100 overall quality of the resulting system heavily depends on the virtue of
   101 distinction between the two categories of ``relevant'' and ``irrelevant''.
   102 
   103 
   104 \subsection{Unix security}
   105 
   106 The main entities of a Unix system are \emph{files} and \emph{processes}
   107 \cite{Tanenbaum:1992}.  Files subsume any persistent ``static'' entity managed
   108 by the system --- ranging from plain files and directories, to more special
   109 ones such device nodes, pipes etc.  On the other hand, processes are
   110 ``dynamic'' entities that may perform certain operations while being run by
   111 the system.
   112 
   113 The security model of classic Unix systems is centered around the file system.
   114 The operations permitted by a process that is run by a certain user are
   115 determined from information stored within the file system.  This includes any
   116 kind of access control, such as read/write access to some plain file, or
   117 read-only access to a certain global device node etc.  Thus proper arrangement
   118 of the main Unix file-system is very critical for overall
   119 security.\footnote{Incidently, this is why the operation of mounting new
   120   volumes into the existing file space is usually restricted to the
   121   super-user.}
   122 
   123 \medskip Generally speaking, the Unix security model is a very simplistic one.
   124 The original designers did not have maximum security in mind, but wanted to
   125 get a decent system working for typical multi-user environments.  Contemporary
   126 Unix implementations still follow the basic security model of the original
   127 versions from the early 1970's \cite{Unix-heritage}.  Even back then there
   128 would have been better approaches available, albeit with more complexity
   129 involved both for implementers and users.
   130 
   131 On the other hand, even in the 2000's many computer systems are run with
   132 little or no file-system security at all, even though virtually any system is
   133 exposed to the net in one way or the other.  Even ``personal'' computer
   134 systems have long left the comfortable home environment and entered the
   135 wilderness of the open net sphere.
   136 
   137 \medskip This treatment of file-system security is a typical example of the
   138 ``worse-is-better'' principle introduced above.  The simplistic security model
   139 of Unix got widely accepted within a large user community, while the more
   140 innovative (and cumbersome) ones are only used very reluctantly and even tend
   141 to be disabled by default in order to avoid confusion of beginners.
   142 
   143 
   144 \subsection{Odd effects}
   145 
   146 Simplistic systems usually work very well in typical situations, but tend to
   147 exhibit some odd features in non-typical ones.  As far as Unix file-system
   148 security is concerned, there are many such features that are well-known to
   149 experts, but may surprise naive users.
   150 
   151 Subsequently, we consider an example that is not so exotic after all.  As may
   152 be easily experienced on a running Unix system, the following sequence of
   153 commands may put a user's file-system into an uncouth state.  Below we assume
   154 that \texttt{user1} and \texttt{user2} are working within the same directory
   155 (e.g.\ somewhere within the home of \texttt{user1}).
   156 
   157 {\small
   158 \begin{verbatim}
   159   user1> umask 000; mkdir foo; umask 022
   160   user2> mkdir foo/bar
   161   user2> touch foo/bar/baz
   162 \end{verbatim}
   163 }
   164   
   165 That is, \texttt{user1} creates a directory that is writable for everyone, and
   166 \texttt{user2} puts there a non-empty directory without write-access for
   167 others.
   168 
   169 In this situation it has become impossible for \texttt{user1} to remove his
   170 very own directory \texttt{foo} without the cooperation of either
   171 \texttt{user2}, since \texttt{foo} contains another non-empty and non-writable
   172 directory, which cannot be removed.
   173 
   174 {\small
   175 \begin{verbatim}
   176   user1> rmdir foo
   177   rmdir: directory "foo": Directory not empty
   178   user1> rmdir foo/bar
   179   rmdir: directory "bar": Directory not empty
   180   user1> rm foo/bar/baz
   181   rm not removed: Permission denied
   182 \end{verbatim}
   183 }
   184 
   185 Only after \texttt{user2} has cleaned up his directory \texttt{bar}, is
   186 \texttt{user1} enabled to remove both \texttt{foo/bar} and \texttt{foo}.
   187 Alternatively \texttt{user2} could remove \texttt{foo/bar} as well.  In the
   188 unfortunate case that \texttt{user2} does not cooperate or is presently
   189 unavailable, \texttt{user1} would have to find the super user (\texttt{root})
   190 to clean up the situation.  In Unix \texttt{root} may perform any file-system
   191 operation without any access control limitations.\footnote{This is the typical
   192   Unix way of handling abnormal situations: while it is easy to run into odd
   193   cases due to simplistic policies it as well quite easy to get out.  There
   194   are other well-known systems that make it somewhat harder to get into a fix,
   195   but almost impossible to get out again!}
   196 
   197 \bigskip Is there really no other way out for \texttt{user1} in the above
   198 situation?  Experiments can only show possible ways, but never demonstrate the
   199 absence of other means exhaustively.  This is a typical situation where
   200 (formal) proof may help.  Subsequently, we model the main aspects Unix
   201 file-system security within Isabelle/HOL \cite{Nipkow-et-al:2000:HOL} and
   202 prove that there is indeed no way for \texttt{user1} to get rid of his
   203 directory \texttt{foo} without help by others (see
   204 \secref{sec:unix-main-result} for the main theorem stating this).
   205 
   206 \medskip The formal techniques employed in this development are the typical
   207 ones for abstract ``verification'' tasks, namely induction and case analysis
   208 over the structure of file-systems and possible system transitions.
   209 Isabelle/HOL \cite{Nipkow-et-al:2000:HOL} is particularly well-suited for this
   210 kind of application.  By the present development we also demonstrate that the
   211 Isabelle/Isar environment \cite{Wenzel:1999:TPHOL,Wenzel:2000:isar-ref} for
   212 readable formal proofs is sufficiently flexible to cover non-trivial
   213 verification tasks as well.  So far this has been the classical domain of
   214 ``interactive'' theorem proving systems based on unstructured tactic
   215 languages.
   216 
   217 
   218 \input{Unix}
   219 
   220 \bibliographystyle{abbrv}
   221 \bibliography{root}
   222 
   223 \end{document}