Sciweavers

Share
ISW
2004
Springer

A Distributed High Assurance Reference Monitor

10 years 1 months ago
A Distributed High Assurance Reference Monitor
Abstract Ajay Chander1 , Drew Dean2 , and John Mitchell3 1 DoCoMo Communications Laboratories USA, San Jose, CA 95110 2 Computer Science Laboratory, SRI International, Menlo Park, CA 94025 3 Computer Science Department, Stanford University, Stanford, CA 94305 We present DHARMA, a distributed high assurance reference monitor that is generated mechanically by the formal methods tool PVS from a verified specification of its key algorithms. DHARMA supports policies that allow delegation of access rights, as well as structured, distributed names. To test DHARMA, we use it as the core reference monitor behind a web server that serves files over SSL connections. Our measurements show that formally verified high assurance access control systems are practical.
Ajay Chander, Drew Dean, John C. Mitchell
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where ISW
Authors Ajay Chander, Drew Dean, John C. Mitchell
Comments (0)
books