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) .
[PDF]
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).
