• Dec 24, 2021 News!Vol 10, No 1- Vol 10, No 2 has been indexed by IET-(Inspec)   [Click]
  • Aug 27, 2020 News!Welcome Prof. D. P. Sharma from India to join the Editorial board of IJFCC     [Click]
  • Jun 01, 2023 News!Vol.12, No.2 has been published with online version.   [Click]
General Information

Prof. Pascal Lorenz
University of Haute Alsace, France
It is my honor to be the editor-in-chief of IJFCC. The journal publishes good papers in the field of future computer and communication. Hopefully, IJFCC will become a recognized journal among the readers in the filed of future computer and communication.

IJFCC 2021 Vol.10(4): 45-52 ISSN: 2010-3751
DOI: 10.18178/ijfcc.2021.10.4.578

Verification of MILS Partition Scheduling Module Using Layered Methods

Yang Gao, Xia Yang, Wensheng Guo, and Xiutai Lu
Abstract—MILS partition scheduling module ensures isolation of data between different domains completely by enforcing secure strategies. Although small in size, it involves complicated data structures and algorithms that make monolithic verification of the scheduling module difficult using traditional verification logic (e.g., separation logic). In this paper, we simplify the verification task by dividing data representation and data operation into different layers and then to link them together by composing a series of abstraction layers. The layered method also supports function calls from higher implementation layers into lower abstraction layers, allowing us to ignore implementation details in the lower implementation layers. Using this methodology, we have verified a realistic MILS partition scheduling module that can schedule operating systems (Ubuntu 14.04, VxWorks 6.8 and RTEMS 11.0) located in different domains. The entire verification has been mechanized in the Coq Proof Assistant.

Index Terms—MILS, separation kernel, formal methods, layered methodology.

Yang Gao, Xia Yang, Wensheng Guo, and Xiutai Lu are with School of Information and Software Engineering University of Electronic Science and Technology of China, Chengdu, China (e-mail: gyang@std.uestc.edu.cn, xyang@uestc.edu.cn, gws@uestc.edu.cn, 1158829283@qq.com) .


Cite: Yang Gao, Xia Yang, Wensheng Guo, and Xiutai Lu, "Verification of MILS Partition Scheduling Module Using Layered Methods," International Journal of Future Computer and Communication vol. 10, no. 4, pp. 45-52, 2021.

Copyright © 2021 by the authors. This is an open access article distributed under the Creative Commons Attribution License which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited (CC BY 4.0).

Copyright © 2008-2023. International Journal of Future Computer and Communication. All rights reserved.
E-mail: ijfcc@ejournal.net