A survey on formal specification and verification of separation kernels

doi:10.1007/s11704-016-4226-2

Front. Comput. Sci.

2017, Vol. 11

Issue (4) : 585-607 https://doi.org/10.1007/s11704-016-4226-2

REVIEW ARTICLE

A survey on formal specification and verification of separation kernels

Yongwang ZHAO¹(

), Zhibin YANG^1,^2,³, Dianfu MA¹

¹. State Key Laboratory of Software Development Environment (NLSDE), School of Computer Science and Engineering, Beihang Univerisity, Beijing 100191, China
². College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China
³. Collaborative Innovation Center of Novel Software Technology and Industrialization, Nanjing 210016, China

Download: PDF(1329 KB)
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

Abstract

Separation kernels are fundamental software of safety and security-critical systems, which provide their hosted applications with spatial and temporal separation as well as controlled information flows among partitions. The application of separation kernels in critical domain demands the correctness of the kernel by formal verification. To the best of our knowledge, there is no survey paper on this topic. This paper presents an overview of formal specification and verification of separation kernels. We first present the background including the concept of separation kernel and the comparisons among different kernels. Then, we survey the state of the art on this topic since 2000. Finally, we summarize research work by detailed comparison and discussion.

Keywords real-time operating systems separation kernel survey formal specification formal verification

Corresponding Author(s): Yongwang ZHAO

Just Accepted Date: 07 July 2016 Online First Date: 17 March 2017 Issue Date: 26 July 2017

Cite this article:

Yongwang ZHAO,Zhibin YANG,Dianfu MA. A survey on formal specification and verification of separation kernels[J]. Front. Comput. Sci., 2017, 11(4): 585-607.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-016-4226-2
https://academic.hep.com.cn/fcs/EN/Y2017/V11/I4/585

