Let's get started by diving into a simple model of access control on files. Along the way, we'll see some basic concepts from functional programming in general and a couple of F*-specific features.
Let's say we want to model a simple access control discipline on files—certain files are readable or writable, whereas others may be unauthorized. We'd like to write a policy to describe the privileges on each file, and we'd like to write programs whose file accesses are checked against this policy, guaranteeing statically that an unauthorized file is never accessed mistakenly.
Our model of this scenario (which we'll make more realistic in later sections) proceeds in three easy steps.
The syntax of F* is based closely on the syntax of OCaml and the non-light syntax of F#. Our F* program is made up of one module per file, and the body of the module contains a number of definitions, and optionally includes a ‘main’ expression.
Here are the first three definitions from the program:
type filename = string
(** [canWrite] is a function specifying whether a file [f] can be written *)
let canWrite (f:filename) =
match f with
| "demo/tempfile" -> true
| _ -> false
(** [canRead] is also a function ... *)
let canRead (f:filename) =
canWrite f (* writeable files are also readable *)
|| f="demo/README" (* and so is demo/README *)
The first definition defines a type synonym: we'll use strings to model filenames.
After that, we define two boolean functions: canWrite and canRead: The canWrite function inspects its argument f using a pattern matching expression: it returns the boolean true when f equals "demo/tempfile" and false otherwise. The function canRead is similar—a file is readable if it is writable, or if it is the "demo/README" file.
Last modified 01 July 2021