Enforcement and validation (at runtime) of various notions of opacity

被引：1
作者：
Yliès Falcone
Hervé Marchand
机构：
[1] UJF-Grenoble 1,
[2] Laboratoire d’Informatique de Grenoble,undefined
[3] INRIA - Rennes Bretagne Atlantique,undefined
来源：
Discrete Event Dynamic Systems | 2015年 / 25卷
关键词：
Opacity; -step opacity; Runtime verification; Runtime enforcement;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
We are interested in the validation of opacity. Opacity models the impossibility for an attacker to retrieve the value of a secret in a system of interest. Roughly speaking, ensuring opacity provides confidentiality of a secret on the system that must not leak to an attacker. More specifically, we study how we can model-check, verify and enforce at system runtime, several levels of opacity. Besides existing notions of opacity, we also introduce K-step strong opacity, a more practical notion of opacity that provides a stronger level of confidentiality.
引用
收藏
页码：531 / 570
页数：39
相关论文
共 36 条
[1]  
Badouel E(2007)Concurrent secrets Discret Event Dyn Syst 17 425-446
[2]  
Bednarczyk M(2008)Opacity generalised to transition systems Int J Inf Secur 7 421-435
[3]  
Borzyszkowski A(2010)Supervisory control for opacity IEEE Trans Autom Control 55 1089-1100
[4]  
Caillaud B(2011)Runtime enforcement monitors: composition, synthesis, and enforcement abilities Form Methods Syst Des 38 223-262
[5]  
Darondeau P(2012)What can you verify and enforce at runtime? STTT 14 349-382
[6]  
Bryans J(2006)Computability classes for enforcement mechanisms ACM Trans Program Lang Syst 28 175-205
[7]  
Koutny M(2008)A brief account of runtime verification J Logic Algebraic Program 78 293-303
[8]  
Mazaré L(2009)Run-time enforcement of nonsafety policies ACM Trans Inf Syst Secur 12 1-41
[9]  
Ryan PYA(2011)Verification of k-step opacity and analysis of its complexity IEEE Trans Autom Sci Eng 8 549-559
[10]  
Dubreil J(2012)Opacity-enforcing supervisory strategies via state estimator constructions IEEE Trans Autom Control 57 1155-1165
1234