Analysing Object-Capability Patterns With Mur'
Deian Stefan, John C. Mitchell · 2011
Object Capability (OCap) patternscan be used to enforcethe principle of least authority. However, despite the popularity and promise of OCap patterns, these patterns have not been sufficiently analyzed or verified. We analyze several OCap patterns using the Mur' verification tool and confirm the utility of our model by finding previously known vulnerabilities. Because these vulnerabilities were not repaired in previous studies, we provide new patterns and verify their correctness, within the accuracy of our model. Considering both distributed system and language-based settings that are designedto supportthe OCap model,we showthat somepatterns that are secure in a language context are vulnerablein a distributed systems context. We further demonstrate implementable attacks on the revocable forwarder and sealer/unsealer patterns, using a (distributed) subset of E and provide code illustrating and implementing repairs.