Sciweavers

CCS
2004
ACM

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

14 years 17 days ago
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...
Brant Hashii
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where CCS
Authors Brant Hashii
Comments (0)