The goal of the project is to develop a formally verified design for a multilevel secure, distributed, fault tolerant reference monitor. A reference monitor is a system program which controls access of user processes to sensitive data. The reference monitor checks accesses for compliance with a system security policy, and disallows accesses not in compliance. ORA will develop a design for a reference monitor which is distributed on multiple processors and can tolerate processor and memory faults. The project will define a formal mathematical model of security for the reference monitor. The design will be formal language and verified to satisfy the security model in a verification environment built at ORA called Romulus.
