A journey into the unknown started when I applied to study computer science, having only read two newspaper articles about computers, and not ever met a person who had seen a computer. The journey prove to be safe and fun: I was inspired by and collaborated with great people, was intrigued by Simula, modules, encapsulation, program verification, invariants, semantics, ownership types, … and many more.

A journey into the unknown starts every day, when our software runs in the open world, in collaboration with third party software of unknown provenance, possibly buggy and potentially malicious. We want this journey to be safe: we entrust our software with our secrets and our assets, and expect it to behave correctly even when the third party software is erroneous or malicious.

As early as the 60s, capabilities were proposed to make such journeys safe. Capabilities give authority for an action: access to a capability is a necessary precondition for a certain effect to take place. Capabilities are unforgeable, can be delegated, duplicated, or revoked. Therefore, for capabilities to provide meaningful guarantees, it is essential to be able to control what capabilities each component of a system can obtain and, therefore, what authority it can yield – thus following the Principle of Least Authority.

In this talk, we will explore the formal reasoning about programs written with object capabilities: How can we specify that a capability is a precondition for a given effect? How can we specify who may hold what capabilities? How can we specify when certain effects will not take place, even in the presence of calls to the third party software? How can we distinguish different third party calls, and guarantee that some of these will not to have certain effects while others may? Finally, we will discuss how we can prove that our code adheres to these specifications.

Speaker Bio

Sophia Drossopoulou studied “Informatik” at the “Technische Universitaet Karlsruhe” (now KIT), where she obtained her PhD and became a lecturer. She then moved to Imperial College London, where she is now a Professor. She has also been Engineering Manager and Software Engineer at Meta, and Visiting Researcher at Microsoft Research. Her research interests are in Programming Language Design Specification, and Implementation, Type Systems, Object Oriented Programming Languages, Concurrency, Module Systems and Separate Compilation, Program Evolution, Type Inference, Program Specification and Verification, Session Types, Ownership Types, Object Capabilities, and Garbage Collection.

She has contributed to the first Ada compiler, the first semantics of Java, proposed object reclassification (which evolved into type-state), formal models and variants for ownership types, introduction of session types into object-oriented languages, the evolution from object-based dynamically typed to class based strongly typed (this evolved into gradual typing), and to the development of the Pony and the Verona programming language.