src/HOL/Unix/document/root.tex
author wenzelm
Tue Jan 23 18:17:14 2001 +0100 (2001-01-23)
changeset 10968 4882d65cc716
parent 10966 8f2c27041a8e
child 11102 5ceaa79c220d
permissions -rw-r--r--
tuned;
     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}.}
    58 
    59 {\small
    60 \begin{verbatim}
    61 The UNIX Philosophy (Score:2, Insightful)
    62 by yebb on Saturday March 25, @11:06AM EST (#69)
    63 (User Info) 
    64 
    65 The philosophy is a result of more than twenty years of software
    66 development and has grown from the UNIX community instead of being
    67 enforced upon it. It is a defacto-style of software development. The
    68 nine major tenets of the UNIX Philosophy are:
    69 
    70   1. small is beautiful 
    71   2. make each program do one thing well 
    72   3. build a prototype as soon as possible 
    73   4. choose portability over efficiency 
    74   5. store numerical data in flat files 
    75   6. use software leverage to your advantage 
    76   7. use shell scripts to increase leverage and portability 
    77   8. avoid captive user interfaces 
    78   9. make every program a filter 
    79 
    80 The Ten Lesser Tenets 
    81 
    82   1. allow the user to tailor the environment 
    83   2. make operating system kernels small and lightweight 
    84   3. use lower case and keep it short 
    85   4. save trees 
    86   5. silence is golden 
    87   6. think parallel 
    88   7. the sum of the parts if greater than the whole 
    89   8. look for the ninety percent solution 
    90   9. worse is better 
    91  10. think hierarchically 
    92 \end{verbatim}
    93 }
    94 
    95 The ``worse-is-better'' approach quoted above is particularly interesting.  It
    96 basically means that \emph{relevant} concepts have to be implemented in the
    97 right way, while \emph{irrelevant} issues are simply ignored in order to avoid
    98 unnecessary complication of the design and implementation.  Certainly, the
    99 overall quality of the resulting system heavily depends on the virtue of
   100 distinction between the two categories of ``relevant'' and ``irrelevant''.
   101 
   102 
   103 \subsection{Unix security}
   104 
   105 The main entities of a Unix system are \emph{files} and \emph{processes}
   106 \cite{Tanenbaum:1992}.  Files subsume any persistent ``static'' entity managed
   107 by the system --- ranging from plain files and directories, to more special
   108 ones such device nodes, pipes etc.  On the other hand, processes are
   109 ``dynamic'' entities that may perform certain operations while being run by
   110 the system.
   111 
   112 The security model of classic Unix systems is centered around the file system.
   113 The operations permitted by a process that is run by a certain user are
   114 determined from information stored within the file system.  This includes any
   115 kind of access control, such as read/write access to some plain file, or
   116 read-only access to a certain global device node etc.  Thus proper arrangement
   117 of the main Unix file-system is very critical for overall
   118 security.\footnote{Incidently, this is why the operation of mounting new
   119   volumes into the existing file space is usually restricted to the
   120   super-user.}
   121 
   122 \medskip Generally speaking, the Unix security model is a very simplistic one.
   123 The original designers did not have maximum security in mind, but wanted to
   124 get a decent system working for typical multi-user environments.  Contemporary
   125 Unix implementations still follow the basic security model of the original
   126 versions from the early 1970's \cite{Unix-heritage}.  Even back then there
   127 would have been better approaches available, albeit with more complexity
   128 involved both for implementers and users.
   129 
   130 On the other hand, even in the 2000's many computer systems are run with
   131 little or no file-system security at all, even though virtually any system is
   132 exposed to the net in one way or the other.  Even ``personal'' computer
   133 systems have long left the comfortable home environment and entered the
   134 wilderness of the open net sphere.
   135 
   136 \medskip This treatment of file-system security is a typical example of the
   137 ``worse-is-better'' principle introduced above.  The simplistic security model
   138 of Unix got widely accepted within a large user community, while the more
   139 innovative (and cumbersome) ones are only used very reluctantly and even tend
   140 to be disabled by default in order to avoid confusion of beginners.
   141 
   142 
   143 \subsection{Odd effects}
   144 
   145 Simplistic systems usually work very well in typical situations, but tend to
   146 exhibit some odd features in non-typical ones.  As far as Unix file-system
   147 security is concerned, there are many such features that are well-known to
   148 experts, but may surprise naive users.
   149 
   150 Subsequently, we consider an example that is not so exotic after all.  As may
   151 be easily experienced on a running Unix system, the following sequence of
   152 commands may put a user's file-system into an uncouth state.  Below we assume
   153 that \texttt{user1} and \texttt{user2} are working within the same directory
   154 (e.g.\ somewhere within the home of \texttt{user1}).
   155 
   156 {\small
   157 \begin{verbatim}
   158   user1> umask 000; mkdir foo; umask 022
   159   user2> mkdir foo/bar
   160   user2> touch foo/bar/baz
   161 \end{verbatim}
   162 }
   163   
   164 That is, \texttt{user1} creates a directory that is writable for everyone, and
   165 \texttt{user2} puts there a non-empty directory without write-access for
   166 others.
   167 
   168 In this situation it has become impossible for \texttt{user1} to remove his
   169 very own directory \texttt{foo} without the cooperation of either
   170 \texttt{user2}, since \texttt{foo} contains another non-empty and non-writable
   171 directory, which cannot be removed.
   172 
   173 {\small
   174 \begin{verbatim}
   175   user1> rmdir foo
   176   rmdir: directory "foo": Directory not empty
   177   user1> rmdir foo/bar
   178   rmdir: directory "bar": Directory not empty
   179   user1> rm foo/bar/baz
   180   rm not removed: Permission denied
   181 \end{verbatim}
   182 }
   183 
   184 Only after \texttt{user2} has cleaned up his directory \texttt{bar}, is
   185 \texttt{user1} enabled to remove both \texttt{foo/bar} and \texttt{foo}.
   186 Alternatively \texttt{user2} could remove \texttt{foo/bar} as well.  In the
   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})
   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
   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
   193   are other well-known systems that make it somewhat harder to get into a fix,
   194   but almost impossible to get out again!}
   195 
   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
   198 absence of other means exhaustively.  This is a typical situation where
   199 (formal) proof may help.  Subsequently, we model the main aspects Unix
   200 file-system security within Isabelle/HOL \cite{Nipkow-et-al:2000:HOL} and
   201 prove that there is indeed no way for \texttt{user1} to get rid of his
   202 directory \texttt{foo} without help by others (see
   203 \secref{sec:unix-main-result} for the main theorem stating this).
   204 
   205 \medskip The formal techniques employed in this development are the typical
   206 ones for abstract ``verification'' tasks, namely induction and case analysis
   207 over the structure of file-systems and possible system transitions.
   208 Isabelle/HOL \cite{Nipkow-et-al:2000:HOL} is particularly well-suited for this
   209 kind of application.  By the present development we also demonstrate that the
   210 Isabelle/Isar environment \cite{Wenzel:1999:TPHOL,Wenzel:2000:isar-ref} for
   211 readable formal proofs is sufficiently flexible to cover non-trivial
   212 verification tasks as well.  So far this has been the classical domain of
   213 ``interactive'' theorem proving systems based on unstructured tactic
   214 languages.
   215 
   216 
   217 \input{Unix}
   218 
   219 \bibliographystyle{abbrv}
   220 \bibliography{root}
   221 
   222 \end{document}