Model Checking Distributed Mandatory Access Control Policies
作者： Perry Alexander , Lee Pike , Peter Loscocco , George Coker
DOI: 10.1145/2785966
关键词: Mandatory access control 、 Computer science 、 Hypervisor 、 Model checking 、 Access control 、 Virtualization 、 Stateful firewall 、 Distributed computing 、 Role-based access control 、 Virtual machine
摘要: This work examines the use of model checking techniques to verify system-level security properties a collection interacting virtual machines. Specifically, we examine how local access control policies implemented in individual machines and hypervisor can be shown satisfy global constraints. The SAL checker is used stateful domains with protected resources MAC attempting needed from other domains. described along verification conditions. need state-space explosion motivated for writing theorems limiting explored. Finally, analysis results are examined complexity.
acm.org
sci-hub.se 参考文章(31)
Vivek Haldar, Michael Franz, Deepak Chandra, Semantic remote attestation: a virtual machine directed approach to trusted computing VM'04 Proceedings of the 3rd conference on Virtual Machine Research And Technology Symposium - Volume 3. pp. 3- 3 ,(2004)
Kathi Fisler, Daniel J. Dougherty, Shriram Krishnamurthi, Timothy Nelson, Christopher Barratt, The margrave tool for firewall analysis usenix large installation systems administration conference. pp. 1- 8 ,(2010)
Karl MacMillan, David Caplan, Frank Mayer, SELinux by Example: Using Security Enhanced Linux (Prentice Hall Open Source Software Development Series) ,(2006)
Reiner Sailer, Trent Jaeger, Xiaolan Zhang, Analyzing integrity protection in the SELinux example policy usenix security symposium. pp. 5- 5 ,(2003)
O. Diekmann, H. Metz, Exploring linear chain trickery for physiologically structured populations CWI quarterly. ,vol. 2, pp. 3- 14 ,(1989)
Alessandro Cimatti, Edmund Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella, NuSMV 2: An OpenSource Tool for Symbolic Model Checking computer aided verification. pp. 359- 364 ,(2002) , 10.1007/3-540-45657-0_29
Dimitar P. Guelev, Mark Ryan, Pierre Yves Schobbens, Model-Checking Access Control Policies international conference on information security. pp. 219- 230 ,(2004) , 10.1007/978-3-540-30144-8_19
N.A. Lynch, M.R. Tuttle, An introduction to input/output automata CWI quarterly. ,vol. 2, pp. 219- 246 ,(1989)
S. Owre, J. M. Rushby, N. Shankar, PVS: A Prototype Verification System conference on automated deduction. pp. 748- 752 ,(1992) , 10.1007/3-540-55602-8_217
Nan Zhang, Mark Ryan, Dimitar P. Guelev, Evaluating access control policies through model checking international conference on information security. ,vol. 3650, pp. 446- 460 ,(2005) , 10.1007/11556992_32