Refinement modeling and verification of secure operating systems for communication in digital twins

Abstract

In traditional digital twin communication system testing, we can apply test cases as completely as possible in order to ensure the correctness of the system implementation, and even then, there is no guarantee that the digital twin communication system implementation is completely correct. Formal verification is currently recognized as a method to ensure the correctness of software system for communication in digital twins because it uses rigorous mathematical methods to verify the correctness of systems for communication in digital twins and can effectively help system designers determine whether the system is designed and implemented correctly. In this paper, we use the interactive theorem proving tool Isabelle/HOL to construct the formal model of the X86 architecture, and to model the related assembly instructions. The verification result shows that the system states obtained after the operations of relevant assembly instructions is consistent with the expected states, indicating that the system meets the design expectations.

Keywords

Theorem proving / Isabelle/HOL / Formal verification / System modeling / Correctness verification

References

[1] H. Hamdoun, A. Sagheer, Information security through controlled quantum teleportation networks, Digital Commun. Netw. 6 (4) (2020) 463-470.

[2] K. Sha, T. Yang, W. Wei, S. Davari, A survey of edge computing-based designs for iot security, Digital Commun. Netw. 6 (2) (2020) 195-202.

[3] R. Li, H. Asaeda, J. Li, X. Fu, A distributed authentication and authorization scheme for in-network big data sharing, Digital Commun. Netw. 3 (4) (2017) 226-235.

[4] J. Rauthan, K. Vaisla, Vrs-db: preserve confidentiality of users' data using encryption approach, Digital Commun. Netw. 7 (1) (2021) 62-71.

[5] Y. Wei, M. Peng, Y. Liu, Intent-based networks for 6G: insights and challenges, Digital Commun. Netw. 6 (3) (2020) 270-280.

[6] K. Ray, A. Banerjee, Modeling and verification of service allocation policies for multi-access edge computing using probabilistic model checking, IEEE Trans. Netw. Service Manag. 18 (3) (2021) 3400-3414.

[7] J. Harrison, HOL Light: a tutorial introduction,in:Proceedings of the International Conference on Formal Methods in Computer-Aided Design, Springer, 1996, pp. 265-269.

[8] K. Slind, M. Norrish, A brief overview of HOL4, in: Proceedings of the International Conference on Theorem Proving in Higher Order Logics, Springer, 2008, pp. 28-32.

[9] T. Nipkow, L.C. Paulson, M. Wenzel, Isabelle/HOL:A Proof Assistant for Higher-Order Logic, Springer Verlag, Berlin, 2002.

[10] S. Li, L. Qiao, M. Yang, Memory state verification based on inductive and deductive reasoning, IEEE Trans. Reliab. 70 (3) (2021) 1026-1039.

[11] S. Adhikary, A. Gurung, J. Thakkar, A.B.D. Costa, S. Dey, A. Hazra, P. Dasgupta, Smt-based verification of safety-critical embedded control software, IEEE Embedded Syst. Lett. 13 (3) (2021) 138-141.

[12] G. Klein, J. Andronick, K. Elphinstone, T. Murray, T. Sewell, R. Kolanski, G. Heiser, Comprehensive formal verification of an OS microkernel, ACM Trans. Comput. Syst. 32 (1) (2014) 1-70.

[13] Z. Shao, Certified software, Commun. ACM 53 (12) (2010) 56-66.

[14] E. Alkassar, M.A. Hillebrand, D. Leinenbach, N.W. Schirmer, A. Starostin, The Verisoft approach to systems verification, in: Proceedings of the Working Conference on Verified Software: Theories, Tools, and Experiments, Springer, 2008, pp. 209-224.

[15] B.J. Walker, R.A. Kemmerer, G.J. Popek, Specification and verification of the UCLA Unix security kernel, Commun. ACM 23 (2) (1980) 118-131.

[16] W.R. Bevier, A Verified Operating System Kernel, Ph.D. thesis, The University of Texas at Austin, 1987.

[17] W.R. Bevier, Kit and the short stack, J. Autom. Reasoning 5 (4) (1989) 519-530.

[18] W.R. Bevier, Kit: a study in operating system verification, IEEE Trans. Software Eng. 15 (11) (1989) 1382-1396.

