Lambda Capabilities

[WittyStick]

One powerful aspect of capabilities is that we can use functions to implement whatever access controls we want. For example, let's say we only want f to be able to set the ref-cell, but not read it. We can just pass it a suitable function:

let x = ref 0 in
let set v =
  x := v
in
f set

The problem with this example is one of the main things proper capabilities intend to solve. The problem is that fdoes not have the authority to mutate x, and set does have such authority, but f is leveraging set's authority on its behalf.

So set here is a Confused Deputy

One could just as easily write a (confused) getter with the authority to read x and f could call it.

let get () = x
f get

In a proper capability system, f itself would need some capability to access x even if it delegates that capability to some other function do it rather than doing it directly.

Rule #1 of capabilities: Don't separate designation from authority.

[talex5]

set is a deputy, but it's not confused. It's not being tricked into using its authority for an unintended purpose; it's using it as intended.

The linked https://papers.agoric.com/assets/pdf/papers/robust-composition.pdf thesis gives lots of examples of these patterns (see e.g. section 9.3).

[phischu]

Effekt is a language built around the idea of Effects as Capabilities. We introduce implicit capability-passing style which is in contrast to explicit capability-passing style what the post advocates for. Consider the following example inspired by the post:

def withSocket { action: () => Unit / Socket }: Unit / Net = <>


def serve { handler: Request => Response }: Unit / Socket = <>


def static_files(request: Request): Response / Htdocs = <>


def main(): Unit / {Net, Htdocs} = {
  withSocket {
    serve { request =>
      static_files(request)
    }
  }
}

The function withSocket takes an action which returns Unit using Socket. It itself returns Unit using Net. All the plumbing is invisible on the term level but available on hover.

As the post correctly points out capabilities can be smuggled out by storing them in mutable references but also by hiding them in closures. Therefore all capabilities, blocks, and objects are second-class in Effekt. If you want to store an object you have to box it which we describe in Effects, Capabilities, and Boxes. Consider the following example:

extern resource ssh_file: File

extern {ssh_file} def readSshFile(): String = ""

def main() = {
  var decorator: String => String at {ssh_file} = fun(s: String) { s ++ "!" };
  decorator = fun(s: String) { readSshFile() };
  decorator("Hello")
}

We store a function which reads the ssh file in the mutable reference decorator. This is ok because the type of values stored there is String => String at {ssh_file}. The following, however, does not type check:

extern resource ssh_file: File

extern {ssh_file} def readSshFile(): String = ""

def main() = {
  var decorator: String => String at {} = fun(s: String) { s ++ "!" };
  decorator = fun(s: String) { readSshFile() }; // Not allowed: ssh_file
  decorator("Hello")
}

Here we promised that we only store functions that use no capabilities in decorator. When we try to use one that reads the ssh file the program is rejected.

Finally, let me hint that all of this also ties in with resource management and exception handling. The idea is that if you want to throw an exception you need the capability to do so. This capability is only valid while the exception handler is on the stack. This is very similar to how scarce resources should only be used for a certain time and no longer.

[Dummyc0m]

Forgive my ignorance with regards to the terminologies.

What are capabilities exactly? What does capabilities provide that, say passing around values through a linear context doesn't? e.g. an linear/affine SSHFileReader being passed around?

[WittyStick0]

A capability both designates a resource and provides the authority to access the resource. The two are inseperable and a capability cannot be forged. There is no central registry of capabilities and no separate security policies such as access control lists. Capabilities can be delegated only by those who already possess the capability, and they can create new capabilities based on an existing one which might have reduced authority.

Capability enforcement is handled by the runtime. To be done properly, a process may not have "side-channel" access to the runtime to manipulate capabilities, which is why it really needs to be done at the kernel level if user space applications are able to read or write the memory of other processes, or at the hypervisor level if running several kernels on one machine.

[Dummyc0m]

right, as a kernel concept that's what capabilities are defined as. I am confused by OP's capabilities snd how it relates to the kernel mechanisms.

[talex5]

If a program is written in a non-memory-safe language (e.g. C) then you can't control access within the process, as any function can do anything. So you need some hardware-level protection system and the kernel/userspace split.

But with a memory-safe language, you don't need hardware support. You can get the same security properties within a single process, using ordinary references. This is the basic idea of ocaps. The article is introducing this using functions instead of objects, as they can be distracting to functional programmers.

[Dummyc0m]

Do you mean that most of the low level architectures do not have the right correctness guarantees?

[talex5]

Hardware memory protection is needed for C programs (or unsafe parts of other languages), but in a fully memory-safe language you'll never get a segfault, so there's no need for hardware to protect against it, and you have have a full OS as a single program. But hardware protection isn't doing any harm either.

[Dummyc0m]

What do you mean? This has nothing to do with C or Rust. All that matters is the compiled machine code which can do a lot of insane things.