Nicollet.Net

My apologies to my non-technical readers: this article is going to be a hairy, brain-roasting piece of technical innovation. The same goes for my technical readers not familiar with Hindley-Milner.

The Problem

An access control system is a piece of software architecture that makes sure only authorized users can access certain parts of the software. Access restrictions are usually defined as rules in a variety of formats. The most basic ones apply to general user categories and features: for instance, only a moderator (user category) can ban another user (feature). Rules can get extremely complex. For your amusement, here’s a real-life example:

The event page may be edited by the creator of that event page, by the moderator of any of the groups in which that event was posted, or by any global administrator account, as long as the editing user has entered their password at least once since they entered the website.

As a software architect mindful of the safety of your data, you have a few basic requirements for any access control system:

• Exhaustivity: no access should remain unchecked. It’s usually easy to determine through code reviews if a developer forgot to write the access-checking code for a feature. But that code is even slightly off, you have a potential disaster on your hands. This is usually solved by applying obscene amounts of testing, both automated and human, to check if all unauthorized accesses are denied by the system correctly.
• Predictability: one should tell if an operation is possible without actually trying it. This is useful for hiding unavailable buttons, displaying error messages in advance, or simply acting in a transactional manner when rollback is not available. This is usually solved by factoring out the code that does the access-checking, and call it both from the actual operation, and from any code that is about to run the operation and wonders if it can be done.
• Readability: since documentation inevitably goes out of sync, the code should be readable enough by itself to determine what the access rules are. A 50-line sequence of API calls, database queries and well-named variables will require some reverse engineering, no matter how well-named the variable are.

This is pretty hard to achieve, mostly because every single project out there contains code like the one below:

User.checkRecipientList(Request.recipients, Request.user)

foreach (var recipient in Request.recipients)
{
    var email = new Email();

    email.From = Request.user
    email.To   = recipient;
    email.attach(file);
    email.send();
}

Of course, the main danger is that the Email class was not written to check that the sender can indeed send a message with an attachment to the recipient. Of course, this can be solved through code reviews, which scan all classes in search of missing access control code, and functional tests, because the specs said an error message should appear. These are costly, tedious solutions that eliminate that problem. However, assuming that the class was indeed written correctly, there’s another problem:

• The sending either fails silently (no user error message: bad user interface design!) or throws an exception which results in a partial sending (you can’t cancel email once it is sent).
• The compiler has no reason to complain or warn the developer about anything.
• The developer wrote this code at 7 p.m. and had something else to do on the next morning.
• The code reviewer and unit tester didn’t know there was a special rule about sending attachments, and expect User.checkRecipientList to throw an error if a recipient is invalid.
• The code coverage tool is perfectly fine with this.
• The specs merely said «an error appears if a recipient is invalid»

In short, this piece of code contains a time bomb that no user or software can detect until it happens.

The Tools

Before I explain what I’ll be doing, I need to describe the tools I’m going to use. As you might have guessed from the Hindley-Milner reference above, I’ll be using a variant of ML, namely Objective Caml. The language provides a sophisticated type system, entirely checked at compile-time, and which can be almost completely inferred from the code (that is, you almost never have to add type annotations to your programs). For instance :

let print_integer x =
  printf "The integer is %d" x

print_integer "hello"

This code defines a function called print_integer that accepts a single argument, and uses the classic printf function to print it. It then tries to call that function with a string argument. The Objective Caml type inference algorithm will look at the format, which contains a single %d, and deduce that it expects a single integer argument. From there, it deduces that the first argument to print_integer should be an integer, and the function returns nothing : int -> unit. As a consequence passing a string is a type error :

This expression has type string but an expression was expected of type int

A highly expressive compile-time type system means we can use it to prove important properties about our software, but it increases the size of type expressions (because types have to carry more information) : and type inference means we won’t have to write those long type expressions everywhere.

Objective Caml types are parametric, which works a bit like generics in C# and Java. The type system automatically infers the type parameters from the code :

let first_element array =
  array.(0)

In this example, the type of the function would be correctly identified as 'a array -> 'a : accepts an argument which is an array of a generic type 'a, and returns an element of that same type 'a. There are plenty of parametric types in the standard library alone : 'a array, 'a list, 'a option…

The latter is the Objective Caml replacement for null values : the language does not allow values to be null (when you say a variable is an array, then it’s always a valid array), so values that might be missing are explicitly tagged as optional using the option type. For instance, when you’re looking for an item in a database, you might want to return an optional type to represent the situation where the item is missing. While exceptions would interrupt the control flow and rise up to the nearest try-catch block that can handle them, using options forces the developer to decide on the spot what he wants to do with the value, usually with pattern matching:

match Database.read id with
  | Some item -> frobnicate item
  | None      -> frobnicate default_item

Options have the advantage that you can’t forget to handle the null case, because you have to use pattern matching to access the returned value. On the contrary, you can always forget that an exception might be thrown (and it’s not obvious when doing a code review, either).

The Solution

Another important element of the Objective Caml type system is the ability of modules to hide away type information. Consider the following example :

