.png){kind=icon}
.png){kind=icon}
Return
Verifying Opacity Properties in Security Systems
.png){kind=icon}
OA
AI
DOI：10.1109/TDSC.2022.3155323.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
We delineate a methodology for the specification and verification of flow security properties expressible in the opacity framework. We propose a logic, OpacTL, for straightforwardly expressing such properties in systems that can be modelled as partially observable labelled transition systems. We develop verification techniques for analysing property opacity with respect to observation notions. Adding a probabilistic operator to the specification language enables quantitative analysis and verification. This analysis is implemented as an extension to the PRISM model checker and illustrated via a number of examples. Finally, an alternative approach to quantifying the opacity property based on entropy is sketched.
Keywords:
Security
Computational modeling
Probabilistic logic
Software
Entropy
Switches
Semantics
Opacity
logic
security
verification
Journal
IF:
7.5
Papers:
2.4K
Citations:
9.6K