[19] R.S. Boyer, J.S. Moore, A computational logic handbook, Math. Comput. Simulat. 31 (3) (1989) 289.

[20] J. Koenig, Z. Shao,CompCertO: compiling certified open C components,in:Proceedings of the 2021 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’21), ACM, Virtual, Canada, 2021, pp. 1095-1109.

[21] Y. Wang, X. Xu, P. Wilke, Z. Shao, CompCertELF: verified separate compilation of C programs into ELF object files,in:Proceedings of the 2020 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’20), ACM, Chicago, IL, USA, 2020, p. 197, 1-28.

[22] Yale Flint team, URL, http://flint.cs.yale.edu/, 2021. (Accessed 2 June 2021).

[23] A. Stampoulis, Z. Shao, Static and user-extensible proof checking, ACM SIGPLAN Not. 47 (1) (2012) 273-284.

[24] A. Stampoulis, Z. Shao, VeriML: typed computation of logical terms inside a language with effects,in:Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ACM, 2010, pp. 333-344.

[25] H. Barendregt, H. Geuvers, Proof-assistants using dependent type systems, Handb. Autom. Reason. 2 (2001) 1149-1238.

[26] R. Gu, Z. Shao, H. Chen, X.N. Wu, J. Kim, V. Sjöberg, D. Costanzo, CertikOS: an extensible architecture for building certified concurrent OS kernels,in:Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation, USENIX, 2016, pp. 653-669.

[27] R. Gu, Z. Shao, J. Kim, X. Wu, J. Koenig, V. Sjöberg, H. Chen, D. Costanzo, T. Ramananandro, Certified concurrent abstraction layers, ACM SIGPLAN Not. 53(4) (2018) 646-661.

[28] M. Liu, Real-Time certiKOS: Compositional Verification of OS Kernels with Preemptive Scheduling and Temporal Isolation, Ph.D. thesis, Yale University, 2020.

[29] W.R. Bevier, W.A. Hunt, J.S. Moore, W.D. Young, An approach to systems verification, J. Autom. Reasoning 5 (4) (1989) 411-428.

[30] K. Elphinstone, G. Klein, P. Derrin, T. Roscoe, G. Heiser,Towards a practical, verified kernel, in:Proceedings of the 2007 Workshop on Hot Topics in Operating Systems, pp. 20:1-6.

[31] H. Tuch, G. Klein, G. Heiser,OS verification-now, in:Proceedings of the 2005 Workshop on Hot Topics in Operating Systems 2, USENIX, 2005, pp. 1-6.

[32] D. Elkaduwe, G. Klein, K. Elphinstone,Verified protection model of the seL 4 microkernel,in:Proceedings of Working Conference on Verified Software: Theories, Tools, and Experiments, Springer, 2008, pp. 99-114.

[33] G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, et al., seL4: formal verification of an OS kernel,in:Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, ACM, 2009, pp. 207-220.

[34] G. Heiser, G. Klein, T. Murray,Can we prove time protection?, in:Proceedings of the 2019 Workshop on Hot Topics in Operating Systems USENIX, 2019, pp. 23-29.

[35] Q. Ge, Y. Yarom, T. Chothia, G. Heiser, Time protection: the missing OS abstraction,in:Proceedings of the 14th EuroSys Conference, ACM, 2019, pp. 1-17.

[36] T. Sewell, S. Winwood, P. Gammie, T. Murray, J. Andronick, G. Klein seL 4 enforces integrity,in:Proceedings of the International Conference on Interactive Theorem Proving, Springer, 2011, pp. 325-340.

[37] G. Heiser, T. Murray, G. Klein, It's time for trustworthy systems, IEEE Secur. Priv. 10 (2) (2012) 67-70.

[38] B. Blackham, Y. Shi, S. Chattopadhyay, A. Roychoudhury, G. Heiser, Timing analysis of a protected operating system kernel, in: Proceedings of the 32nd IEEE Real-Time Systems Symposium, IEEE, 2011, pp. 339-348.

[39] W. Li, Mathematical Logic: Foundations for Information Science, Springer, Switzerland, Birkhäuser, 2010.

[40] M.O. Rabin, D. Scott, Finite automata and their decision problems, IBM J. Res. Dev. 3 (2) (1959) 114-125.