A security modeling and verification method of embedded software based on Z and MARTE. Issue 88 (January 2020)

• Record Type: Journal Article
• Authors: Hu, Xinwen; Zhuang, Yi; Zhang, Fuyuan
• Is Part Of: Computers & security. Issue 88(2020)
• Publication Date: 2020-01
• Subjects: Embedded software -- Security -- Z, UML/MARTE -- Model Checking; Computer security -- Periodicals; Electronic data processing departments -- Security measures -- Periodicals; 005.805
• DOI: 10.1016/j.cose.2019.101615
• Languages: English
• ISSNs: 0167-4048

Abstract

Abstract: The existing modeling and verification methods for embedded software are insufficient towards the increasingly prominent security requirements. In this paper, aiming at high security requirements of embedded software, a security modeling and verification framework of embedded software based on semi-formal and formal methods is proposed. An extensible security model ZMsec (Z-MARTE security model), which extends Z with elements of MARTE (Modeling and Analysis of Real-Time and Embedded systems) and FSA (Finite State Automata), is presented to describe three dimensions of software: security usecases, static structures and dynamic behaviors. Further on, this paper designs ZMsecTL (ZMsecTemporal Logic) formulas to describe security properties, and proposes ZMCA (ZMsec Model Checking Algorithm), a security model checking algorithm on ZMsec model, to verify security properties in ZMsecTL formulas. In order to provide an intuitive state transition diagram for model checking, a depth-first ZMsecSD (ZMsecState Diagram) generation algorithm is designed. Drawing on the abstract framework, this paper develops a prototype implementation of ZMV (ZMsec Modeling and Verification tool), a tool for ZMsec integrated with modeling and verification phases. We finally discuss an embedded software example with ZMV, which illustrates and validates the security modeling and verification method proposed in this paper.