A Semantic Framework for Direct Information Flows in Hybrid-Dynamic Systems
Pages 5 - 15
Abstract
Hybrid-dynamic models provide an underlying framework to study the evergrowing cyber-physical systems with an emphasis on the integration of their discrete computational steps and the associated continuous physical dynamics. Ubiquity of cyber-physical systems necessitates some level of assurance about the secure flow of information through different discrete and continuous components. In recent years, different logical frameworks have been proposed to analyze indirect information flows in cyber-physical systems. While these frameworks are used to verify secure flow of information in a metalevel, they naturally fall short in support of implementing information flow analyzers that could effectively enforce policies at runtime. This practical limitation has triggered the implementation of direct information flow analyzers in different language settings. In this paper, we focus on direct flows of information confidentiality in hybrid-dynamic environments and propose a semantic framework through which we can judge about such flows. This semantic framework can be used to study the correctness of enforced policies by these analyzers, and in particular taint tracking tools. In this regard, we specify a dynamic taint tracking policy for hybrid dynamic systems and prove its soundness based on the proposed semantic framework. As a case study, we consider the flow of information in a public transportation control system, and the effectiveness of our enforced policy on this system.
References
[1]
Ravi Akella and Bruce M McMillin. 2010. Information flow analysis of energy management in a smart grid. In International Conference on Computer Safety, Reliability, and Security. Springer, 263--276.
[2]
Ravi Akella, Han Tang, and Bruce M McMillin. 2010. Analysis of information flow security in cyber--physical systems. International Journal of Critical Infrastructure Protection, Vol. 3, 3--4 (2010), 157--173.
[3]
Rajeev Alur, Costas Courcoubetis, Thomas A Henzinger, and Pei-Hsin Ho. 1992. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Hybrid systems. Springer, 209--229.
[4]
Aslan Askarov and Andrei Sabelfeld. 2007. Gradual Release: Unifying Declassification, Encryption and Key Release Policies. In IEEE S&P. 207--221.
[5]
Jonathan Bell and Gail Kaiser. 2015. Dynamic taint tracking for java with phosphor. In Proceedings of the 2015 International Symposium on Software Testing and Analysis. 409--413.
[6]
Patrick Blackburn and Jerry Seligman. 1995. Hybrid languages. Journal of Logic, Language and Information, Vol. 4, 3 (1995), 251--272.
[7]
Brandon Bohrer and André Platzer. 2018. A hybrid, dynamic logic for hybrid-dynamic information flow. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. 115--124.
[8]
John H Castellanos, Mart'in Ochoa, and Jianying Zhou. 2018. Finding dependencies between cyber-physical domains for security testing of industrial control systems. In Proceedings of the 34th Annual Computer Security Applications Conference. 582--594.
[9]
Z Berkay Celik, Leonardo Babun, Amit Kumar Sikder, Hidayet Aksu, Gang Tan, Patrick McDaniel, and A Selcuk Uluagac. 2018. Sensitive information tracking in commodity IoT. In 27th USENIX Security Symposium (USENIX Security 18). 1687--1704.
[10]
Hari Cherupalli, Henry Duwe, Weidong Ye, Rakesh Kumar, and John Sartori. 2017. Software-based gate-level information flow security for IoT systems. In Proceedings of the 50th Annual IEEE/ACM International Symposium on Microarchitecture. 328--340.
[11]
Michael R. Clarkson and Fred B. Schneider. 2010. Hyperproperties. Journal of Computer Security, Vol. 18, 6 (2010), 1157--1210.
[12]
Pieter Jan Laurens Cuijpers and Michel A Reniers. 2005. Hybrid process algebra. The Journal of Logic and Algebraic Programming, Vol. 62, 2 (2005), 191--245.
[13]
Werner Damm, Alfred Mikschl, Jens Oehlerking, Ernst-Rüdiger Olderog, Jun Pang, André Platzer, Marc Segelken, and Boris Wirtz. 2007. Automating verification of cooperation, control, and design in traffic applications. In Formal methods and hybrid real-time systems. Springer, 115--169.
[14]
Sriharsha Etigowni, Dave Tian, Grant Hernandez, Saman Zonouz, and Kevin Butler. 2016. CPAC: securing critical infrastructure with cyber-physical access control. In Proceedings of the 32nd annual conference on computer security applications. 139--152.
[15]
Earlence Fernandes, Justin Paupore, Amir Rahmati, Daniel Simionato, Mauro Conti, and Atul Prakash. 2016. Flowfence: Practical data protection for emerging iot application frameworks. In 25th USENIX Security Symposium (USENIX Security 16). 531--548.
[16]
Pietro Ferrara, Amit Kr Mandal, Agostino Cortesi, and Fausto Spoto. 2020 a. Static analysis for discovering IoT vulnerabilities. International Journal on Software Tools for Technology Transfer (2020), 1--18.
[17]
Pietro Ferrara, Luca Olivieri, and Fausto Spoto. 2020 b. BackFlow: Backward Context-Sensitive Flow Reconstruction of Taint Analysis Results. In International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, 23--43.
[18]
William Fu, Raymond Lin, and Daniel Inge. 2018. Taintassembly: Taint-based information flow control tracking for webassembly. arXiv preprint arXiv:1802.01050 (2018).
[19]
Vashti Galpin, Luca Bortolussi, and Jane Hillston. 2013. HYPE: Hybrid modelling by composition of flows. Formal Aspects of Computing, Vol. 25, 4 (2013), 503--541.
[20]
Thoshitha T Gamage, Bruce M McMillin, and Thomas P Roth. 2010. Enforcing information flow security properties in cyber-physical systems: A generalized framework based on compensation. In 2010 IEEE 34th Annual Computer Software and Applications Conference Workshops. IEEE, 158--163.
[21]
Thomas A Henzinger. 2000. The theory of hybrid automata. In Verification of digital and hybrid systems. Springer, 265--292.
[22]
Alex Q Huang. 2009. Renewable energy system research and education at the NSF FREEDM systems center. In 2009 IEEE Power & Energy Society General Meeting. IEEE, 1--6.
[23]
Wei Huang, Yao Dong, and Ana Milanova. 2014. Type-based taint analysis for Java web applications. In International Conference on Fundamental Approaches to Software Engineering. Springer, 140--154.
[24]
Neil Klingensmith, Younghyun Kim, and Suman Banerjee. 2019. A Hypervisor-Based Privacy Agent for Mobile and IoT Systems. In Proceedings of the 20th International Workshop on Mobile Computing Systems and Applications. 21--26.
[25]
Ivan Lanese, Luca Bedogni, and Marco Di Felice. 2013. Internet of things: a process calculus approach. In Proceedings of the 28th Annual ACM Symposium on Applied Computing. 1339--1346.
[26]
Ruggero Lanotte and Massimo Merro. 2017. A calculus of cyber-physical systems. In International Conference on Language and Automata Theory and Applications. Springer, 115--127.
[27]
Ruggero Lanotte and Massimo Merro. 2018. A semantic theory of the Internet of Things. Information and Computation, Vol. 259 (2018), 72--101.
[28]
Ruggero Lanotte, Massimo Merro, Riccardo Muradore, and Luca Viganò. 2017. A formal approach to cyber-physical attacks. In 2017 IEEE 30th Computer Security Foundations Symposium (CSF). IEEE, 436--450.
[29]
Jed Liu, Joe Corbett-Davies, Andrew Ferraiuolo, Alexander Ivanov, Mulong Luo, G Edward Suh, Andrew C Myers, and Mark Campbell. 2018. Secure autonomous cyber-physical systems through verifiable information flow control. In Proceedings of the 2018 Workshop on Cyber-Physical Systems Security and PrivaCy. 48--59.
[30]
Amit Mandal, Pietro Ferrara, Yuliy Khlyebnikov, Agostino Cortesi, and Fausto Spoto. 2020. Cross-program taint analysis for IoT systems. In Proceedings of the 35th Annual ACM Symposium on Applied Computing. 1944--1952.
[31]
Eric Rothstein Morris, Carlos G Murguia, and Mart'in Ochoa. 2017. Design-time quantification of integrity in cyber-physical systems. In Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security. 63--74.
[32]
André Platzer. 2007. Differential dynamic logic for verifying parametric hybrid systems. In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods. Springer, 216--232.
[33]
André Platzer. 2008. Differential dynamic logic for hybrid systems. Journal of Automated Reasoning, Vol. 41, 2 (2008), 143--189.
[34]
André Platzer. 2012. The complete proof theory of hybrid systems. In 2012 27th Annual IEEE Symposium on Logic in Computer Science. IEEE, 541--550.
[35]
André Platzer. 2018. Logical foundations of cyber-physical systems. Vol. 662. Springer.
[36]
Andrei Sabelfeld and Andrew C Myers. 2003. Language-based Information-flow Security. IEEE Journal on selected areas in communications, Vol. 21, 1 (2003), 5--19.
[37]
Fred B Schneider. 2000. Enforceable security policies. ACM Transactions on Information and System Security (TISSEC), Vol. 3, 1 (2000), 30--50.
[38]
Daniel Schoepe, Musard Balliu, Benjamin C. Pierce, and Andrei Sabelfeld. 2016. Explicit Secrecy: A Policy for Taint Tracking. In IEEE EuroS&P. 15--30.
[39]
Philipp Dominik Schubert, Ben Hermann, and Eric Bodden. 2019. PhASAR: An inter-procedural static analysis framework for C/C+. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 393--410.
[40]
Julian Schütte and Gerd Stefan Brost. 2018. LUCON: Data flow control for message-based IoT systems. In 2018 17th IEEE International Conference On Trust, Security And Privacy In Computing And Communications/12th IEEE International Conference On Big Data Science And Engineering (TrustCom/BigDataSE). IEEE, 289--299.
[41]
Koushik Sen, Swaroop Kalasapur, Tasneem Brutch, and Simon Gibbs. 2013. Jalangi: a selective record-replay and dynamic analysis framework for JavaScript. In Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering. 488--498.
[42]
Christian Skalka, Sepehr Amir-Mohammadian, and Samuel Clark. 2020. Maybe tainted data: Theory and a case study. Journal of Computer Security Preprint (2020), 1--41.
[43]
Hao Sun, Xiangyu Zhang, Chao Su, and Qingkai Zeng. 2015. Efficient dynamic tracking technique for detecting integer-overflow-to-buffer-overflow vulnerability. In Proceedings of the 10th ACM Symposium on Information, Computer and Communications Security. 483--494.
[44]
Pengfei Sun, Luis Garcia, and Saman Zonouz. 2019. Tell Me More Than Just Assembly! Reversing Cyber-Physical Execution Semantics of Embedded IoT Controller Software Binaries. In 2019 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). IEEE, 349--361.
[45]
Aron Szanto, Timothy Tamm, and Artidoro Pagnoni. 2018. Taint tracking for webassembly. arXiv preprint arXiv:1807.08349 (2018).
[46]
Dennis M. Volpano. 1999. Safety versus Secrecy. In SAS. 303--311.
[47]
Jingming Wang and Huiqun Yu. 2014. Analysis of the composition of non-deducibility in cyber-physical systems. Applied Mathematics & Information Sciences, Vol. 8, 6 (2014), 3137.
[48]
Ran Wang, Guangquan Xu, Xianjiao Zeng, Xiaohong Li, and Zhiyong Feng. 2018. TT-XSS: A novel taint tracking based dynamic detection framework for DOM Cross-Site Scripting. J. Parallel and Distrib. Comput., Vol. 118 (2018), 100--106.
Index Terms
- A Semantic Framework for Direct Information Flows in Hybrid-Dynamic Systems
Recommendations
A permission-carrying security policy and static enforcement for information flows in Android programs
AbstractTo detect information leaks in Android programs, existing taint analysis approaches usually specify and enforce (statically or dynamically) the two-level information flow policy, represented by a lattice ( { ⊤ , ⊥ } , ⊑ ) with ⊥ ⊑ ⊤. ...
A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow
LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer ScienceInformation-flow security is important to the safety and privacy of cyber-physical systems (CPSs) across many domains: information leakage can both violate user privacy and reveal vulnerabilities to physical attacks. CPSs face the challenge that ...
Statically analyzing information flows: an abstract interpretation-based hyperanalysis for non-interference
SAC '19: Proceedings of the 34th ACM/SIGAPP Symposium on Applied ComputingIn the context of systems security, information flows play a central role. Unhandled information flows potentially leave the door open to very dangerous types of attacks, such as code injection or sensitive information leakage. Information flows ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
May 2021
81 pages
ISBN:9781450384025
DOI:10.1145/3457339
- General Chairs:
- Jiannong Cao,
- Man Ho Au,
- Program Chairs:
- Mauro Conti,
- Nils Ole Tippenhauer
Copyright © 2021 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 25 May 2021
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
ASIA CCS '21
Sponsor:
ASIA CCS '21: ACM Asia Conference on Computer and Communications Security
June 7, 2021
Virtual Event, Hong Kong
Acceptance Rates
Overall Acceptance Rate 43 of 135 submissions, 32%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 58Total Downloads
- Downloads (Last 12 months)5
- Downloads (Last 6 weeks)0
Reflects downloads up to 18 Jan 2025
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