In object capability systems, attenuating objects give secure access to some, but not all capabilities of another object. One such example, is restricted (DOM) tree access, where an attenuating object allows reading and writing the properties of nodes, but only up to a certain hight in the tree.

We will present a specification of this example, employing the concepts of permission and authority, the concept of domination, in terms of Hoare triples and invariants. We will outline how we can show that execution of unknown code whose access to the tree can only go through attenuating objects is guaranteed not to affect the properties of nodes which are beyond the height of these attenuating objects.