Abstract
The security of operating system is the foundation of information system. There is no recognized answer about how to guarantee the OS security. The accepted and reliable approach is to validate the design and implementation of OS with formal methods of mathematical logic reasoning. In this paper, we propose to use the “lightweight” formal method to describe and design the system. Through the formalization of OS functionality model and security requirements, we can get the description of system functionality design and security requirements on the same domain. We use logical reasoning to verify whether the system functionality design meets the security requirements. If the verification cannot pass, indicating that there are problems in the system functionality design, then we improve the design and implementation, and verify the re-designed functionality again. The verification result shows that the proposed method is feasible.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Software Eng. Methodol. 11(2), 256–290 (2002)
Bill, M.: SELinux: NSA’s Open Source Security Enhanced Linux. O’Reilly Media, Sebastopol (2004)
Qing, X., Zhu, J.: Covet channel analysis on ANSHENG secure operating system. J. Software 15(9), 1385–1392 (2004)
Qing, X.: Covert channel analysis in secure operating systems with high security levels. J. Software 15(12), 1837–1849 (2004)
Walker, B.J., Kemmerer, R.A., Popek, G.J.: Specification and verification of the UCLA Unix security kernel. Commun. ACM 23(2), 118–131 (1980)
SRI International. http://www.sri.com. Accessed 31 Oct 2017
Bevier, W.R.: A verified operating system kernel. Ph.D. thesis. University of Texas at Austin (1987)
Hohmuth, M., Tews, H., Stephens, S.G.: Applying source-code verification to a microkernel: the VFiasco project. In: 10th Workshop on ACM SIGOPS European Workshop, pp. 165–169. ACM, New York (2002)
Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55602-8_217
Tews, H.: Microhypervisor Verification: Possible Approaches and Relevant Properties. In: Nluug Voorjaarsconferentie 2007, pp. 96–109. Nluug Voorjaarsconferentie, Nijmegen (2007)
Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol. 6989, pp. 12–27. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24364-6_2
Heiser, G., Elphinstone, K.: L4 microkernels: the lessons from 20 years of research and deployment. ACM Trans. Comput. Syst. 34(1), 1–29 (2016)
Klein, G., Andronick, J., Elphinstone, K., Murray, T., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32(1), 1–70 (2014)
Alkassar, E., Hillebrand, Mark A., Leinenbach, D., Schirmer, Norbert W., Starostin, A.: The verisoft approach to systems verification. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 209–224. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-87873-5_18
Alkassar, E., Cohen, E., Hillebrand, M., Kovalev, M., Paul, W.J.: Verifying shadow page table algorithms. In: 2010 Conference on Formal Methods in Computer-Aided Design, pp. 267–270. IEEE, Switzerland (2010)
Alkassar, E., Cohen, E., Hillebrand, M., Pentchev, H.: Modular specification and verification of interprocess communication. In: 2010 Conference on Formal Methods in Computer-Aided Design, pp. 167–174. IEEE, Switzerland (2010)
Flint Team. http://flint.cs.yale.edu/ Accessed 31 Oct 2017
Stampoulis, A.: VeriML: a dependently-typed, user-extensible, and language-centric approach to proof assistant. Ph.D. thesis. Yale University (2012)
Gu, R., Shao, Z., Chen, H., Wu, X., Kim, J., Sjöberg, V., Costanzo, D.: CertiKOS: an extenisble architecture for building certified concurrent OS kernels. In: 2016 USENIX Symposium on Operating Systems Design and Implementation, pp. 653–669. USENIX Association, Savannah (2016)
Chen, H., Wu, X., Shao, Z., Lockerman, J., Gu, R.: Toward compositional verification of interruptible os kernels and device drivers. In: 2016 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 431–447. ACM, Santa Barbara (2016)
Costanzo, D., Shao, Z., Gu, R.: End-to-end verification of information-flow security for C and Assembly Programs. In: 2016 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 648–664. ACM, Santa Barbara (2016)
Acknowledgment
This work is supported by the Natural Science Foundation of China under grant No. 61402057, the Natural Science Foundation of Jiangsu Province in China under grant No. BK20140418, the Qing Lan Project of Jiangsu Province in China under grant No. 2017, and Science and Technology Project of State Grid Corporation in China (Research on Key Techniques of Trusted Root and Trust Chain Construction in Power Cloud Platform).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Qian, Z. et al. (2018). Research on Formal Design and Verification of Operating Systems. In: Bi, Y., Chen, G., Deng, Q., Wang, Y. (eds) Embedded Systems Technology. ESTC 2017. Communications in Computer and Information Science, vol 857. Springer, Singapore. https://doi.org/10.1007/978-981-13-1026-3_6
Download citation
DOI: https://doi.org/10.1007/978-981-13-1026-3_6
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-13-1025-6
Online ISBN: 978-981-13-1026-3
eBook Packages: Computer ScienceComputer Science (R0)
