Lessons learned using alloy to formally specify MLS-PCA trusted security architecture

In order to solve future Multi Level Security (MLS) problems, we have developed a solution based on the DARPA Polymorphous Computing Architecture (PCA). MLS-PCA uses a novel distributed process-level encryption scheme to provide high assurance separation between different security levels. High level security evaluations of the TCSEC and Common Criteria require formal specification. Further, in order to enhance our understanding of the model and to facilitate a high assurance implementation, we have formally specified the architecture in Alloy. This paper presents our efforts to produce the formal model and what we have learned from it. We found a number of errors and initiated design changes as a result of the modeling effort. Categories and Subject Descriptors D.2.4 [Software/Program Verification]: Assertion checkers, Class invariants, Formal methods, Model checking, Validation; C.2.0 [General]: Security and protection General Terms Security, Verification Keywords Alloy, forma...

• Type: Conference
• Year: 2004
• Where: CCS
• Authors: Brant Hashii
• Keywords: CCS 2004, Formal Specification, Level Security, Security, Security Privacy