Login Register Cart 0
Generic placeholder image

Recent Advances in Computer Science and Communications

Editor-in-Chief

ISSN (Print): 2666-2558
ISSN (Online): 2666-2566

Back
Journal Home About Journal Editorial Board Current Issue Volumes/Issues
Subscribe
General Research Article

Formal Specification and Verification of Data Separation for Muen Separation Kernel

Author(s): Ram C. Bhushan* and Dharmendra K. Yadav

Volume 15, Issue 2, 2022

Published on: 31 August, 2020

Page: [274 - 283] Pages: 10

DOI: 10.2174/2666255813999200831103502

Price: $65

Abstract

Introduction: Integrated mixed-criticality systems are becoming increasingly popular for application-specific systems that need a separation mechanism for available onboard resources and the processors equipped with hardware virtualization, which allows the partitions to physical resources, including processor cores, memory, and I/O devices, among guest Virtual Machines (VMs). For building mixed-criticality computing environment, traditional virtual machine systems are inappropriate because they use hypervisors to schedule separate VMs from physical processor cores. This article discusses the design of an environment for mixed-criticality systems: The Muen, an x86/64 separation kernel for high assurance. The Muen Separation Kernel is an open source microkernel with no run-time errors at the source code level. The Muen separation kernel has been designed precisely to encounter the challenging requirements of high-assurance systems built on the Intel x86/64 platform. Muen is under active development, and none of the kernel properties of it has been verified yet. In this paper, we present a novel work of demonstrating one of the kernel properties formally.

Methods: The CTL used in NuSMV is a first-order modal along with data-depended processes and regular formulas. CTL is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any of which might be an actual path that is realized. This section shows the verification of all the requirements mentioned in section 3. In the NuSMV tool, the command used for confirmation of the formulas written in CTL is checkctlspec -p ”CTL-expression”. The nearest quantifier binds each occurrence of a variable in the scope of the bound variable, which has the same name and the same number of arguments.

Results: Formal methods have been applied to various projects for specification and verification of safety properties. Some of them are the SCOMP , SeaView , LOCK, and Multinet Gateway projects. The TLS was written formally. Several mappings were done between the TLS and the SCOMP code: Informal English language to TLS, TLS to actual code, and TLS to pseudo-code. The authors present an ACL2 model for a generic separation kernel, also known as GWV approach.

Conclusion: We consider the formal verification of data separation property, which is one of the crucial modules to achieve separation functionality. The verification of the data separation manager is carried out on the design level using the NuSMV tool. Furthermore, we present the complete model of the data separation unit along with its code written in the NuSMV modelling language. Finally, we have converted the non-functional requirements into the formal logic, which then has verified the model formally.

Keywords: Formal verification, data separation, separation kernel, muen, model checking, theorem proving.

Graphical Abstract

