Mu, C;
Clark, D;
(2022)
Verifying Opacity Properties in Security Systems.
IEEE Transactions on Dependable and Secure Computing
10.1109/TDSC.2022.3155323.
(In press).
Preview |
Text
Verifying_Opacity_Properties_in_Security_Systems.pdf - Accepted Version Download (730kB) | Preview |
Abstract
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.
Type: | Article |
---|---|
Title: | Verifying Opacity Properties in Security Systems |
Open access status: | An open access version is available from UCL Discovery |
DOI: | 10.1109/TDSC.2022.3155323 |
Publisher version: | https://doi.org/10.1109/TDSC.2022.3155323 |
Language: | English |
Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
Keywords: | Security , Computational modeling , Probabilistic logic , Software , Entropy , Switches , Semantics |
UCL classification: | UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science UCL > Provost and Vice Provost Offices > UCL BEAMS UCL |
URI: | https://discovery.ucl.ac.uk/id/eprint/10145402 |



1. | ![]() | 23 |
2. | ![]() | 22 |
3. | ![]() | 17 |
4. | ![]() | 10 |
5. | ![]() | 8 |
6. | ![]() | 8 |
7. | ![]() | 3 |
8. | ![]() | 3 |
9. | ![]() | 3 |
10. | ![]() | 2 |
Archive Staff Only
![]() |
View Item |