LIO.FS

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:

• .magic file 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.
• .obj directory containing all the objects (files and directories) in the filesystem, organized according to the object's label.
• ROOT symbolic link pointing to a directory object in .obj, representing the root of the filesystem.

As the details of .magic and ROOT are straight forward, we now focus on the details of .obj.

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:

 .obj/oTAUzOt5YoQAyThw89eSgWuig-0=/obj012345

where oTAUzOt5YoQAyThw89eSgWuig-0= is the base64url encoding of the (SHA-224 hash of) label bob, and 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 example,

 .obj/oTAUzOt5YoQAyThw89eSgWuig-0=/.label

would have bob's label.

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, looking up /aliceOrbob/bob/ actually corresponds to looking up /lioFS/ROOT/aliceOrbob/bob/. This prevents untrusted code from accessing objects by guessing filenames and further allows untrusted code to pick arbitrary filenames (including .label, .obj, etc.).

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:

1. temporary files or directories whose names start with the "#" character, or
2. 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 .label files.

Documentation

evalWithRoot

Arguments

:: (Serialize l, LabelState l p s)

=> FilePath

Filesystem root

-> Maybe l

Label of root

-> LIO l p s a

LIO action

-> s

Initial state

-> IO (a, l)

Same as 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 supplied label. 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 root label.

Creating and finding (labeled) objects

lookupObjPath

Arguments

:: (LabelState l p s, Serialize l)

=> FilePath

Path to object

-> LIO l p s (LFilePath l)

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 foobar/.. will first be rewritten to /foo and thus no traversal to bar. Note that this is a more permissive behavior than forcing the read of .. from bar.

lookupObjPathP

Arguments

:: (LabelState l p s, Serialize l)

=> p

Privilege

-> FilePath

Path to object

-> LIO l p s (LFilePath l)

Same as lookupObjPath but takes an additional privilege object that is exercised when raising the current label.

getObjLabelTCB :: (Serialize l, LabelState l p s) => FilePath -> LIO l p s l

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 TCB.

createFileTCB :: (Serialize l, Label l) => l -> FilePath -> IOMode -> IO Handle

Create a file object with the given label and link the supplied path to the object. The handle to the file is returned.

createDirectoryTCB :: (Serialize l, Label l) => l -> FilePath -> IO ()

Create a directory object with the given label and link the supplied path to the object.

Labeled FilePath

data LFilePath l

Label associated with a FilePath.

labelOfFilePath :: Label l => LFilePath l -> l

Get the label of a labeled filepath.

unlabelFilePath :: LabelState l p s => LFilePath l -> LIO l p s FilePath

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.

unlabelFilePathP :: LabelState l p s => p -> LFilePath l -> LIO l p s FilePath

Same as unlabelFilePath but uses privileges to unlabel the filepath.

unlabelFilePathTCB :: Label l => LFilePath l -> FilePath

Trusted version of unlabelFilePath that ignores IFC.

Misc helper functions

cleanUpPath :: LabelState l p s => FilePath -> LIO l p s FilePath

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.

stripSlash :: FilePath -> FilePath

Remove any pathSeparators from the front of a file path.