1	RushbyJ. Design and verification of secure systems. ACM SIGOPS Operating Systems Review, 1981, 15(5): 12–21 https://doi.org/10.1145/1067627.806586
2	Alves-FossJ, OmanP W, TaylorC, Harrison W S. The MILS architecture for high-assurance embedded systems. International journal of embedded systems, 2006, 2(3-4): 239–247 https://doi.org/10.1504/IJES.2006.014859
3	DenningD E. A lattice model of secure information flow. Communications of the ACM, 1976, 19(5): 236–243 https://doi.org/10.1145/360051.360056
4	GjertsenT, Nordbotten N A. Multiple independent levels of security (MILS) — a high assurance architecture for handling information of different classification levels. Technical Report. 2008
5	ARINC Airlines Electronic Engineering Committee. ARINC 653 – avionics application software standard interface. 2003
6	Wind river VxWorks MILS platform. Technical Report, 2013
7	Green Hills Software, Inc. Safety-critical products: Integrity-178b real-time operationg system. Technical Report. 2005
8	LynuxWorks, Inc. Lynxsecure: software security driven by an embedded hypervisor. Technical Report. 2012
9	LynuxWorks, Inc. Lynxos-se: time- and space-partitioned RTOS with open-standards apis. Technical Report. 2008
10	RobertK, Stephan W. The pikeos concept —history and design. Technical Report. 2007
11	DelangeJ, LecL. Pok, an ARINC 653-compliant operating system released under the BSD license. In: Proceedings of the 13th Real-Time Linux Workshop. 2011
12	MasmanoM, RipollI, CrespoA, Metge J. Xtratum: a hypervisor for safety critical embedded systems. In: Proceedings of the 11th Real- Time Linux Workshop. 2009
13	WoodcockJ, LarsenPG, BicarreguiJ , FitzgeraldJ. Formal methods: practice and experience. ACM Computing Surveys, 2009, 41(4): 1729–1739 https://doi.org/10.1145/1592434.1592436
14	National Security Agency. Common criteria for information technology security evaluation. 3.1 r4 edition, 2012
15	National Security Agency. U.S. government protection profile for separation kernels in environments requiring high robustness. Technical Report. 2007
16	Federal Aviation Authority. Software considerations in airborne systems and equipment certification. Technical Report RTCA/DO-178B. RTCA, Inc., 1992
17	Federal Aviation Authority. Software considerations in airborne systems and equipment certification. Technical Report RTCA/DO-178C. RTCA, Inc., 2011
18	WildingM M, GreveD A, RichardsR J , HardinD S. Formal verification of partition management for the AAMP7G microprocessor. In: Hardin D S, eds. Design and Verification of Microprocessor Systems for High-Assurance Applications. Berlin: Springer, 2010, 175–191 https://doi.org/10.1007/978-1-4419-1539-9_6
19	BaumannC, Beckert B, BlasumH , BormerT. Formal verification of a microkernel used in dependable software systems. In: Buth B, Rade G, Seyfarth T, eds. Computer Safety, Reliability, and Security. Berlin: Springer, 2009, 187–200 https://doi.org/10.1007/978-3-642-04468-7_16
20	BaumannC, BormerT. Verifying the PikeOS microkernel: first results in the Verisoft XT avionics project. In: Proceedings of Doctoral Symposium on Systems Software Verification.2009
21	BaumannC, Beckert B, BlasumH , BormerT. Ingredients of operating system correctness (lessons learned in the formal verification of PikeOS). In: Proceedings of Embedded World Conference. 2010
22	BaumannC, BormerT, BlasumH, Tverdyshev S. Proving memory separation in a microkernel by code level verification. In: Proceedings of the 14th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing Workshops. 2011, 25–32 https://doi.org/10.1109/isorcw.2011.14
23	RichardsR J. Modeling and security analysis of a commercial real-time operating system kernel. In: Hardin D S, eds. Design and Verification of Microprocessor Systems for High-Assurance Applications. Berlin: Springer, 2010, 301–322 https://doi.org/10.1007/978-1-4419-1539-9_10
24	HeitmeyerC L, ArcherM, LeonardE I, McLean J. Formal specification and verification of data separation in a separation kernel for an embedded system. In: Proceedings of the 13th ACM Conference on Computer and Communications Security. 2006, 346–355 https://doi.org/10.1145/1180405.1180448
25	HeitmeyerC L, ArcherM, LeonardE I, McLean J. Applying formal methods to a certifiably secure software system. IEEE Transactions on Software Engineering, 2008, 34(1): 82–98 https://doi.org/10.1109/TSE.2007.70772
26	PenixJ, VisserW, EngstromE, Larson A, WeiningerN . Verification of time partitioning in the DEOS scheduler kernel. In: Proceedings of the 22nd International Conference on Software Engineering. 2000, 488–497 https://doi.org/10.1145/337180.337364
27	PenixJ, VisserW, ParkS, Pasareanu C, EngstromE , LarsonA, Weininger N. Verifying time partitioning in the DEOS scheduling kernel. Formal Methods in System Design, 2005, 26(2): 103–135 https://doi.org/10.1007/s10703-005-1490-4
28	HaV, Rangarajan M, CoferD , RuesH, and Dutertre B. Feature-based decomposition of inductive proofs applied to real-time avionics software: an experience report. In: Proceedings of the 26th International Conference on Software Engineering. 2004, 304–313
29	BulkeleyW. Crash-proof code. MIT Technology Review, 2011, 114(3): 53–54
30	KleinG, Elphinstone K, HeiserG , AndronickJ, CockD, DerrinP, Elkaduwe D, EngelhardtK , KolanskiR, Norrish M, SewellT , TuchH, Winwood S. seL4: formal verification of an OS kernel. In: Proceedings of the 22nd ACM SIGOPS Symposium on Operating Systems Principles. 2009, 207–220 https://doi.org/10.1145/1629575.1629596
31	KleinG, Andronick J, ElphinstoneK , HeiserG, CockD, DerrinP, Elkaduwe D, EngelhardtK , KolanskiR, Norrish M, SewellT , TuchH, Winwood S. seL4: formal verification of an operating-system kernel. Communications of the ACM, 2010, 53(6): 107–115 https://doi.org/10.1145/1743546.1743574
32	KleinG. Operating system verification —an overview. Sadhana, 2009, 34(1): 27–69 https://doi.org/10.1007/s12046-009-0002-4
33	AmesS R, GasserM, SchellR R. Security kernel design and implementation: an introduction. Computer, 1983, 16(7): 14–22 https://doi.org/10.1109/MC.1983.1654439
34	MarkV, William B, BenC , JahnL, CarolT, GordonU. MILS: architecture for high-assurance embedded computing. CrossTalk: The Journal of Defense Software Engineering, 2005, 12–16
35	The Open Group. Protection profile for partitioning kernels in environments requiring augmented high robustness. Technical Report. 2003
36	ParrG R, Edwards R. Integrated modular avionics. Air & Space Europe, 1999, 1(2): 72–75 https://doi.org/10.1016/S1290-0958(99)80018-5
37	LevinT E, IrvineC E, WeissmanC, Nguyen T D. Analysis of three multilevel security architectures. In: Proceedings of the 2007 ACM Workshop on Computer Security Architecture. 2007, 37–46 https://doi.org/10.1145/1314466.1314473
38	RushbyJ. Partitioning in avionics architectures: requirements, mecha nisms, and assurance. Technical Report. 2000
39	LeinerB, Schlager M, ObermaisserR , HuberB. A comparison of partitioning operating systems for integrated systems. In: Proceedings of the 26th International Conference on Computer Safety, Reliability, and Security. 2007, 342–355 https://doi.org/10.1007/978-3-540-75101-4_33
40	RamamrithamK, Stankovic J A. Scheduling algorithms and operating systems support for real-time systems. Proceedings of the IEEE, 1994, 82(1): 55–67 https://doi.org/10.1109/5.259426
41	PopekG J, Goldberg R P. Formal requirements for virtualizable third generation architectures. Communication of ACM, 1974, 17(7): 412–421 https://doi.org/10.1145/361011.361073
42	GoguenJ A, Meseguer J. Security policies and security models. In: Proceedings of IEEE Symposium on Security and Privacy. 1982 https://doi.org/10.1109/sp.1982.10014
43	MartinW, WhiteP, TaylorF S, Goldberg A. Formal construction of the mathematically analyzed separation kernel. In: Proceedings of IEEE International Conference on Automated Software Engineering. 2000, 133–141 https://doi.org/10.1109/ase.2000.873658
44	MartinW B, WhiteP D, TaylorF S. Creating high confidence in a separation kernel. Automated Software Engineering, 2002, 9(3): 263–284 https://doi.org/10.1023/A:1016324624000
45	MurrayT, Matichuk D, BrassilM , GammieP, KleinG. Noninterference for operating system kernels. In: Proceedings of International Conference on Certified Programs and Proofs. 2012, 126–142 https://doi.org/10.1007/978-3-642-35308-6_12
46	GreveD, Wilding M, VaneetW M . A separation kernel formal security policy. In: Proceedings of the ACL2 Workshop. 2003
47	Alves-fossJ, TaylorC. An analysis of the gwv security policy. In: Proceedings of the ACL2 Workshop. 2004
48	Green Hills Software. Integrity-178b separation kernel security target. Technical Report. 2008
49	GreveD, Richards R, WildingM . A summary of intrinsic partitioning verification. In: Proceedings of the ACL2 Workshop. 2004
50	GreveD. Information security modeling and analysis. In: Hardin D S, eds. Design and Verification of Microprocessor Systems for High- Assurance Applications. Berlin: Springer, 2010, 249–299 https://doi.org/10.1007/978-1-4419-1539-9_9
51	RushbyJ. A separation kernel formal security policy in PVS. Technical Report, CSL Technical Note, SRI International. 2004
52	TverdyshevS. Extending the GWV security policy and its modular application to a separation kernel. In: Bobaru M, Havelund K, Holzmann G J, et al. eds. NASA Formal Methods. Berlin: Springer, 2011, 391–405 https://doi.org/10.1007/978-3-642-20398-5_28
53	GreveD, Wilding M, VanfleetW M . High assurance formal security policy modeling. In: Proceedings of the 17th Systems and Software Technology Conference. 2005
54	RushbyJ. Noninterference, transitivity, and channel-control security policies. Technical Report, SRI International, Computer Science Laboratory. 1992
55	OheimbD. Information flow control revisited: noninfluence= noninterference+ nonleakage. In: Proceedings of the 9th European Symposium on Research Computer Security. 2004, 225–243 https://doi.org/10.1007/978-3-540-30108-0_14
56	MantelH, Sabelfeld A. A generic approach to the security of multithreaded programs. In: Proceedings of the 14th IEEE Workshop on Computer Security Foundations. 2001, 126–142
57	MurrayT, Matichuk D, BrassilM , GammieP, BourkeT, SeefriedS, Lewis C, GaoX , KleinG. sel4: from general purpose to a proof of information flow enforcement. In: Proceedings of the 34th IEEE Symposium on Security and Privacy. 2013, 415–429 https://doi.org/10.1109/sp.2013.35
58	RamirezA, Schmaltz J, VerbeekF , LangensteinB, BlasumH. On two models of noninterference: rushby and greve, wilding, and vanfleet. In: Proceedings of the 33rd International Conference on Computer Safety, Reliability, and Security. 2014, 246–261 https://doi.org/10.1007/978-3-319-10506-2_17
59	CraigI. Formal Models of Operating System Kernels. London: Springer, 2006
60	CraigI. Formal Refinement for Operating System Kernels. London: Springer, 2007
61	AbrialJ R, Schuman S, MeyerB . Specification language. In: McKeag R M, Macnaghten A M, eds. On the Construction of Programs. Cambridge: Cambridge University Press, 1980, 343–410
62	VelykisA, Freitas L. Formal modelling of separation kernel components. In: Proceedings of the 7th International Colloquium Conference on Theoretical Aspects of Computing. 2010, 230–244 https://doi.org/10.1007/978-3-642-14808-8_16
63	VelykisA. Formal modelling of separation kernels. Dissertation for the Master Degree. York: University of York, 2009
64	JonesC, O’Hearn P, WoodcockJ . Verified software: a grand challenge. Computer, 2006, 39(4): 93–95 https://doi.org/10.1109/MC.2006.145
65	WoodcockJ, DaviesJ. Using Z: Specification, Refinement, and Proof. Upper Saddle River, NJ: Prentice-Hall, 1996
66	AbrialJ R. The B-Book: Assigning Programs to Meanings. Cambridge: Cambridge University press, 1996 https://doi.org/10.1017/CBO9780511624162
67	AndréP. Assessing the formal development of a secure partitioning kernel with the Bmethod. In: Proceedings of ESAWorkshop on Avionics Data, Control and Software Systems. 2009
68	LeuschelM, ButlerM. ProB: a model checker for B. In: Proceedings of International Symposium of Formal Methods. 2003, 855–874 https://doi.org/10.1007/978-3-540-45236-2_46
69	KawamoritaK, Kasahara R, MochizukiY , NoguchiK. Application of formal methods for designing a separation kernel for embedded systems. World Academy of Science, Engineering and Technology, 2010, 506–514
70	ZhaoY W, YangZ B, SananD, Liu Y. Event-based formalization of safety-critical operating system standards: an experience report on ARINC 653 using Event-B. In: Proceedings of the 26th IEEE International Symposium on Software Reliability Engineering. 2015, 281–292 https://doi.org/10.1109/issre.2015.7381821
71	AbrialJ R, Hallerstede S. Refinement, decomposition, and instantiation of discrete models: application to Event-B. Fundamenta Informaticae, 2007, 77(1-2): 1–28
72	VerbeekF, Schmaltz J, TverdyshevS , HavleO, BlasumH, LangensteinB , StephanW, Feliachi A, NemouchiY , WotffB. Formal specification of a generic separation kernel. Archive of Formal Proofs, 2014
73	VerbeekF, HavleO, SchmaltzJ, Tverdyshev S, BlasumH , LangensteinB, Stephan W, WolffB , NemouchiY. Formal API specification of the PikeOS separation kernel. In: Havelund K, Holzmann G, Joshi R, eds. NASA Formal Methods. Springer, 2015, 375–389 https://doi.org/10.1007/978-3-319-17524-9_26
74	KaiserR, WagnerS. Evolution of the pikeos microkernel. In: Proceedings of the 1st International Workshop on Microkernels for Embedded Systems. 2007
75	BaumannC, Beckert B, BlasumH , BormerT. Better avionics software reliability by code verification? A glance at code verification methodology in the Verisoft XT project. In: Proceedings of Embedded World Conference. 2009
76	DamM, Guanciale R, KhakpourN , NematiH, Schwarz O. Formal verification of information flow security for a simple arm-based separation kernel. In: Proceedings of the ACM SIGSAC Conference on Computer & Communications Security. 2013, 223–234 https://doi.org/10.1145/2508859.2516702
77	ZhaoY, SananD, ZhangF, Liu Y. Reasoning about information flow security of separation kernels with channel-based communication. In: Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2016, 791–810 https://doi.org/10.1007/978-3-662-49674-9_50
78	HeiserG. The role of virtualization in embedded systems. In: Proceedings of the 1st Workshop on Isolation and Integration in Embedded Systems. 2008, 11–16 https://doi.org/10.1145/1435458.1435461
79	McDermottJ, Montrose B, LiM , KirbyJ, KangM. Separation virtual machine monitors. In: Proceedings of the 28th Annual Computer Security Applications Conference. 2012, 419–428 https://doi.org/10.1145/2420950.2421011
80	CrespoA, RipollI, MasmanoM. Partitioned embedded architecture based on hypervisor: the XtratuM approach. In: Proceedings of the 8th European Dependable Computing Conference (EDCC). 2010, 67–72 https://doi.org/10.1109/edcc.2010.18
81	FranklinJ, ChakiS, DattaA, Seshadri A. Scalable parametric verification of secure systems: how to verify reference monitors without worrying about data structure size. In: Proceedings of the 2010 IEEE Symposium on Security and Privacy. 2010, 365–379 https://doi.org/10.1109/SP.2010.29
82	FranklinJ, ChakiS, DattaA, McCune J M, VasudevanA . Parametric verification of address space separation. Lecture Notes in Computer Science. 2012, 7215(1): 51–68 https://doi.org/10.1007/978-3-642-28641-4_4
83	BartheG, Betarte G, CampoJ D , LunaC. Formally verifying isolation and availability in an idealized model of virtualization. In: Proceedings of International Symposium on Formal Methods. 2011, 231–245 https://doi.org/10.1007/978-3-642-21437-0_19
84	McDermottJ, KirbyJ, MontroseB, Johnson T, KangM . Reengineering Xen internals for higher-assurance security. Information Security Technical Report, 2008, 13(1): 17–24 https://doi.org/10.1016/j.istr.2008.01.001
85	McDermottJ, Freitas L. A formal security policy for Xenon. In: Proceedings of the 6th ACM Workshop on Formal Methods in Security Engineering. 2008, 43–52 https://doi.org/10.1145/1456396.1456401
86	RoscoeA, Woodcock J, WulfL . Non-interference through determinism. In: Proceedings of the 3rd European Symposium on Research in Computer Security. 1994, 33–53 https://doi.org/10.1007/3-540-58618-0_55
87	CarnevaliL, LipariG, PinzutiA, Vicario E. A formal approach to design and verification of two-level hierarchical scheduling systems. In: Proceedings of the 16th Ada-Europe International Conference on Reliable Software Technologies. 2011, 118–131 https://doi.org/10.1007/978-3-642-21338-0_9
88	CarnevaliL, Pinzuti A, VicarioE . Compositional verification for hierarchical scheduling of real-time systems. IEEE Transactions on Software Engineering, 2013, 39(5): 638–657 https://doi.org/10.1109/TSE.2012.54
89	AsbergM, Pettersson P, NolteT . Modelling, verification and synthesis of two-tier hierarchical fixed-priority preemptive scheduling. In: Proceedings of the 23rd Euromicro Conference on Real-Time Systems (ECRTS). 2011, 172–181 https://doi.org/10.1109/ecrts.2011.24
90	FersmanE, KrcalP, PetterssonP , WangY. Task automata: schedulability, decidability and undecidability. Information and Computation, 2007, 205(8): 1149–1172 https://doi.org/10.1016/j.ic.2007.01.009
91	SinghoffF, Plantec A. AADL modeling and analysis of hierarchical schedulers. ACM SIGAda Ada Letters, 2007, 27(3): 41–50 https://doi.org/10.1145/1315607.1315593
92	ZerzelidisA, Wellings A. Getting more flexible scheduling in the RTSJ. In: Proceedings of the 9th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing. 2006 https://doi.org/10.1109/isorc.2006.38
93	ZerzelidisA, Wellings A. A framework for flexible scheduling in the RTSJ. ACM Transactions on Embedded Computing Systems, 2010, 10(1): 501–512 https://doi.org/10.1145/1814539.1814542
94	ZerzelidisA, Wellings A. Model-based verification of a framework for flexible scheduling in the real-time specification for Java. In: Proceedings of the 4th International Workshop on Java Technologies for Realtime and Embedded Systems, 2006, 20–29 https://doi.org/10.1145/1167999.1168005
95	Alves-FossJ. Multiple independent levels of security. In: Van Tilborg H C A, Jajodia S, eds. Encyclopedia of Cryptography and Security. Springer US, 2011, 815–818
96	ClarksonM, Schneider F. Hyperproperties. Journal of Computer Security, 2010, 18(6): 1157–1210 https://doi.org/10.3233/JCS-2009-0393
97	ClarksonM R, Finkbeiner B, KoleiniM , MicinskiK K, RabeM N, SánchezC . Temporal logics for hyperproperties. In: Proceedings of International Conference on Principles of Security and Trust. 2014, 265–284 https://doi.org/10.1007/978-3-642-54792-8_15
98	AbrialJ R. Formal methods in industry: achievements, problems, future. In: Proceedings of the 28th International Conference on Software Engineering. 2006, 761–768 https://doi.org/10.1145/1134285.1134406

