Policy as Types

TL;DR

This paper explores representing security policies as types within a behavioral type system for the RHO-calculus, aiming to enhance expressiveness in object-capability systems.

Contribution

It introduces a novel approach to encode policies as types using the Curry-Howard isomorphism in a reflective higher-order pi-calculus variant.

Findings

Policy as types can effectively model object-capability security policies

The approach leverages the Curry-Howard isomorphism for policy expression

Potential for improved security guarantees in object-capability systems

Abstract

Drossopoulou and Noble argue persuasively for the need for a means to express policy in object-capability-based systems. We investigate a practical means to realize their aim via the Curry-Howard isomorphism. Specifically, we investigate representing policy as types in a behavioral type system for the RHO-calculus, a reflective higher-order variant of the pi-calculus.