type 'a page = { password : string ; id : int }

let read page =
  Database.read page.id

let write page content =
  Database.write page.id content

let unlock page password =
  if password = page.password then Some page else None

let lock page =
  page

This is an elementary access control system : you can read both locked and unlocked pages, but once you lock a page, you need to unlock it with a password before you can write to it again. Looking at the code above, this doesn’t appear at all : theres no locked/unlocked boolean variable on the page, which means I could pass a locked page to the write function and it would not complain about it at all! The lock function merely returns its argument without doing anything to it! The only password-related code is the unlock function, which does indeed check that a page is password-protected, but there’s no need to unlock a page before it’s written to…

The unnecessary type parameter on the page type should have been a hint, and it all becomes clear when one looks at the module signature :

type 'a page

val read   : 'a page -> string
val write  : [`Unlocked] page -> string -> unit
val unlock : [`Locked]   page -> string -> [`Unlocked] page option
val lock   : [`Unlocked] page -> [`Locked] page

This module signature describes how every other module in the system will see our page-related functions. It hides the definition of the page type, to prevent people from accessing its fields directly, uses the seemingly unnecessary type parameter to carry additional information about the locked/unlocked state of the page, and it restricts the type of the write function to only accept pages which are unlocked. All of this is allowed : as long as the signature defines a type that’s more restrictive than the actual type inside the module, it’s still going to work.

So, from inside the module, the page is fully accessible regardless of its locked/unlocked status, but outside the module, the locked/unlocked status is enforced at compile time by the type system. This is very important : if you try to write to the page without asking for a password first, you don’t get a runtime exception, you get a compiler error message. And a pretty clean one, too:

This expression has type [`Locked] page but an expression was expected of type [`Unlocked] page

Also, since the definition of the page type is hidden away by the module signature, the only way to create an unlocked page is with the unlock function above.

As for performance, once the software is compiled, all of this vanishes into nothingness : Objective Caml only uses type information for checking the validity of the program, and discards it from the final binary.

All of it using only standard language features. Can your language do that?

This approach revolves around proving that you have access to a certain feature of a certain object. That proof is created by a first function (the provider) , placed in the type parameter of the object, and required by a second function (the consumer) that actually performs the intended operation. In the example above:

• The unlock function is a provider : it proves that the user knows the password by placing [`Unlocked] in the type parameter of the page.
• The write function is a consumer : it expects the page to be [`Unlocked] before it writes data to it.

In short, you have providers that perform the access control tests (is this user authenticated? is he an administrator? does he know the password?) and then securely store the result of those tests to be used by the features they are protecting. The type system prevents the users from using features without successfully calling the providers first, and the module system lets you write providers and consumers without having to define brand new types all the time.

The security comes from the fact that if the consumer expects a certain proof (as an argument of specified type) then that argument was necessarily returned by one of the providers able to create that proof. Tight control of proof providers (made possible by the fact that providers are always in the same module as the one that defines the type that carries the proof) combined with responsible and conservative definition of consumers helps keep a system safe and secure.

A Few Examples

In practice, the proof that is being carried around takes many shapes, the two main ones being about proving who the user is, and proving what the user can do. The provider of who-proofs is the authentication system, which digs up information about the user from the cookie, the session and the database, and concludes about its nature:

type 'a user

val current_user : [`Unknown] user
val as_admin     : 'a user -> [`Admin] user option

It’s fairly common to transform who-proofs into what-proofs based on generic rules such as “an administrator can edit everything“:

type 'a page

val edit_by_author : 'a page -> 'b user-> [`Editable] page option
val edit_by_admin  : 'a page -> [`Admin] user -> [`Editable] page
val edit           : [`Editable] page -> string -> unit

This illustrates the difference between absolute rules and conditional rules : “an administrator can edit everything” is an absolute rule, because it’s always true, whereas “the author can edit his creation” is a conditional rule because the user might not be the author of the page. This is outlined in the example above by the fact that one function returns an option (indicating the possibility of failure) while the other does not.

The edit-by-author property could also be handled by representing ownership as a proof on the page :

val is_author      : 'a page -> 'b user -> [`Owned] page option
val edit_by_author : [`Owned] page -> [`Editable] page

As an example, the above can be used to construct a generic “editable” function that accepts any page and user as an argument, and proves whether the page can be edited by the user :

let editable page user =
    match is_admin user with
    | Some admin -> Some (edit_by_admin admin page)
    | None -> match is_author page user with
              | Some owned -> Some (edit_by_author owned)
              | None -> None

val editable : 'a page -> 'b user -> [`Editable] page option

Another example would be giving another user a token that they can use to edit a page, but do nothing else :

let prove_editable page =
  hash (secret_key, page.id, "editable")

val prove_editable : [`Editable] page -> string

let check_proof_editable proof page =
  if proof = hash (secret_key, page.id, "editable") then Some page else None

val check_proof_editable : string -> 'a page -> [`Editable] page option

This effectively lets you serialize a proof to a string, and later unserialize it to allow edit access to a user that normally couldn’t have edited the page.