This module implements a labeled filesystem as a file store in which a label is associated with every file and directory. The module LIO.Handle provides an interface for working with labeled directories and files -- this module provides the underlying low-level (mostly trusted) interface.
The file store contains 3 components:
.magicfile containing a sequence of pre-defined bytes. The existence of this file and correct contents indicates that the file store and root of the labeled filesystem were created before any system crash.
.objdirectory containing all the objects (files and directories) in the filesystem, organized according to the object's label.
ROOTsymbolic link pointing to a directory object in
.obj, representing the root of the filesystem.
As the details of
ROOT are straight forward, we
now focus on the details of
Each object is stored in
.obj in a directory corresponding
to the label of the file. For example, an object protected by
bob's label will exist as:
oTAUzOt5YoQAyThw89eSgWuig-0= is the base64url encoding of
the (SHA-224 hash of) label
obj012345 is the object's
name. Each label directory also contains a
.label file whose
contents correspond to the serialization of the label. Hence, for
Every object in a label directory is either a file or a directory. If the object is a directory, its contents will strictly have symbolic links to objects in the file store. This is more easily understood using an example.
Consider the following familiar filesystem layout, containing 4 directories and 2 files:
/ |-- bobOralice (type: directory, label: bob \/ alice) | |-- alice (type: directory, label: alice) | |-- bob (type: directory, label: bob) | | '-- secret (type: file , label: bob) | '-- messages (type: file , label: bob \/ alice) '-- clarice (type: directory, label: clarice)
Suppose we take
/lioFS as the location of the file store for our
labeled filesystem. The above files and directories will have the
same layout in our file system, but each file/directory points to
an object in the object store (
.obj), as shown below.
/lioFS/ROOT |-- bobOralice -> ../../c_EkXYGrmrSit9j_8VjP_-8DgaM=/objXIBabq | |-- alice -> ../../12to8q3vDp7ApyKEQk2LQ_2nrvs=/objqZeR5w | |-- bob -> ../../oTAUzOt5YoQAyThw89eSgWuig-0=/objtsePnc | | '-- secret -> ../../oTAUzOt5YoQAyThw89eSgWuig-0=/objFIQCIm | '-- messages -> ../../c_EkXYGrmrSit9j_8VjP_-8DgaM=/objQaiwuA '-- clarice -> ../../wordEFmBzWc7Q6qP-TetDgZaG8A=/objOMh0mj
Note that, to a user, the interface (see LIO.Handle) is unchanged and they do not need to handle or understand the underlying file store. We refer to this view as "friendly". The file store for the above layout is:
/lioFS/ |-- .magic |-- .obj | |-- 12to8q3vDp7ApyKEQk2LQ_2nrvs= | | |-- .label (=alice's label) | | '-- objqZeR5w | |-- c_EkXYGrmrSit9j_8VjP_-8DgaM= | | |-- .label (=label bob \/ alice) | | |-- objQaiwuA | | '-- objXIBabq | | |-- alice -> ../../12to8q3vDp7ApyKEQk2LQ_2nrvs=/objqZeR5w | | |-- bob -> ../../oTAUzOt5YoQAyThw89eSgWuig-0=/objtsePnc | | '-- messages -> ../../c_EkXYGrmrSit9j_8VjP_-8DgaM=/objQaiwuA | |-- jX7q5Kb8_G4GsjgNpOHB17kypQo= | | |-- .label (=label of the filesystem root) | | '-- objTj5JZD | | |-- bobOralice -> ../../c_EkXYGrmrSit9j_8VjP_-8DgaM=/objXIBabq | | '-- clarice -> ../../wordEFmBzWc7Q6qP-TetDgZaG8A=/objOMh0mj | |-- oTAUzOt5YoQAyThw89eSgWuig-0= | | |-- .label (=bob's label) | | |-- objFIQCIm | | '-- objtsePnc | | '-- secret -> ../../oTAUzOt5YoQAyThw89eSgWuig-0=/objFIQCIm | '-- wordEFmBzWc7Q6qP-TetDgZaG8A= | |-- .label (=clarice's label) | '-- objOMh0mj '-- ROOT -> .obj/jX7q5Kb8_G4GsjgNpOHB17kypQo=/objTj5JZD
Observe that every directory object contains symbolic links pointing to file or directory objects in the store.
Accessing any file or directory in the "friendly" view requires
a lookup (
lookupObjPath) of the corresponding object. Each
path is, however, relative to the root. So, for example,
/aliceOrbob/bob/ actually corresponds to looking
/lioFS/ROOT/aliceOrbob/bob/. This prevents untrusted code
from accessing objects by guessing filenames and further allows
untrusted code to pick arbitrary filenames (including
Several precautions are taken to keep the filesystem in a working state in case of a crash. The code tries to maintain the invariant that any inconsistencies will either be:
- temporary files or directories whose names start with the
#" character, or
- dangling symbolic links.
Both of these inconsistencies can be checked and cleaned up
locally without examining the whole file system. The code tries
to fix up these inconsistencies on-the-fly as it encounters them.
However, it could possibly leave some stranded temporary
- evalWithRoot :: (Serialize l, LabelState l p s) => FilePath -> Maybe l -> LIO l p s a -> s -> IO (a, l)
- lookupObjPath :: (LabelState l p s, Serialize l) => FilePath -> LIO l p s (LFilePath l)
- lookupObjPathP :: (LabelState l p s, Serialize l) => p -> FilePath -> LIO l p s (LFilePath l)
- getObjLabelTCB :: (Serialize l, LabelState l p s) => FilePath -> LIO l p s l
- createFileTCB :: (Serialize l, Label l) => l -> FilePath -> IOMode -> IO Handle
- createDirectoryTCB :: (Serialize l, Label l) => l -> FilePath -> IO ()
- data LFilePath l
- labelOfFilePath :: Label l => LFilePath l -> l
- unlabelFilePath :: LabelState l p s => LFilePath l -> LIO l p s FilePath
- unlabelFilePathP :: LabelState l p s => p -> LFilePath l -> LIO l p s FilePath
- unlabelFilePathTCB :: Label l => LFilePath l -> FilePath
- cleanUpPath :: LabelState l p s => FilePath -> LIO l p s FilePath
- stripSlash :: FilePath -> FilePath
|:: (Serialize l, LabelState l p s)|
|-> Maybe l|
Label of root
|-> LIO l p s a|
|-> IO (a, l)|
evalLIO, but takes two additional parameters
corresponding to the path of the labeled filesystem store and the
label of the root. If the labeled filesystem store does not exist,
it is created at the specified path with the root having the
If the filesystem does exist, the supplied label is ignored and thus
unnecessary. However, if the root label is not provided and the
filesystem has not been initialized, then
lbot is used as the
Creating and finding (labeled) objects
Given a pathname (forced to be relative to the root of the labeled filesystem), find the path to the corresponding object. The current label is raised to reflect all the directories traversed. Note that if the object does not exist an exception will be thrown; the label of the exception will be the join of all the directory labels up to the lookup failure.
Additionally, this function cleans up the
path before doing the lookup, so e.g., path
first be rewritten to
/foo and thus no traversal to
Note that this is a more permissive behavior than forcing the read
|:: (LabelState l p s, Serialize l)|
Path to object
|-> LIO l p s (LFilePath l)|
lookupObjPath but takes an additional privilege object
that is exercised when raising the current label.
Read the label file of an object. Note that because the format
of the supplied path is not checked this function is considered to
be in the
Create a file object with the given label and link the supplied path to the object. The handle to the file is returned.
Create a directory object with the given label and link the supplied path to the object.
Unlabel a filepath. If the path corresponds to a directory, you can now get the contents of the directory; if it's a file, you can open the file.
unlabelFilePath but uses privileges to unlabel the
Trusted version of
unlabelFilePath that ignores IFC.
Misc helper functions
Cleanup a file path, if it starts out with a
.., we consider
this invalid as it can be used explore parts of the filesystem
that should otherwise be unaccessible. Similarly, we remove any
from the path.