Semiautomated Verification of Access Control Implementation in Industrial Networked Systems

被引:15
作者
Cheminod, Manuel [1 ]
Durante, Luca [1 ]
Seno, Lucia [1 ]
Valenzano, Adriano [1 ]
机构
[1] CNR, Natl Res Council Italy, Ist Elettron & Ingn Informaz & Telecomun, I-10129 Turin, Italy
关键词
Access control policies; automated verification; industrial system security; role-based access control (RBAC); CONTROL POLICIES; BUILDING AUTOMATION; SECURITY ANALYSIS; MANAGEMENT; MODELS;
D O I
10.1109/TII.2015.2489181
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
Access control is a necessary building block in the security of any kind of cyber system and, in this sense, industrial networked systems (INSs) make no exception. Typically, access control policies are specified at a high implementation-independent level of abstraction and then mapped onto the real system by leveraging available policy enforcement mechanisms. Unfortunately, different from general-purpose ICT systems, enforcement mechanisms are generally very basic in INS. As a consequence, verifying the correctness of policy implementation becomes a crucial task, especially cumbersome when it needs to be carried out entirely by hand. This paper presents a new methodology, which also serves as the basis of a purposely developed software tool conceived to cope with the lack of policy enforcement mechanisms in INS and to allow semiautomatic verification of policy implementation. Our approach is based on a twofold system model that enables both the abstract specification of access control policies and the detailed description of the target physical system. These two separate views are then combined to automatically determine whether the current system implementation matches the policy specification.
引用
收藏
页码:1388 / 1399
页数:12
相关论文
共 44 条
[1]  
Alberti F., 2011, P 6 ACM S INF COMP C, P165
[2]  
[Anonymous], P 10 IEEE INT S IND
[3]  
[Anonymous], P 2 ACM WKSP ASS US
[4]  
[Anonymous], 3592012 ANSI INCITS
[5]  
[Anonymous], P 43 IEEE HAW INT C
[6]   Automated analysis of security-design models [J].
Basin, David ;
Clavel, Manuel ;
Doser, Juergen ;
Egea, Marina .
INFORMATION AND SOFTWARE TECHNOLOGY, 2009, 51 (05) :815-831
[7]  
Bengtsson J., 1996, Hybrid Systems III. Verification and Control, P232, DOI 10.1007/BFb0020949
[8]   A twofold model for the analysis of access control policies in industrial networked systems [J].
Bertolotti, Ivan Cibrario ;
Durante, Luca ;
Seno, Lucia ;
Valenzano, Adriano .
COMPUTER STANDARDS & INTERFACES, 2015, 42 :171-181
[9]   A Multidimensional Critical State Analysis for Detecting Intrusions in SCADA Systems [J].
Carcano, A. ;
Coletta, A. ;
Guglielmi, M. ;
Masera, M. ;
Fovino, I. Nai ;
Trombetta, A. .
IEEE TRANSACTIONS ON INDUSTRIAL INFORMATICS, 2011, 7 (02) :179-186
[10]   Verification and enforcement of access control policies [J].
Cau, Antonio ;
Janicke, Helge ;
Moszkowski, Ben .
FORMAL METHODS IN SYSTEM DESIGN, 2013, 43 (03) :450-492