Generic placeholder image

Recent Advances in Computer Science and Communications

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

DOI: 10.2174/2666255813666201207154230

DownloadDownload PDF Flyer Cite As
A Survey on Formal Verification of Separation Kernels

Article ID: e210322188790 Pages: 19

  • * (Excluding Mailing and Handling)

Abstract

Introduction: In developing safety and security-critical systems, separation kernel acts as a primary foundation, which provides spatial as well as temporal separation. The separation kernel offers highly assured partitions to the applications hosted on the fundamentally critical systems and can also control the flow of information between them. The industries, as well as academia, have developed several separation kernels that have been broadly applied in critical systems like military/defense secured applications, avionics/aerospace intelligent systems, healthcare units that deal with human lives and in many more areas. The increasing popularity of separation kernels demands the formal verification that assures the correctness of the functionalities in it. Further, formal verification of separation kernels has become mandatory by the security/safety certification authorities.

Conclusion: This paper first presents the concept of the separation kernel, and then it discusses the functionalities, design, and properties of it. The classification and analysis of the formal languages are being presented in this paper used for writing the specifications of the separation kernel and verifying it. The paper is an attempt towards the classification of formal languages being used for the verification of several separation kernels.

Keywords: Separation Kernel, Formal Method, Verification, Spatial Separation, Temporal Separation, Information Control Flow.

