[cap-talk] Announcing "Analysing Object-Capability Security" Paper and Authodox v. 0.2.0

[David-Sarah Hopwood]

Jonathan S. Shapiro wrote:
>   1. The opaqueness boundary at the OS/application layer is a problem,
>      because it forces the OS to make mostly static, conservative
>      assumptions about program behavior. For most programs this is fine,
>      but there are two classes of important programs for which it is
>      a problem:
[...]
>      B  Memoryless programs. There is a class of programs that require
>         state for realistic implementations, but none of that state
>         remains live when the program returns from a given request.
>         The OS cannot see this. Functional programming doesn't help,
>         because the compiled realization of a functional program is
>         generally stateful.

I'd dispute that functional programming doesn't help here. It helps by
providing a high-level programming model that does not depend on use of
logically visible state.

It is true that typical current implementations of functional
programming languages make heavy use of implementation-level state.
But suppose that the OS could snapshot the state of the process after
an initialization phase, and then reset it to the snapshot after each
application-level request. That would allow existing language
implementations (functional or not) to be used in a way that obtains
most of the advantages of statelessness, for application programs that
are logically stateless between requests.

>   4. Given a formal model, it really ought to be possible to connect
>      the capability invocation layer (which occurs at the level of
>      application semantics) to the behavior within the OS (which occurs
>      at the layer of the cap runtime formal model).
> 
> Point [4] was still fairly inchoate in my mind at that time. It took a
> comment by MarkM years later to bring it into clear focus: capability
> semantics is the semantics of lambda calculus with side effects.

*Sequential* capability semantics is essentially the semantics of the
lambda calculus with side effects.

-- 
David-Sarah Hopwood