[1]

FCS-0585-14226-YWZ_suppl_1

Download

[1]	Panthadeep BHATTACHARJEE, Pinaki MITRA. A survey of density based clustering algorithms[J]. Front. Comput. Sci., 2021, 15(1): 151308-.
[2]	Syed Farooq ALI, Muhammad Aamir KHAN, Ahmed Sohail ASLAM. Fingerprint matching, spoof and liveness detection: classification and literature review[J]. Front. Comput. Sci., 2021, 15(1): 151310-.
[3]	Yanhong HUANG,Jifeng HE,Huibiao ZHU,Yongxin ZHAO,Jianqi SHI,Shengchao QIN. Semantic theories of programs with nested interrupts[J]. Front. Comput. Sci., 2015, 9(3): 331-345.
[4]	Van Chan NGO, Jean-Pierre TALPIN, Thierry GAUTIER, Paul Le GUERNIC, Lo?c BESNARD. Formal verification of synchronous data-flow program transformations toward certified compilers[J]. Front Comput Sci, 2013, 7(5): 598-616.
[5]	Zhiyuan LIU, Jun PANG, Chenyi ZHANG. Design and formal verification of a CEM protocol with transparent TTP[J]. Front Comput Sci, 2013, 7(2): 279-297.
[6]	Yuehua DAI, Yi SHI, Yong QI, Jianbao REN, Peijian WANG. Design and verification of a lightweight reliable virtual machine monitor for a many-core architecture[J]. Front Comput Sci, 2013, 7(1): 34-43.
[7]	Shaoying LIU. Pre-post notation is questionable in effectively specifying operations of object-oriented systems[J]. Front Comput Sci Chin, 2011, 5(3): 341-352.
[8]	Mingsong LV, Nan GUAN, Qingxu DENG, Ge YU, Wang Yi, . Static worst-case execution time analysis of the μ C/OS-II real-time kernel[J]. Front. Comput. Sci., 2010, 4(1): 17-27.
[9]	ZHANG Jian, ZHANG Wenhui, ZHAN Naijun, SHEN Yidong, CHEN Haiming, ZHANG Yunquan, WANG Yongji, WU Enhua, WANG Hongan, ZHU Xueyang. Basic research in computer science and software engineering at SKLCS[J]. Front. Comput. Sci., 2008, 2(1): 1-11.
[10]	Sargur N. Srihari, Xuanshen Yang, Gregory R. Ball. Offline Chinese handwriting recognition: an assessment of current technology[J]. Front. Comput. Sci., 2007, 1(2): 137-155.

Viewed

Full text

Abstract

Cited

Shared

Discussed