Runtime Verification of Linux Kernel Security Module
作者： Ilya Shchepetkov , Denis Efremov
DOI:
关键词:
摘要: The Linux kernel is one of the most important Free/Libre Open Source Software (FLOSS) projects. It installed on billions devices all over world, which process various sensitive, confidential or simply private data. crucial to establish and prove its security properties. This work-in-progress paper presents a method verify for conformance with an abstract policy model written in Event-B specification language. based system call tracing aims at checking that results execution do not lead accesses violate requirements. As basis it, we use additional interface formally proved satisfy requirements model. In order perform checks it reproduce intercepted calls accesses.
arxiv.org
harvard.edu参考文章(14)
Petr N. Devyanin, Alexey V. Khoroshilov, Victor V. Kuliamin, Alexander K. Petrenko, Ilya V. Shchepetkov, Formal Verification of OS Security Model with Alloy and Event-B ABZ 2014 Proceedings of the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z - Volume 8477. pp. 309- 313 ,(2014) , 10.1007/978-3-662-43652-3_30
Jean-Raymond Abrial, Modeling in Event-B: System and Software Engineering ,(2010)
Stefan Hallerstede, Jean-Raymond Abrial, Refinement, Decomposition, and Instantiation of Discrete Models: Application to Event-B Fundamenta Informaticae. ,vol. 77, pp. 1- 28 ,(2007)
Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta, Laurent Voisin, Rodin: an open toolset for modelling and reasoning in Event-B verified software theories tools experiments. ,vol. 12, pp. 447- 466 ,(2010) , 10.1007/S10009-010-0145-Y
Karen Tsirunyan, Vahram Martirosyan, Andrey Tsyvarev, The Spruce System: quality verification of Linux file systems drivers Proceedings of the Spring/Summer Young Researchers’ Colloquium on Software Engineering. ,(2012) , 10.15514/SYRCOSE-2012-6-25
Giorgio Zanin, Luigi Vincenzo Mancini, Towards a formal model for security policies specification and validation in the selinux system Proceedings of the ninth ACM symposium on Access control models and technologies - SACMAT '04. pp. 136- 145 ,(2004) , 10.1145/990036.990059
Joshua D. Guttman, Amy L. Herzog, John D. Ramsdell, Clement W. Skorupka, Verifying information flow goals in security-enhanced Linux Journal of Computer Security. ,vol. 13, pp. 115- 134 ,(2005) , 10.3233/JCS-2005-13105
K. J. Biba, Integrity Considerations for Secure Computer Systems ,(1977)
James Morris, Crispin Cowan, Stephen Smalley, Chris Wright, Greg Kroah-Hartman, Linux Security Modules: General Security Support for the Linux Kernel usenix security symposium. pp. 17- 31 ,(2002)
Antony Edwards, Trent Jaeger, Xiaolan Zhang, Runtime verification of authorization hook placement for the linux security modules framework Proceedings of the 9th ACM conference on Computer and communications security - CCS '02. pp. 225- 234 ,(2002) , 10.1145/586110.586141