Stoic: Towards Disciplined Capabilities

Capabilities are widely used in the design of software systems to ensure security. A system of capabilities can become a mess in the presence of objects and functions: objects may leak capabilities and functions may capture capabilities. They make reasoning and enforcing invariants in capability-based systems challenging if not intractable. How to reason about capability-based systems formally? What abstractions that programming languages should provide to facilitate the construction of capability-based systems? Can we formulate some fundamental capability disciplines as typing rules? In this paper we propose that stoicity is a useful property in designing, reasoning and organizing capabilities in systems both at the macro-level and micro-level. Stoicity means that a component of a system does not interact with its environment in any way except through its interfaces. As an incarnation of this idea, we introduce stoic functions in a functional language. In contrast to normal functions, stoic functions cannot capture capabilities nor non-stoic functions from the environment. We formalize stoic functions in a language with mutable references as capabilities. In that setting, we show that stoic functions enjoy non-interference of memory effects. The concept of stoic functions also shows its advantage in ffect polymorphism and effect masking when used to control side effects of programs.


Année
Jan 09 2020
Mots-clefs:
Laboratoires:


Note: Le statut de ce fichier est: Anyone


 Notice créée le 2020-01-09, modifiée le 2020-04-20

PREPRINT:
Télécharger le document
PDF

Évaluer ce document:

Rate this document:
1
2
3
 
(Pas encore évalué)