The Application of Model Checking in Validating Information System Software Security

被引：0
作者：
Liu Xin [1 ]
Cai Wandong [1 ]
机构：
[1] Northwestern Polytech Univ, Xian, Peoples R China
来源：
2011 INTERNATIONAL CONFERENCE ON COMPUTERS, COMMUNICATIONS, CONTROL AND AUTOMATION (CCCA 2011), VOL III | 2010年
关键词：
software security; validation; model checking;
D O I：
暂无
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
This paper discusses the effectiveness of model checking in validating information system software security, and give the formal definition for these two properties. A model checking based security policy validation and verification method is proposed to validate the consistency and completeness for security policy. This method can also be used to generate a validation sequence. Finally, we'll discuss our availability and reliability of validation methods:
引用
收藏
页码：448 / 451
页数：4
相关论文
共 50 条
[41]   An overview of model checking practices on verification of PLC software [J].
Tolga Ovatman ;
Atakan Aral ;
Davut Polat ;
Ali Osman Ünver .
Software & Systems Modeling, 2016, 15 :937-960
[42]   Exploiting symmetry when model-checking software [J].
Godefroid, P .
FORMAL METHODS FOR PROTOCOL ENGINEERING AND DISTRIBUTED SYSTEMS, 1999, 28 :257-275
[43]   Deductively Verified Program Models for Software Model Checking [J].
Amilon, Jesper ;
Gurov, Dilian .
LEVERAGING APPLICATIONS OF FORMAL METHOD, VERIFICATION AND VALIDATION: SPECIFICATION AND VERIFICATION, PT III, ISOLA 2024, 2025, 15221 :8-25
[44]   Model Checking Applied to Embedded Software of University Satellite [J].
Alencar, Waldo A. F. ;
Villani, Emilia .
JOURNAL OF CONTROL AUTOMATION AND ELECTRICAL SYSTEMS, 2014, 25 (01) :126-136
[45]   Deductive Verification Based Abstraction for Software Model Checking [J].
Amilon, Jesper ;
Lidstrom, Christian ;
Gurov, DiHan .
LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION. VERIFICATION PRINCIPLES, ISOLA 2022, PT I, 2022, 13701 :7-28
[46]   Formally Analyzing Software Vulnerability Based on Model Checking [J].
Wang Chunlei ;
Huang Minhuan ;
He Ronghui .
NSWCTC 2009: INTERNATIONAL CONFERENCE ON NETWORKS SECURITY, WIRELESS COMMUNICATIONS AND TRUSTED COMPUTING, VOL 1, PROCEEDINGS, 2009, :615-+
[47]   Automatic software model checking via constraint logic [J].
Flanagan, C .
SCIENCE OF COMPUTER PROGRAMMING, 2004, 50 (1-3) :253-270
[48]   Model checking aircraft controller software: a case study [J].
Chen, Zhe ;
Gu, Yi ;
Huang, Zhiqiu ;
Zheng, Jun ;
Liu, Chang ;
Liu, Ziyi .
SOFTWARE-PRACTICE & EXPERIENCE, 2015, 45 (07) :989-1017
[49]   Specification and Generation of Environment for Model Checking of Software Components [J].
Parizek, Pavel ;
Plasil, Frantisek .
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 176 (02) :143-154
[50]   Combining predicate and numeric abstraction for software model checking [J].
Gurfinkel A. ;
Chaki S. .
International Journal on Software Tools for Technology Transfer, 2010, 12 (06) :409-427
12345