[1]
Muen separation kernel http://muen.codelabs.ch/
[2]
"Difference between microkernel and monolithic kernel from tech differences",
[3]
J.M. Rushby, Design and verification of secure systems., p. vol. Vol. 15. ACM, 1981., .
[4]
J. Alves-Foss, P. W. Oman, C. Taylor, and W. S. Harrison, "The mils architecture for high-assurance embedded systems", International journal of embedded systems. vol. 2 , no. 3-4 , pp. 239 -247 , 2006.
[5]
D.E. Denning, "A lattice model of secure information flow", Commun. ACM, vol. 19, no. 5, pp. 236-243, 1976.
[http://dx.doi.org/10.1145/360051.360056]
[6]
W. W. H. Been, Mils: Architecture for high-assurance embedded computing.
[7]
R. Collins, Protection profile for partitioning kernels in environments requiring augmented high robustness.
[8]
J. McLean, and C. Heitmeyer, NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYS-TEMS., High assurance computer systems: A research agenda, Tech. rep., CHACS, 1995.
[http://dx.doi.org/10.21236/ADA465571]
[9]
J. Rushby, "Critical system properties: Survey and taxonomy", Reliab. Eng. Syst. Saf., vol. 43, no. 2, pp. 189-219, 1994.
[http://dx.doi.org/10.1016/0951-8320(94)90065-5]
[10]
J. Rushby, Partitioning in avionics architectures: Requirements, mechanisms, and assurance, Tech. rep., SRI INTERNATIONAL MENLO PARK CA COMPUTER SCIENCE LAB, 2000.
[11]
S. R. Ames Jr, M. Gasser, and R. R. Schell, Security kernel design and implementation: An introduction.
[12]
B. Leiner, M. Schlager, R. Obermaisser, and B. Huber, "A comparison of partitioning operating systems for integrated systems", International Conference on Computer Safety, Reliability, and Security, pp. 342-355, 2007.
[http://dx.doi.org/10.1007/978-3-540-75101-4_33]
[13]
P.A. Karger, "Multi-level security requirements for hypervisors", Computer Security Applications Conference, 21st Annual, p. 2005p. 9, .
[http://dx.doi.org/10.1109/CSAC.2005.41]
[14]
R. Sailer, T. Jaeger, E. Valdez, R. Caceres, R. Perez, S. Berger, J.L. Griffin, and L. Van Doorn, Building a mac-based security architecture for the xen open-source hypervisor.
[http://dx.doi.org/10.1109/CSAC.2005.13]
[15]
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.
[16]
"Xtratum", xtratum hypervisor, 2015. http://www.xtratum.org/
[17]
R. West, Y. Li, E. Missimer, and M. Danish, "A virtualized separation kernel for mixed-criticality systems", ACM Trans. Comput. Syst., vol. 34, no. 3, p. 8, 2016.
[http://dx.doi.org/10.1145/2935748]
[18]
S.H. VanderLeest, "Arinc 653 hypervisor", Digital Avionics Systems Conference (DASC), p. 5, 2010.
p [http://dx.doi.org/10.1109/DASC.2010.5655298]
[19]
S. Han, and H-W. Jin, "Full virtualization based arinc 653 partitioning", Digital Avionics Systems Conference (DASC). 2011p. 7E1–1
[20]
S.H. VanderLeest, D. Greve, and P. Skentzos, "A safe secure arinc 653 hypervisor", Digital Avionics Systems Conference (DASC).
2013p. 7B4–1 [http://dx.doi.org/10.1109/DASC.2013.6712638]
[21]
A. Specification, "653-2: Avionics application software standard interface: Part 1-required", servicesTech. rep., Technical report, Avionics Electronic Engineering Committee.. ARINC, 2006
[22]
J. Woodcock, P. G. Larsen, J. Bicarregui, and J. Fitzgerald, "Formal methods: Practice and experience", ACM computing surveys (CSUR). vol. 41 , no. 4 , p. 19 , 2009.
[23]
M. Manderscheid, G. Weiss, and R. Knorr, "Verification of network end-to-end latencies for adaptive ethernet-based cyber-physical systems", J. Systems Archit., vol. 88, pp. 23-32, 2018.
[http://dx.doi.org/10.1016/j.sysarc.2018.05.004]
[24]
I. Grobelna, "Model checking of reconfigurable fpga modules specified by petri nets", J. Systems Archit., vol. 89, pp. 1-9, 2018.
[http://dx.doi.org/10.1016/j.sysarc.2018.06.005]
[25]
B. Chen, X. Li, and X. Zhou, "Model checking of marte/ccsl time behaviors using timed i/o automata", Journal of Systems Architecture.
[26]
A.S. Fathabadi, M.J. Butler, S. Yang, L.A. Maeda-Nunez, J. Bantock, B.M. Al-Hashimi, and G.V. Merrett, "A model-based framework for software portability and verification in embedded power management systems", J. Systems Archit., vol. 82, pp. 12-23, 2018.
[http://dx.doi.org/10.1016/j.sysarc.2017.12.001]
[27]
L.A. Johnson, "Do-178b, software considerations in airborne systems and equipment certification", Crosstalk, no. October, p. 199, .
[28]
P. K. Infrastructure, and T. P. Profile, "Profile, Common criteria for information technology security evaluation", National Security Agency.
[29]
I. Directorate, Protection profile for separation kernels in environments requiring high robustness US Government.
[30]
B. Lampson, M. Abadi, M. Burrows, and E. Wobber, "Authentication in distributed systems: Theory and practice", ACM Trans. Comput. Syst., vol. 10, no. 4, pp. 265-310, 1992.
[http://dx.doi.org/10.1145/138873.138874]
[31]
R. Buerki, and A.-K. Rueegsegger, Muen-an x86/64 separation kernel for high assurance, University of Applied Sciences Rapperswil (HSR) Tech. Rep..
[32]
S. Brien, The development of z.Semantics of Specification Languages (SoSL)., Springer, 1994, pp. 1-14.
[http://dx.doi.org/10.1007/978-1-4471-3229-5_1]
[33]
J. R. Abrial, Data semantics, Universit´e scientifique et m´edicale.
[34]
J.M. Spivey, "An introduction to z and formal specifications", Softw. Eng. J., vol. 4, no. 1, pp. 40-50, 1989.
[http://dx.doi.org/10.1049/sej.1989.0006]
[35]
I.D. Craig, "Formal Refinement for Operating System Kernels",
[36]
K. A. L. Below, formal refinement for operating system kernels..
[37]
A. Velykis, and L. Freitas, "Formal modelling of separation kernel components", International Colloquium on Theoretical Aspects of Computing, p. 2010pp. 230-244, .
[38]
A. Velykis, Formal modelling of separation kernels. Master’s thesis Department of Computer Science, University of York, .
[39]
C. Jones, P. O’Hearn, and J. Woodcock, "Verified software: A grand challenge", Computer, vol. 39, no. 4, pp. 93-95, 2006.
[http://dx.doi.org/10.1109/MC.2006.145]
[40]
J-R. Abrial, and J-R. Abrial, The B-book: assigning programs to meanings., Cambridge University Press, 2005.
[41]
"Paris mtro line 14", wikipedia, the free encyclopedia",
[42]
A. Passos, J.M. Faria, and S.M. de Sousa, Critical SoftwareAssessing the formal development of a secure partitioning kernel with the b method., ADCSS, 2009.
[43]
M. Leuschel, and M. Butler, "Prob: A model checker for b", International Symposium of Formal Methods Europe, pp. 855-874, 2003.
[44]
Y. Zhao, Formal specification and verification of separation kernels: An overview.
[45]
K. Kawamorita, R. Kasahara, Y. Mochizuki, and K. Noguchi, "Application of formal methods for designing a separation kernel for embedded systems", World Acad. Sci. Eng. Technol., no. 68, pp. 506-514, 2010.
[46]
D. Jackson, Software abstractions-logic, language, and analysis evised edition The MIT Press, ..
[47]
A.M. Sloane, "Software abstractions: Logic, language, and analysis by jackson daniel, the mit press, 2006, 366pp, isbn 978-0262101141", J. Funct. Program., vol. 19, no. 2, pp. 253-254, 2009.
[http://dx.doi.org/10.1017/S0956796808006977]
[48]
D. Phelps, M. Auguston, and T.E. Levin, Formal models of a least privilege separation kernel alloy, Tech. rep., NAVAL POSTGRADUATE SCHOOL MONTEREY CA, 2008.
[49]
M. Archer, and C. Heitmeyer, Tame: A specialized specification and verification system for timed automata, Tech. rep., NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS., CHACS, 1996.
[50]
C.L. Heitmeyer, M. Archer, E.I. Leonard, and J. McLean, "Formal specification and verification of data separation in a separation kernel for an embedded system", Proceedings of the 13th ACM conference on Computer and communications security, pp. 346-355, 2006.
[http://dx.doi.org/10.1145/1180405.1180448]
[51]
C. Heitmeyer, M. Archer, E. Leonard, and J. McLean, "Applying formal methods to a certifiably secure software system", IEEE Trans. Softw. Eng., vol. 34, no. 1, pp. 82-98, 2008.
[http://dx.doi.org/10.1109/TSE.2007.70772]
[52]
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", Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, pp. 207-220, 2009.
[http://dx.doi.org/10.1145/1629575.1629596]
[53]
"sel4: formal verification of an operating system kernel", Communica tionsoftheAcm. vol. 53 , no. 6 , pp. 107 -115 , 2010.
[54]
R. Gu, J. Koenig, T. Ramananandro, Z. Shao, X.N. Wu, S-C. Weng, H. Zhang, and Y. Guo, Deep specifications and certified abstraction layers.ACM SIGPLAN Notices., vol., vol. Vol. 50. ACM, 2015, pp. 595-608.
[55]
D. Costanzo, Z. Shao, and R. Gu, "End-to-end verification of information-flow security for c and assembly programs", ACM SIGPLAN Not., vol. 51, no. 6, pp. 648-664, 2016.
[http://dx.doi.org/10.1145/2980983.2908100]
[56]
M. Kaufmann, P. Manolios, and J.S. Moore, Computer-aided reasoning: ACL2 case studies., vol., vol. Vol. 4. Springer Science & Business Media, 2013.
[57]
J. Alves-Foss, B. Rinker, M. Benke, and J. Marshall, "Formal modelling of security policies for multi-partition systems", Tech. rep, 2002.
[58]
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]
[59]
D. Greve, M. Wilding, and W.M. Vanfleet, "A separation kernel formal security policy", Proc. Fourth International Workshop on the ACL2 Theorem Prover and Its Applications, Citeseer, 2003.
[60]
D.S. Hardin, Design and Verification of Microprocessor Systems for High-Assurance Applications., vol., vol. Vol. 15. Springer, 2010.
[http://dx.doi.org/10.1007/978-1-4419-1539-9]
[61]
D. Greve, R. Richards, and M. Wilding, "A summary of intrinsic partitioning verification", 5th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2004),. 2004 Austin, TX
[62]
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 HighAssurance Applications., Springer, 2010, pp. 175-191.
[http://dx.doi.org/10.1007/978-1-4419-1539-9_6]
[63]
T. Nipkow, L.C. Paulson, and M. Wenzel, Isabelle/HOL: a proof assistant for higher-order logic., vol., vol. Vol. 2283. Springer Science & Business Media, 2002.
[http://dx.doi.org/10.1007/3-540-45949-9]
[64]
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 kernel", NASA Formal Methods Symposium, pp. 375-389, 2015.
[http://dx.doi.org/10.1007/978-3-319-17524-9_26]
[65]
R. G. J. K. T. Ramananandro, Z. Shao, N. W. S.-C. W. Haozhong, and Z. Y. Guo, Deep specifications and certified abstraction layers..
[66]
R. Kaiser, and S. Wagner, "Evolution of the pikeos microkernel", First International Workshop on Microkernels for Embedded Systems, p. 50, 2007. p
[67]
C. Baumann, B. Beckert, H. Blasum, and T. Bormer, "Formal verification of a microkernel used in dependable software systems", International Conference on Computer Safety, Reliability, and Security, pp. 187-200, 2009.
[http://dx.doi.org/10.1007/978-3-642-04468-7_16]
[68]
C. Baumann, and T. Bormer, "Verifying the pikeos microkernel: First results in the verisoft xt avionics project", Doctoral Symposium on Systems Software Verification (DS SSV09),. 2009p. 20
[69]
C. Baumann, B. Beckert, H. Blasum, and T. Bormer, "Better avionics software reliability by code verification", Proceedings, embedded world Conference. 2009 Nuremberg, Germany, Citeseer
[70]
C. Baumann, T. Bormer, H. Blasum, and S. Tverdyshev, “Proving memory separation in a microkernel by code level verification”, Object/Component/Service-Oriented Real-Time Distributed Computing Workshops., ISORCW, 2011, pp. 25-32.
[http://dx.doi.org/10.1109/ISORCW.2011.14]
[71]
S. Tverdyshev, "Extending the gwv security policy and its modular application to a separation kernel", NASA Formal Methods Symposium, pp. 391-405, 2011.
[http://dx.doi.org/10.1007/978-3-642-20398-5_28]
[72]
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., Security and Privacy (SP),: SP, 2013, pp. 415-429.
[73]
T. Murray, D. Matichuk, M. Brassil, P. Gammie, and G. Klein, "Noninterference for operating system kernels", International Conference on Certified Programs and Proofs, pp. 126-142, 2012.
[http://dx.doi.org/10.1007/978-3-642-35308-6_12]
[74]
D. Von Oheimb, "Information flow control revisited: Noninfluence= noninterference+ nonleakage", European Symposium on Research in Computer Security, pp. 225-243, 2004.
[http://dx.doi.org/10.1007/978-3-540-30108-0_14]
[75]
A. Crespo, I. Ripoll, and M. Masmano, "Partitioned embedded architecture based on hypervisor: The xtratum approach", Dependable Computing Conference (EDCC), pp. 67-72, 2010.
[76]
G. Heiser, "The role of virtualization in embedded systems", Proceedings of the 1st workshop on Isolation and integration in embedded systems, pp. 11-16, 2008.
[http://dx.doi.org/10.1145/1435458.1435461]
[77]
J. McDermott, B. Montrose, M. Li, J. Kirby, and M. Kang, "Separation virtual machine monitors", Proceedings of the 28th Annual Computer Security Applications Conference, pp. 419-428, 2012.
[78]
G. Barthe, G. Betarte, J.D. Campo, and C. Luna, "Formally verifying isolation and availability in an idealized model of virtualization", International Symposium on Formal Methods, pp. 231-245, 2011.
[http://dx.doi.org/10.1007/978-3-642-21437-0_19]
[79]
K. Slind, and M. Norrish, "A brief overview of hol4", International Conference on Theorem Proving in Higher Order Logics, pp. 28-32, 2008.
[http://dx.doi.org/10.1007/978-3-540-71067-7_6]
[80]
M. Dam, R. Guanciale, N. Khakpour, H. Nemati, and O. Schwarz, "Formal verification of information flow security for a simple arm-based separation kernel", Proceedings of the 2013 ACM SIGSAC conference on Computer communications security, pp. 223-234, 2013.
[http://dx.doi.org/10.1145/2508859.2516702]
[81]
The coq development team, 1989 https://en.wikipedia.org/wiki/Coq, coq.inria.fr
[82]
Promela manual (extracted from spin manual) http://spinroot.com/spin/Man/Manual.html
[83]
J. Penix, W. Visser, E. Engstrom, A. Larson, and N. Weininger, "Verification of time partitioning in the deos scheduler kernel", Proceedings of the 22nd international conference on Software engineering, pp. 488-497, 2000.
[http://dx.doi.org/10.1145/337180.337364]
[84]
J. Penix, W. Visser, S. Park, C. Pasareanu, E. Engstrom, A. Larson, and N. Weininger, "Verifying time partitioning in the deos scheduling kernel", Form. Methods Syst. Des., vol. 26, no. 2, pp. 103-135, 2005.
[http://dx.doi.org/10.1007/s10703-005-1490-4]
[85]
V. Ha, M. Rangarajan, D. Cofer, H. Rues, and B. Dutertre, "Feature-based decomposition of inductive proofs applied to real-time avionics software: An experience report", Proceedings of the 26th International Conference on Software Engineering, pp. 304-313, 2004.
[86]
D. Cofer, and M. Rangarajan, "Formal modeling and analysis of advanced scheduling features in an avionics rtos", International Workshop on Embedded Software, pp. 138-152, 2002.
[http://dx.doi.org/10.1007/3-540-45828-X_11]
[87]
J.C. Woodcock, and C. Morgan, "Refinement of state-based concurrent systems", International Symposium of VDM Europe. 1990pp. 340-351
[88]
G. Nuka, and J. Woodcock, "Mechanising the alphabetised relational calculus", Electron. Notes Theor. Comput. Sci., vol. 95, pp. 209-225, 2004.
[http://dx.doi.org/10.1016/j.entcs.2004.04.013]
[89]
J. S. UJ, The z notation: A reference manual.
[90]
C.A. Hoare, "Communicating sequential processes", Commun. ACM, vol. 26, no. 1, pp. 100-106, 1983.
[http://dx.doi.org/10.1145/357980.358021]
[91]
R. Milner, Communication and concurrency. international series in computer science , 1989.
[92]
B. Roscoe, The theory and practice of concurrency.
[93]
E.W. Dijkstra, E.W. Dijkstra, E.W. Dijkstra, E-U. Informaticien, and E.W. Dijkstra, ""A discipline of programming", prentice-hall Englewood Cliffs. vol. 1, 1976
[94]
J. Franklin, S. Chaki, A. Datta, and A. Seshadri, "Scalable parametric verification of secure systems: How to verify reference monitors without worrying about data structure size", 2010 IEEE Symposium on Security and Privacy (SP), pp. 365-379, 2010.
[http://dx.doi.org/10.1109/SP.2010.29]
[95]
J. Franklin, S. Chaki, A. Datta, J.M. McCune, and A. Vasudevan, "Parametric verification of address space separation", International Conference on Principles of Security and Trust, pp. 51-68, 2012.
[http://dx.doi.org/10.1007/978-3-642-28641-4_4]
[96]
J. McDermott, J. Kirby, B. Montrose, T. Johnson, and M. Kang, "Re-engineering xen internals for higherassurance security", Inf. Secur. Tech. Rep., vol. 13, no. 1, pp. 17-24, 2008.
[http://dx.doi.org/10.1016/j.istr.2008.01.001]
[97]
J. McDermott, and L. Freitas, "A formal security policy for xenon", Proceedings of the 6th ACM workshop on Formal methods in security engineering, pp. 43-52, 2008.
[98]
A. Roscoe, J. Woodcock, and L. Wulf, "Non-interference through determinism", European Symposium on Research in Computer Security, pp. 31-53, 1994.
[99]
A.G. Ramirez, J. Schmaltz, F. Verbeek, B. Langenstein, and H. Blasum, "On two models of noninterference: Rushby and greve, wilding, and vanfleet", International Conference on Computer Safety, Reliability, and Security, pp. 246-261, 2014.
[http://dx.doi.org/10.1007/978-3-319-10506-2_17]
[100]
D. San’an, A. Butterfield, and M. Hinchey, "Separation kernel verification: The xtratum case study", Working Conference on Verified Software: Theories, Tools, and Experiments, pp. 133-149, 2014.
[http://dx.doi.org/10.1007/978-3-319-12154-3_9]
[101]
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 kernel.
[102]
Y. Zhao, Z. Yang, D. San’an, and Y. Liu, Event-based formalization of safety-critical operating system standards: An experience report on arinc 653 using event-b.
[103]
W. Martin, P. White, F. Taylor, and A. Goldberg, Formal construction of the mathematically analyzed separation kernel.
[http://dx.doi.org/10.1109/ASE.2000.873658]
[104]
W. Martin, P. White, and F. Taylor, "Creating high confidence in a separation kernel", Autom. Softw. Eng., vol. 9, no. 3, pp. 263-284, 2002.
[http://dx.doi.org/10.1023/A:1016324624000]
[105]
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]
[106]
F. Singhoff, and A. Plantec, Aadl modeling and analysis of hierarchical schedulers.ACM SIGAda Ada Letters., vol., vol. Vol. 27. ACM, 2007, pp. 41-50.
[http://dx.doi.org/10.1145/1315580.1315593]
[107]
A. Zerzelidis, and A.J. Wellings, Getting more flexible scheduling in the rtsj.
[http://dx.doi.org/10.1109/ISORC.2006.38]
[108]
A. Zerzelidis, and A. Wellings, "A framework for flexible scheduling in the rtsj", ACM Trans. Embed. Comput. Syst., vol. 10, no. 1, p. 3, 2010.
[http://dx.doi.org/10.1145/1814539.1814542]
[109]
M. Asberg, P. Pettersson, and T. Nolte, "Modelling, verification and synthesis of two-tier hierarchical fixedpriority preemptive scheduling", Real-Time Systems (ECRTS), p. 2011pp. 172-181, .