Talk by Sophia Drossopoulou, (Imperial College London), with Julian Mackay, (Victoria University of Wellington), James Noble, (Victoria University of Wellington) and Susan Eisenbach (Imperial College London)
ABSTRACT:
In today’s complex software, internal, trusted, code is tightly intertwined with external, untrusted, code: External code may call into internal code, and internal code may call out to external code. This tight intertwining introduces a high degree of uncertainty which developers strive to mitigate: They want to prevent the external code from causing certain effects unless it is “entitled” to.
The OCAP (object capabilities) model has proposed means to mitigate this uncertainty: Capabilities are transferable rights to perform one or more operations on a given object. Thus, capabilities enable effects. But even more: Capabilities guard effects: callers can make the effect happen, only if they have access to the corresponding capability. As a result, sharing of capabilities has to be carefully managed.
Our work addresses the specification and verification of code which relies on capabilities as guards.
Our specification language can express that capabilities are necessary (rather than sufficient) conditions for certain effects. To reflect that the guarantees should hold in the presence of internal code calling and being called by external code, we propose bounded two-state invariants, where the notion of the future is bounded by the currently executing method. To define the management of sharing of capabilities, we propose the concept of protected capability which guarantees that access by external objects is controlled by the internal objects. %(thus going further than traditional object capabilities). For the verification: We propose Hoare logic inference rules which allow us to reason about calls to external code (open calls). We also propose inference rules which assert that our modules satisfy our specifications. We prove that a sound Hoare logic augmented by the proposed rules is also sound. We use a motivating example and prove its properties using our logic.