Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
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.
,
Boi Faltings, Robert West, Maxime Jean Julien Peyrard, Martin Josifoski, Valentin Hartmann, Debjit Paul, Jiheng Wei, Frano Rajic