As software ecosystems grow larger, an increasingly-common type of security vulnerability is the supply chain attack. Austral solves this problem using capability-based security, which adds permission checking to code.
To the filesystem, or the network, or some other privileged resource, code has to be explicitly passed a linear value, called a capability, representing the permission to access that resource.
A capability is a value that represents an unforgeable proof of the authority to perform an action. They have the following properties:
Capabilities can be destroyed.
Capabilities can be surrended by passing them to others.
Capabilities cannot be duplicated.
Capabilities cannot be acquired out of thin air: they must be passed by the client.
Capabilities in Austral are implemented as linear types: they are destroyed by being consumed, they are surrended by simply passing the value to a function, they are non-duplicable since linear types cannot be duplicated.
Example: Environment Variables
Consider a non-capability-secure API for accessing and modifying environment variables:
module Env is function get(name: String): Option[String]; function put(name: String, value: String): Unit; end module.
Often, sensitive data is stored in the environment. We don’t want arbitrary code to be able to access it. How do we lock this down? Like so:
module Env is type EnvCap: Linear; generic [R: Region] function acquire(root: &[RootCapability, R]): EnvCap; function release(cap: EnvCap): Unit; generic [R: Region] function get(cap: &[EnvCap, R], name: String): Option[String]; generic [R: Region] function put(cap: &![EnvCap, R], name: String, value: String): Unit; end module.
EnvCap is a linear value that represents the ability to access the
environment. Since it is an opaque type, it cannot be created by clients. The
only way to construct an instance of the
EnvCap type is via the
function. Dually, the
release function consumes the capability.
put functions have been modified so that they take a reference
to the capability: essentially, the client has to pass proof that they have an
EnvCap in order to use these functions.
Here’s how you’d use this:
function main(root: RootCapability): ExitCode is -- Acquire the environment capability from -- a reference to the root capability. let cap: EnvCap := acquire(&root); -- Now we can interact with the environment. print(get(&cap, "HOME")); put(&!cap, "TERM", "xterm"); -- Release the capability; release(cap); -- Release the root capability; surrenderRoot(root); -- Finally, end the program by returning -- the success status code. return ExitSuccess(); end;
The Root Capability
Capabilities cannot be created out of thin air: they can only be created by proving proof that the client has access to a more powerful capability. This recursion has to end somewhere.
The root of the capability hierarchy is the built-in
type. Values of this type cannot be created by the programmer. A root capability
is the first and only argument to an Austral program’s entrypoint function:
function main(root: RootCapability): ExitCode is -- Do something effectful here. -- ... -- Release the root capability; surrenderRoot(root); -- End the program. return ExitSuccess(); end;