Object capabilities let mutually distrustful principals share
private state without giving up integrity, thus ostensibly making
secure programming easier in the presence of buggy or malicious
code. In practice, however, programmers may use object
capabilities incorrectly, creating subtle security flaws. I aim to
enable verification of programs that use object capabilities. In
this work, I model Firefox's use of object capabilities—which is
quite rich, going beyond "standard" patterns described in the
literature—and develop a program logic to prove integrity
properties.