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