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