Enforceable Security Policies Revisited

被引:36
作者
Basin, David [1 ]
Juge, Vincent [2 ]
Klaedtke, Felix [1 ]
Zalinescu, Eugen [1 ]
机构
[1] Swiss Fed Inst Technol, Inst Informat Secur, Zurich, Switzerland
[2] MINES ParisTech, Paris, France
关键词
Reliability; Security; Verification; Automata; monitoring; safety properties; security policies; temporal logic; REAL-TIME; MODEL CHECKING; ENFORCEMENT; AUTOMATA; LOGICS;
D O I
10.1145/2487222.2487225
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
We revisit Schneider's work on policy enforcement by execution monitoring. We overcome limitations of Schneider's setting by distinguishing between system actions that are controllable by an enforcement mechanism and those actions that are only observable, that is, the enforcement mechanism sees them but cannot prevent their execution. For this refined setting, we give necessary and sufficient conditions on when a security policy is enforceable. To state these conditions, we generalize the standard notion of safety properties. Our classification of system actions also allows one, for example, to reason about the enforceability of policies that involve timing constraints. Furthermore, for different specification languages, we investigate the decision problem of whether a given policy is enforceable. We provide complexity results and show how to synthesize an enforcement mechanism from an enforceable policy.
引用
收藏
页数:26
相关论文
共 52 条
[1]   DEFINING LIVENESS [J].
ALPERN, B ;
SCHNEIDER, FB .
INFORMATION PROCESSING LETTERS, 1985, 21 (04) :181-185
[2]   A REALLY TEMPORAL LOGIC [J].
ALUR, R ;
HENZINGER, TA .
JOURNAL OF THE ACM, 1994, 41 (01) :181-204
[3]  
ALUR R, 1992, LECT NOTES COMPUT SC, V600, P74, DOI 10.1007/BFb0031988
[4]  
[Anonymous], 2008, P 28 IARCS C FDN SOF, DOI [DOI 10.4230/LIPICS.FSTTCS.2008.1740, 10.4230/LIPIcs.FSTTCS.2008.1740]
[5]  
[Anonymous], 2004, ROLE BASED ACCESS CO
[6]  
Barringer H, 2004, LECT NOTES COMPUT SC, V2937, P44
[7]  
Basin D., 2011, Proceedings of the 2011 Eighteenth International Symposium on Temporal Representation and Reasoning (TIME 2011), P88, DOI 10.1109/TIME.2011.14
[8]  
Basin D, 2012, LECT NOTES COMPUT SC, V7215, P309, DOI 10.1007/978-3-642-28641-4_17
[9]   Monitoring Security Policies with Metric First-order Temporal Logic [J].
Basin, David ;
Klaedtke, Felix ;
Mueller, Samuel .
SACMAT 2010: PROCEEDINGS OF THE 15TH ACM SYMPOSIUM ON ACCESS CONTROL MODELS AND TECHNOLOGIES, 2010, :23-33
[10]  
Basin David., 2007, ASIACCS, P70