点击次数：
所属单位：计算机科学与技术学院/人工智能学院/软件学院
发表刊物：Comput Secur
摘要：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. © 2019 Elsevier Ltd
ISSN号：0167-4048
是否译文：否
发表时间：2020-01-01
合写作者：Hu, Xinwen,Zhang, Fuyuan
通讯作者：庄毅