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{\isamarkupcmt}[1]{{\isastylecmt---~~#1}}
10
11\newcommand{\secref}[1]{\S\ref{#1}}
12
13
14\begin{document}
15
16\title{Some aspects of Unix file-system security}
17\author{Markus Wenzel \\ TU M\"unchen}
18\maketitle
19
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.
29  
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}
40
41\tableofcontents
42\newpage
43
44\parindent 0pt\parskip 0.5ex
45
46
47\section{Introduction}\label{sec:unix-intro}
48
49\subsection{The Unix philosophy}
50
51Over the last 2 or 3 decades the Unix community has collected a certain amount
52of folklore wisdom on building systems that actually work, see
53\cite{Unix-heritage} for further historical background information.  Here is a
54recent account of the philosophical principles behind the Unix way of software
55and systems engineering.\footnote{This has appeared on \emph{Slashdot} on
56  25-March-2000, see \url{http://slashdot.com}.}
57
58{\small
59\begin{verbatim}
60The UNIX Philosophy (Score:2, Insightful)
61by yebb on Saturday March 25, @11:06AM EST (#69)
62(User Info) 
63
64The philosophy is a result of more than twenty years of software
65development and has grown from the UNIX community instead of being
66enforced upon it. It is a defacto-style of software development. The
67nine major tenets of the UNIX Philosophy are:
68
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 
78
79The Ten Lesser Tenets 
80
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}
93
94The ``worse-is-better'' approach quoted above is particularly interesting.  It
95basically means that \emph{relevant} concepts have to be implemented in the
96right way, while \emph{irrelevant} issues are simply ignored in order to avoid
97unnecessary complication of the design and implementation.  Certainly, the
98overall quality of the resulting system heavily depends on the virtue of
99distinction between the two categories of ``relevant'' and ``irrelevant''.
100
101
102\subsection{Unix security}
103
104The main entities of a Unix system are \emph{files} and \emph{processes}
105\cite{Tanenbaum:1992}.  Files subsume any persistent ``static'' entity managed
106by the system --- ranging from plain files and directories, to more special
107ones such device nodes, pipes etc.  On the other hand, processes are
108``dynamic'' entities that may perform certain operations while being run by
109the system.
110
111The security model of classic Unix systems is centered around the file system.
112The operations permitted by a process that is run by a certain user are
113determined from information stored within the file system.  This includes any
114kind of access control, such as read/write access to some plain file, or
115read-only access to a certain global device node etc.  Thus proper arrangement
116of the main Unix file-system is very critical for overall
117security.\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.}
120
121\medskip Generally speaking, the Unix security model is a very simplistic one.
122The original designers did not have maximum security in mind, but wanted to
123get a decent system working for typical multi-user environments.  Contemporary
124Unix implementations still follow the basic security model of the original
125versions from the early 1970's \cite{Unix-heritage}.  Even back then there
126would have been better approaches available, albeit with more complexity
127involved both for implementers and users.
128
129On the other hand, even in the 2000's many computer systems are run with
130little or no file-system security at all, even though virtually any system is
131exposed to the net in one way or the other.  Even ``personal'' computer
132systems have long left the comfortable home environment and entered the
133wilderness of the open net sphere.
134
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
137of Unix got widely accepted within a large user community, while the more
138innovative (and cumbersome) ones are only used very reluctantly and even tend
139to be disabled by default in order to avoid confusion of beginners.
140
141
142\subsection{Odd effects}
143
144Simplistic systems usually work very well in typical situations, but tend to
145exhibit some odd features in non-typical ones.  As far as Unix file-system
146security is concerned, there are many such features that are well-known to
147experts, but may surprise naive users.
148
149Subsequently, we consider an example that is not so exotic after all.  As may
150be easily experienced on a running Unix system, the following sequence of
151commands may put a user's file-system into an uncouth state.  Below we assume
152that \texttt{user1} and \texttt{user2} are working within the same directory
153(e.g.\ somewhere within the home of \texttt{user1}).
154
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}
162  
163That 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
165others.
166
167In this situation it has become impossible for \texttt{user1} to remove his
168very own directory \texttt{foo} without the cooperation of either
169\texttt{user2}, since \texttt{foo} contains another non-empty and non-writable
170directory, which cannot be removed.
171
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}
182
183Only after \texttt{user2} has cleaned up his directory \texttt{bar}, is
184\texttt{user1} enabled to remove both \texttt{foo/bar} and \texttt{foo}.
185Alternatively \texttt{user2} could remove \texttt{foo/bar} as well.  In the
186unfortunate case that \texttt{user2} does not cooperate or is presently
187unavailable, \texttt{user1} would have to find the super user (\texttt{root})
188to clean up the situation.  In Unix \texttt{root} may perform any file-system
189operation 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!}
194
195\bigskip Is there really no other way out for \texttt{user1} in the above
196situation?  Experiments can only show possible ways, but never demonstrate the
197absence of other means exhaustively.  This is a typical situation where
198(formal) proof may help.  Subsequently, we model the main aspects Unix
199file-system security within Isabelle/HOL \cite{Nipkow-et-al:2000:HOL} and
200prove that there is indeed no way for \texttt{user1} to get rid of his
201directory \texttt{foo} without help by others (see
202\secref{sec:unix-main-result} for the main theorem stating this).
203
204\medskip The formal techniques employed in this development are the typical
205ones for abstract ``verification'' tasks, namely induction and case analysis
206over the structure of file-systems and possible system transitions.
207Isabelle/HOL \cite{Nipkow-et-al:2000:HOL} is particularly well-suited for this
208kind of application.  By the present development we also demonstrate that the
209Isabelle/Isar environment \cite{Wenzel:1999:TPHOL,Wenzel:2002:isar-ref} for
210readable formal proofs is sufficiently flexible to cover non-trivial
211verification tasks as well.  So far this has been the classical domain of
212``interactive'' theorem proving systems based on unstructured tactic
213languages.
214
215
216\input{Unix}
217
218\bibliographystyle{abbrv}
219\bibliography{root}
220
221\end{document}
222