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}