TY - JOUR AU - Brucker, Achim D. AU - Wolff, Burkhart PY - 2005 DA - 2005// TI - A Verification Approach for Applied System Security JO - International Journal on Software Tools for Technology (STTT) SP - 233 EP - 247 VL - 7 IS - 3 PB - Springer-Verlag CY - Heidelberg KW - verification, security, access control, refinement, POSIX, CVS, Z AB - We present a method for the security analysis of realistic models over off-the-shelf systems and their configuration by formal, machine-checked proofs. The presentation follows a large case study based on a formal security analysis of a CVS-Server architecture. The analysis is based on an abstract architecture (enforcing a role-based access control), which is refined to an implementation architecture (based on the usual discretionary access control provided by the \posix environment). Both architectures serve as a skeleton to formulate access control and confidentiality properties. Both the abstract and the implementation architecture are specified in the language Z. Based on a logical embedding of Z into Isabelle/HOL, we provide formal, machine-checked proofs for consistency properties of the specification, for the correctness of the refinement, and for security properties. SN - 1433-2779 L1 - https://www.brucker.ch/bibliography/download/2005/brucker.ea-verification-2005.pdf UR - https://www.brucker.ch/bibliography/abstract/brucker.ea-verification-2005 UR - https://doi.org/10.1007/s10009-004-0176-3 DO - 10.1007/s10009-004-0176-3 LA - USenglish ID - brucker.ea:verification:2005 ER -