[1]
J.S. Moore, T.W. Lynch, and M. Kaufmann, "A mechanically checked proof of the amd5k86tm floating-point division program", IEEE Transactions on Computers, vol. 47, no. 9, pp. 913-926, 1998.
[http://dx.doi.org/10.1109/12.713311]
[2]
J. Rushby, "A formally verified algorithm for clock synchronization under a hybrid fault model", In: Proceedings of the thirteenth annual ACM symposium on Principles of Distributed Computing, 1994, pp. 304-313.
[http://dx.doi.org/10.1145/197917.198115]
[3]
J. Jurjens, "Sound methods and effective tools for model-based security engineering with UML", In: Proceedings 27th International Conference Software Engineering, 2005, pp. 322-331.
[4]
C. Meadows, "Analysis of the internet key exchange protocol using the NRL protocol analyzer", In: Proceedings of the 1999 IEEE Symposium on Security and Privacy, 1999, pp. 216-231.
[http://dx.doi.org/10.21236/ADA465466]
[5]
C. Heitmeyer, M. Archer, E. Leonard, and J. McLean, "Applying formal methods to a certifiably secure software system", IEEE Transactions on Software Engineering, vol. 34, no. 1, pp. 82-98, 2008.
[http://dx.doi.org/10.1109/TSE.2007.70772]
[6]
J.M. Rushby, "Design and verification of secure systems", ACM SIGOPS Oper. Syst. Rev., vol. 15, no. 5, pp. 12-21, 1981.
[7]
C. Gehrmann, H. Douglas, and D.K. Nilsson, Are there good reasons for protecting mobile phones with hypervisors?IEEE Consumer Communications & Networking Conference, 2011, pp. 906-911.
[http://dx.doi.org/10.1109/CCNC.2011.5766638]
[8]
J. McDermott, B. Montrose, M. Li, J. Kirby, and M. Kang, "Separation virtual machine monitors", In: Proceedings of the 28th Annual Computer Security Applications Conference, 2012, pp. 419-428.
[9]
R. Sailer, E. Valdez, T. Jaeger, R. Perez, L. Van Doorn, J.L. Griffin, S. Berger, R. Sailer, E. Valdez, and T. Jaeger, "Shype: Secure hypervisor approach to trusted virtualized systems", Techn. Rep, vol. 5, 2005.
[10]
G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, and M. Norrish, "sel4: Formal verification of an OS kernel", In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, 2009, pp. 207-220.
[http://dx.doi.org/10.1145/1629575.1629596]
[11]
D. Leinenbach, and T. Santen, Verifying the microsoft hyper-v hypervisor with VCCInternational Symposium on Formal Methods, 2009, pp. 806-809.
[http://dx.doi.org/10.1007/978-3-642-05089-3_51]
[12]
R. J. Richards, "Modeling and security analysis of a commercial real-time operating system kernel", Design and Verification of Microprocessor Systems for High-Assurance Applications. Springer. 2010, pp. 301-322.
[http://dx.doi.org/10.1007/978-1-4419-1539-9_10]
[13]
R. Buerki, and A. K. Rueegsegger, "Muen-an x86/64 separation kernel for high assurance", University of Applied Sciences Rapperswil (HSR)", Tech. Rep., 2013.
[14]
I. Directorate, "Protection profile for separation kernels in environments requiring high robustness", Tech. Rep.. 2007. US Government.
[15]
W.M. Vanfleet, J.A. Luke, R.W. Beckwith, C. Taylor, B. Calloni, and G. Uchenick, "Mils: Architecture for high-assurance embedded computing", Crosstalk, vol. 18, no. 8, pp. 12-16, 2005.
[16]
C. Adams, "Keeping secrets in integrated avionics", AVIONICS MAGAZINE, vol. 28, no. 3, pp. 24-31, 2004.
[17]
J.P. Anderson, Computer security technology planning studyTech. Rep., vol. 2. 1972.
[18]
X. Bai, Z. Cheng, Z. Duan, and K. Hu, "Formal modeling and verification of smart contracts", In: Proceedings of the 2018 7th International Conference on Software and Computer Applications, 2018, pp. 322-326.
[http://dx.doi.org/10.1145/3185089.3185138]
[19]
S. Cranen, J.F. Groote, J.J. Keiren, F.P. Stappers, E.P. De Vink, W. Wesselink, and T.A. Willemse, An overview of the mcrl2 toolset and its recent advancesInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2013, pp. 199-213.
[http://dx.doi.org/10.1007/978-3-642-36742-7_15]
[20]
I. D. Craig, Formal Refinement for Operating System Kernels. Springer Science & Business Media 2007.
[21]
L. Freitas, and J. McDermott, "Formal methods for security in the xenon hypervisor", Int. J. Softw. Tools Technol. Transf., vol. 13, no. 5, p. 463, 2011.
[http://dx.doi.org/10.1007/s10009-011-0195-9]
[22]
T. Murray, D. Matichuk, M. Brassil, P. Gammie, T. Bourke, S. Seefried, C. Lewis, X. Gao, and G. Klein, "sel4: From general purpose to a proof of information flow enforcement", In: 2013 IEEE Symposium on Security and Privacy, 2013, pp. 415-429.
[23]
D. San’an, A. Butterfield, and M. Hinchey, Separation kernel verification: The xtratum case studyWorking Conference on Verified Software: Theories, Tools, and Experiments, 2014, pp. 133-149.
[http://dx.doi.org/10.1007/978-3-319-12154-3_9]
[24]
M. M. Wilding, D. A. Greve, R. J. Richards, and D. S. Hardin, "Formal verification of partition management for the aamp7g microprocessor", Design and Verification of Microprocessor Systems for High-Assurance Applications. Springer, 2010, pp. 175-191.
[http://dx.doi.org/10.1007/978-1-4419-1539-9_6]
[25]
A. Velykis, and L. Freitas, "Formal modelling of separation kernel components", In: Lecture Notes in Computer Science., Springer Berlin Heidelberg, 2010, pp. 230-244.
[26]
F. Verbeek, S. Tverdyshev, O. Havle, H. Blasum, B. Langenstein, W. Stephan, Y. Nemouchi, A. Feliachi, B. Wolff, and J. Schmaltz, Formal specification of a generic separation kernelArchive of Formal Proofs, vol. 2014. 2014.
[27]
F. Verbeek, O. Havle, J. Schmaltz, S. Tverdyshev, H. Blasum, B. Langenstein, W. Stephan, B. Wolff, and Y. Nemouchi, Formal API specification of the pikeos separation kernelNASA Formal Methods Symposium, 2015, pp. 375-389.
[http://dx.doi.org/10.1007/978-3-319-17524-9_26]
[28]
Y. Zhao, "Formal specification and verification of separation kernels: An overview", ArXiv e-prints, 2015.
[29]
A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri, "Nusmv: A new symbolic model checker", Int. J. Softw. Tools Technol. Transf., vol. 2, no. 4, pp. 410-425, 2000.
[http://dx.doi.org/10.1007/s100090050046]
[30]
"Wikipedia contributors, Computation tree logic", The Free Encyclopedia. 15-May-2021. [Online]. Available from: https://en.wikipedia.org/w/index.php?title=Computation&oldid=1023214953. [Accessed: 16-Sep-2021].
[31]
L.J. Fraim, "Secure office management system: The first commodity application on a trusted system", In: Proceedings of the 1987 Fall Joint Computer Conference on Exploring Technology: Today and Tomorrow, 1987, pp. 421-426.
[32]
T.F. Lunt, D.E. Denning, R.R. Schell, M. Heckman, and W.R. Shockley, "The seaview security model", IEEE Transaction on Software Engineering, vol. 16, no. 6, pp. 593-607, 1990.
[http://dx.doi.org/10.1109/32.55088]
[33]
R.E. Smith, "Cost profile of a highly assured, secure operating system", ACM Transactions on Information and System Security, vol. 4, no. 1, pp. 72-101, 2001.
[http://dx.doi.org/10.1145/383775.383778]
[34]
S. Gerhart, D. Craigen, and T. Ralston, "Case study: Multinet gateway system", IEEE Softw., vol. 11, no. 1, pp. 37-28, 1994.
[http://dx.doi.org/10.1109/MS.1994.1279943]]
[35]
T.V. Benzel, "Analysis of a kemel verification", In: 1984 IEEE Symposium on Security and Privacy, 1984, p. 125.
[36]
J. Alves-Foss, and C. Taylor, "An analysis of the gwv security Policy. In", Fifth International Workshop on the ACL2 Prover and its Applications, 2004. Available from: http://www.cs.utexas.edu/users/moore/acl2/workshop-2004/contrib/alves-foss-taylor/ACL2004-final
[37]
D. Greve, M. Wilding, and W.M. Vanfleet, "A separation kernel formal security policy", In: Proceeding Fourth International Workshop on the ACL2 Theorem Prover and Its Applications, Citeseer, 2003.
[38]
R. Richards, D. Greve, M. Wilding, and W.M. Vanfleet, The common criteria, formal methods and ACL2ACL2 Workshop, 2004.

Rights & Permissions Print Cite
Article Metrics
12
2
© 2024 Bentham Science Publishers | Privacy Policy