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.

• Type: Conference
• Year: 2004
• Where: ISW
• Authors: Ajay Chander, Drew Dean, John C. Mitchell
• Keywords: Assurance Reference Monitor, Computer Science, ISW 2004, Reference Monitor