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