Modeling and verification of security properties for critical infrastructure protection
Article No.: 6, Pages 1 - 5
Abstract
Recently, studies have revealed new security issues in critical infrastructures, emphasizing the need for verification of security properties. Any mechanism to verify the security of such systems should merge the cyber and physical aspects in a unified way. This paper proposes a novel direction using process algebras to model and verify security properties within a cyber-physical system (CPS). Specifically, we adopt the π-calculus to perform security analysis of a representative CPS, an advanced electric smart grid. We present the verification of an information flow security property, non-deducibility, defined in terms of more discriminating behavioral equivalences available in π-calculus compared to other process algebras.
References
[1]
M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. In 4th ACM Conference on Computer and Communications Security, pages 36--47. ACM Press, 1997.
[2]
S. Amin, X. Litrico, S. Sastry, and A. Bayen. Stealthy deception attacks on water SCADA systems. In Proceedings of the 13th ACM international conference on Hybrid systems: computation and control (HSCC'10), pages 161--170. ACM, 2010.
[3]
R. Bakhshi and D. Gurov. Verification of peer-to-peer algorithms: a case study. Electron. Notes Theor. Comput. Sci., 181:35--47, June 2007.
[4]
J. A. Goguen and J. Meseguer. Security policies and security models. In Proc. of the IEEE Symposium on Security and Privacy (SSP'82), pages 195--204. IEEE Computer Society Press, 2002.
[5]
Y. Liu, P. Ning, and M. K. Reiter. False data injection attacks against state estimation in electric power grids. In ACM Transactions on Information Systems Security, volume 14(1), June 2011.
[6]
T. McEvoy and S. Wolthusen. A formal adversary capability model for SCADA environments. In C. Xenakis and S. Wolthusen, editors, Critical Information Infrastructures Security, volume 6712 of Lecture Notes in Computer Science, pages 93--103. Springer Berlin/Heidelberg, 2011.
[7]
R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes i. Information and Computation, 100(1):1--40, 1992.
[8]
A. Platzer. Integrative challenges of cyber-physical systems. In Workshop on Usable Verification, November 2010.
[9]
R. Akella, F. Meng, D. Ditch, B. McMillin and M. Crow. Distributed power balancing for the FREEDM system. In The 1st IEEE International Conference on Smart Grid Communications, pages 7--12, October 2010.
[10]
D. Sangiorgi and D. Walker. The π-Calculus - A Theory of Mobile Processes. Cambridge University Press, 2001.
[11]
D. Sutherland. A model of information. In Proceedings of the 9th National Security Conference., pages 175--183, 1986.
Index Terms
- Modeling and verification of security properties for critical infrastructure protection
Recommendations
RETRACTED ARTICLE: Verification and modeling of IoT time automata for gateway security system
AbstractInternet of Things (IoT) is a multiple heterogeneous network, and its perception layer is often faced with various security threats. As the bridge between the perception layer and the network layer, the IoT gateway should have the security ...
Identifying Security Critical Properties for the Dynamic Verification of a Processor
Asplos'17We present a methodology for identifying security critical properties for use in the dynamic verification of a processor. Such verification has been shown to be an effective way to prevent exploits of vulnerabilities in the processor, given a meaningful ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2013
282 pages
ISBN:9781450316873
DOI:10.1145/2459976
Copyright © 2013 Authors.
Sponsors
- Los Alamos National Labs: Los Alamos National Labs
- Sandia National Labs: Sandia National Laboratories
- DOE: Department of Energy
- Oak Ridge National Laboratory
- Lawrence Livermore National Lab.: Lawrence Livermore National Laboratory
- BERKELEYLAB: Lawrence National Berkeley Laboratory
- Argonne Natl Lab: Argonne National Lab
- Idaho National Lab.: Idaho National Laboratory
- Pacific Northwest National Laboratory
- Nevada National Security Site: Nevada National Security Site
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 08 January 2013
Check for updates
Qualifiers
- Research-article
Funding Sources
Conference
CSIIRW '13
Sponsor:
- Los Alamos National Labs
- Sandia National Labs
- DOE
- Lawrence Livermore National Lab.
- BERKELEYLAB
- Argonne Natl Lab
- Idaho National Lab.
- Nevada National Security Site
CSIIRW '13: Cyber Security and Information Intelligence
January 8 - 10, 2013
Tennessee, Oak Ridge, USA
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 264Total Downloads
- Downloads (Last 12 months)4
- Downloads (Last 6 weeks)1
Reflects downloads up to 23 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in