Confinement for Active Objects

TL;DR

This paper introduces a formal security framework for distributed active objects, utilizing a semi-lattice security model and a type system to ensure safe communication and confinement in distributed functional active object programming.

Contribution

It presents a novel formal security model and type system for distributed active objects, enabling secure method calls and confinement properties.

Findings

Security model based on semi-lattice for multi-lateral security

Type safety and confinement property established for ASPfun

Secure down calls implemented in the programming model

Abstract

In this paper, we provide a formal framework for the security of distributed active objects. Active objects communicate asynchronously implementing method calls via futures. We base the formal framework on a security model that uses a semi-lattice to enable multi-lateral security crucial for distributed architectures. We further provide a security type system for the programming model ASPfun of functional active objects. Type safety and a confinement property are presented. ASPfun thus realizes secure down calls.