SWS   Info

Public Audience

English

-- Not specified --

Saarbrücken

In scenarios such as web programming, where code is linked
together from multiple sources, object capability patterns
(OCPs) provide an essential safeguard, enabling programmers to
protect the private state of their objects from corruption by
unknown and untrusted code. However, the benefits of OCPs in
terms of security and program verification are barely
understood. Our proposed thesis bridges this gap, advancing
our understanding of the security and functional properties of
OCP-based programs, systems, and programming language
implementations.

Building on the recently developed Iris framework for
separation logic, we propose OCPL, the first formal system for
compositionally specifying and verifying OCPs in a simple but
representative language with closures and mutable state. The
key idea of OCPL is to account for the boundary between
verified and untrusted code by adopting a well-known idea from
the literature on security protocol verification, namely
robust safety. Programs that export only properly wrapped
values to their environment can be proven robustly safe,
meaning that their untrusted environment cannot violate their
internal invariants. Using OCPL, we can give the first
general, compositional, and machine-checked specs for several
commonly-used OCPs—including the dynamic sealing, membrane,
and caretaker patterns—which we can then use to verify robust
safety for representative client code.

A second apsect of our thesis is that separation logic and
robust safety scale to reasoning about the far more
sophisticated OCPs arising in practical systems. We propose to
model the Firefox web browser and its script interpreter,
which uses an automatic security membrane to enforce the web's
same-origin policy. After extending OCPL to account for the
browser and the membrane-aware scripts it interprets, we can
formalize how, under certain trust assumptions, Firefox
supports the illusion (critical to most script authors) of
“normal object reasoning” for membrane-unaware scripts.

The final element in our thesis is that robust safety and
separation logic ease the burden of developing certified
programming language implementations. To benefit from OCPs, a
programmer must choose a language implementation that
preserves the functional and security properties of her
capability-wrapped code. We propose to develop a correct and
secure compiler (targeting WebAssembly, an interesting new
language for running low-level code in web browsers) based on
the ideas of preserving OCPL specifications and robust safety.
This is meaningful because a compiler focused on such concrete
goals is easier to certify and can generate more efficient
code, compared to compilers organized around generic notions
of correctness and security.

--email hidden

Yes

Kaiserslautern

G26

111

passcode not visible

logged in users only