More Web Proxy on the site http://driver.im/

research-article

Public Access

Hyperproperties of real-valued signals

Authors:

Luan Viet Nguyen,

James Kapinski,

Jyotirmoy V. Deshmukh,

Taylor T. JohnsonAuthors Info & Claims

MEMOCODE '17: Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design

Pages 104 - 113

https://doi.org/10.1145/3127041.3127058

Published: 29 September 2017 Publication History

Abstract

A hyperproperty is a property that requires two or more execution traces to check. This is in contrast to properties expressed using temporal logics such as LTL, MTL and STL, which can be checked over individual traces. Hyperproperties are important as they are used to specify critical system performance objectives, such as those related to security, stochastic (or average) performance, and relationships between behaviors. We present the first study of hyperproperties of cyber-physical systems (CPSs). We introduce a new formalism for specifying a class of hyperproperties defined over real-valued signals, called HyperSTL. The proposed logic extends signal temporal logic (STL) by adding existential and universal trace quantifiers into STL's syntax to relate multiple execution traces. Several instances of hyperproperties of CPSs including stability, security, and safety are studied and expressed in terms of HyperSTL formulae. Furthermore, we propose a testing technique that allows us to check or falsify hyperproperties of CPS models. We present a discussion on the feasibility of falsifying or verifying various classes of hyperproperties for CPSs. We extend the quantitative semantics of STL to HyperSTL and show its utility in formulating algorithms for falsification of HyperSTL specifications. We demonstrate how we can specify and falsify HyperSTL properties for two case studies involving automotive control systems.

References

[1]

Houssam Abbas, Bardh Hoxha, Georgios Fainekos, and Koichi Ueda. 2014. Robustness-guided temporal logic testing and verification for stochastic cyber-physical systems. In Cyber Technology in Automation, Control, and Intelligent Systems (CYBER), 2014 IEEE 4th Annual International Conference on. IEEE, 1--6.

[2]

Houssam Abbas, Hans Mittelmann, and Georgios Fainekos. 2014. Formal property verification in a conformance testing framework. In Formal methods and models for codesign (memocode), 2014 twelfth acm/ieee international conference on. IEEE, 155--164.

Digital Library

[3]

Aditya Agrawal, Gyula Simon, and Gabor Karsai. 2004. Semantic Translation of Simulink/Stateflow Models to Hybrid Automata Using Graph Transformations. Electronic Notes in Theoretical Computer Science 109 (2004), 43--56.

Digital Library

[4]

Shreya Agrawal and Borzoo Bonakdarpour. 2016. Runtime verification of k-safety hyperproperties in HyperLTL. In Computer Security Foundations Symposium (CSF), 2016 IEEE 29th. IEEE, 239--252.

[5]

Mohammad Al Faruque, Francesco Regazzoni, and Miroslav Pajic. 2015. Design methodologies for securing cyber-physical systems. In Proceedings of the 10th International Conference on Hardware/Software Codesign and System Synthesis. IEEE Press, 30--36.

Digital Library

[6]

Mack W Alford, Jean-Pierre Ansart, Günter Hommel, Leslie Lamport, Barbara Liskov, Geoff P Mullery, and Fred B Schneider. 1985. Distributed systems: methods and tools for specification. An advanced course. Springer-Verlag New York, Inc.

Digital Library

[7]

Gilles Barthe, Pedro R D'Argenio, and Tamara Rezk. 2004. Secure information flow by self-composition. In Computer Security Foundations Workshop, 2004. Proceedings. 17th IEEE. IEEE, 100--114.

Digital Library

[8]

Omar Beg, Taylor Johnson, and Ali Davoudi. 2017. Detection of False-data Injection Attacks in Cyber-Physical DC Microgrids. IEEE Transactions on Industrial Informatics (2017).

[9]

Nam Parshad Bhatia and Giorgio P Szegö. 2002. Stability theory of dynamical systems. Springer Science & Business Media.

[10]

Eli Biham and Adi Shamir. 1997. Differential fault analysis of secret key cryptosystems. In Annual International Cryptology Conference. Springer, 513--525.

Digital Library

[11]

F. Blanchini. 1999. Survey Paper: Set Invariance in Control. Automatica 35, 11 (Nov. 1999), 1747--1767.

Digital Library

[12]

Noel Brett, Umair Siddique, and Borzoo Bonakdarpour. 2017. Rewriting-Based Runtime Verification for Alternation-Free HyperLTL. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 77--93.

Digital Library

[13]

Jeremy W Bryans, Maciej Koutny, Laurent Mazaré, and Peter YA Ryan. 2008. Opacity generalised to transition systems. International Journal of Information Security 7, 6 (2008), 421--435.

Digital Library

[14]

Michael R Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K Micinski, Markus N Rabe, and César Sánchez. 2014. Temporal logics for hyperproperties. In International Conference on Principles of Security and Trust. Springer, 265--284.

[15]

Michael R Clarkson and Fred B Schneider. 2010. Hyperproperties. Journal of Computer Security 18, 6 (2010), 1157--1210.

[16]

Alexandre Donzé. 2010. Breach, a toolbox for verification and parameter synthesis of hybrid systems. In Computer Aided Verification. Springer, 167--170.

Digital Library

[17]

Alexandre Donzé, Thomas Ferrere, and Oded Maler. 2013. Efficient robust monitoring for STL. In Computer Aided Verification. Springer, 264--279.

[18]

Georgios E Fainekos, Antoine Girard, and George J Pappas. 2006. Temporal logic verification using simulation. In International Conference on Formal Modeling and Analysis of Timed Systems. Springer, 171--186.

Digital Library

[19]

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 Computer Software and Applications Conference Workshops (COMPSACW), 2010 IEEE 34th Annual. IEEE, 158--163.

Digital Library

[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 COMPSAC Workshops. IEEE Computer Society, 158--163.

Digital Library

[21]

Antoine Girard and George J Pappas. 2006. Verification using simulation. In International Workshop on Hybrid Systems: Computation and Control. Springer, 272--286.

Digital Library

[22]

Joseph A Goguen and José Meseguer. 1982. Security policies and security models. In Security and Privacy, 1982 IEEE Symposium on. IEEE, 11--11.

[23]

Thomas A. Henzinger, Jan Otop, and Roopsha Samanta. 2016. Lipschitz Robustness of Timed I/O Systems. Springer Berlin Heidelberg, Berlin, Heidelberg, 250--267.

Digital Library

[24]

Bardh Hoxha, Adel Dokhanchi, and Georgios Fainekos. {n. d.}. Mining parametric temporal logic properties in model-based design for cyber-physical systems. International Journal on Software Tools for Technology Transfer ({n. d.}), 1--15.

[25]

Xiaoqing Jin, Alexandre Donzé, Jyotirmoy V Deshmukh, and Sanjit A Seshia. 2015. Mining requirements from closed-loop control models. Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on 34, 11 (2015), 1704--1717.

[26]

John Kelsey, Bruce Schneier, David Wagner, and Chris Hall. 1998. Side channel cryptanalysis of product ciphers. In European Symposium on Research in Computer Security Springer, 97--110.

Digital Library

[27]

Paul Kocher, Joshua Jaffe, and Benjamin Jun. 1999. Differential power analysis. In Annual International Cryptology Conference. Springer, 388--397.

Digital Library

[28]

Paul Kocher, Ruby Lee, Gary McGraw, Anand Raghunathan, and Srivaths Moderator-Ravi. 2004. Security as a new dimension in embedded system design. In Proceedings of the 41st annual Design Automation Conference. ACM, 753--760.

Digital Library

[29]

Paul C Kocher. 1996. Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems. In Annual International Cryptology Conference. Springer, 104--113.

Digital Library

[30]

Karl Koscher, Alexei Czeskis, Franziska Roesner, Shwetak Patel, Tadayoshi Kohno, Stephen Checkoway, Damon McCoy, Brian Kantor, Danny Anderson, Hovav Shacham, et al. 2010. Experimental security analysis of a modern automobile. In Security and Privacy (SP), 2010 IEEE Symposium on. IEEE, 447--462.

Digital Library

[31]

Chunxiao Li, Anand Raghunathan, and Niraj K Jha. 2011. Hijacking an insulin pump: Security attacks and defenses for a diabetes therapy system. In e-Health Networking Applications and Services (Healthcom), 2011 13th IEEE International Conference on. IEEE, 150--156.

[32]

Lanchao Liu, Mohammad Esmalifalak, Qifeng Ding, Valentine A Emesih, and Zhu Han. 2014. Detecting false data injection attacks on power grid by sparse optimization. IEEE Transactions on Smart Grid 5, 2 (2014), 612--621.

[33]

Oded Maler and Dejan Nickovic. 2004. Monitoring temporal properties of continuous signals. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. Springer, 152--166.

[34]

Kebina Manandhar, Xiaojun Cao, Fei Hu, and Yao Liu. 2014. Detection of faults and attacks including false data injection attack in smart grid using kalman filter. IEEE transactions on control of network systems 1, 4 (2014), 370--379.

[35]

Daryl McCullough. 1987. Specifications for multi-level security and a hook-up. In Security and Privacy, 1987 IEEE Symposium on. IEEE, 161--161.

[36]

John McLean. 1990. Security models and information flow. In Research in Security and Privacy, 1990. Proceedings., 1990 IEEE Computer Society Symposium on. IEEE, 180--187.

[37]

John McLean. 1994. A general theory of composition for trace sets closed under selective interleaving functions. In Research in Security and Privacy, 1994. Proceedings., 1994 IEEE Computer Society Symposium on. IEEE, 79--93.

Digital Library

[38]

Shaunak Mishra, Yasser Shoukry, Nikhil Karamchandani, Suhas Diggavi, and Paulo Tabuada. 2015. Secure state estimation: optimal guarantees against sensor attacks in the presence of noise. In Information Theory (ISIT), 2015 IEEE International Symposium on. IEEE, 2929--2933.

[39]

Yilin Mo, Tiffany Hyun-Jin Kim, Kenneth Brancik, Dona Dickinson, Heejo Lee, Adrian Perrig, and Bruno Sinopoli. 2012. Cyber-physical security of a smart grid infrastructure. Proc. IEEE 100, 1 (2012), 195--209.

[40]

Truong Nghiem, Sriram Sankaranarayanan, Georgios Fainekos, Franjo Ivancić, Aarti Gupta, and George J. Pappas. 2010. Monte-carlo Techniques for Falsification of Temporal Properties of Non-linear Hybrid Systems. In Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control (HSCC '10). ACM, New York, NY, USA, 211--220.

Digital Library

[41]

Markus N Rabe. 2016. A temporal logic approach to information-flow control. (2016).

[42]

Srivaths Ravi, Anand Raghunathan, and Srimat Chakradhar. 2004. Tamper resistance mechanisms for secure embedded systems. In VLSI Design, 2004. Proceedings. 17th International Conference on. IEEE, 605--611.

Digital Library

[43]

Pankaj Rohatgi. 2009. Electromagnetic attacks and countermeasures. In Cryptographic Engineering. Springer, 407--430.

[44]

Andrei Sabelfeld and David Sands. 2005. Dimensions and principles of declassification. In Computer Security Foundations, 2005. CSFW-18 2005. 18th IEEE Workshop. IEEE, 255--269.

Digital Library

[45]

Florian Sagstetter, Martin Lukasiewycz, Sebastian Steinhorst, Marko Wolf, Alexandre Bouard, William R Harris, Somesh Jha, Thomas Peyrin, Axel Poschmann, and Samarjit Chakraborty. 2013. Security challenges in automotive hardware/software architecture design. In Proceedings of the Conference on Design, Automation and Test in Europe. EDA Consortium, 458--463.

Digital Library

[46]

Yasser Shoukry, Paul Martin, Paulo Tabuada, and Mani Srivastava. 2013. Non-invasive Spoofing Attacks for Anti-lock Braking Systems. In Proceedings of the 15th International Conference on Cryptographic Hardware and Embedded Systems (CHES'13). Springer-Verlag, Berlin, Heidelberg, 55--72.

Digital Library

[47]

Geoffrey Smith. 2009. On the foundations of quantitative information flow. In International Conference on Foundations of Software Science and Computational Structures. Springer, 288--302.

[48]

Jiang Wan, Arquimedes Canedo, and Mohammad Abdullah Al Faruque. 2015. Security-aware functional modeling of cyber-physical systems. In Emerging Technologies & Factory Automation (ETFA), 2015 IEEE 20th Conference on. IEEE, 1--4.

[49]

J Todd Wittbold and Dale M Johnson. 1990. Information flow in nondeterministic systems. In Research in Security and Privacy, 1990. Proceedings., 1990 IEEE Computer Society Symposium on. IEEE, 144--161.

[50]

Zhe Xu and A Agung Julius. 2016. Census signal temporal logic inference for multiagent group behavior analysis. IEEE Transactions on Automation Science and Engineering (2016).

[51]

Steve Zdancewic and Andrew C Myers. 2003. Observational determinism for concurrent program security. In Computer Security Foundations Workshop, 2003. Proceedings. 16th IEEE. IEEE, 29--43.

[52]

Liang Zou, Naijun Zhan, Shuling Wang, and Martin Fränzle. 2015. Formal Verification of Simulink/Stateflow Diagrams. In Automated Technology for Verification and Analysis - 13th International Symposium, Shanghai, China. 464--481.

Cited By

Anand MMurali VTrivedi AZamani M(2024)Verification of Hyperproperties for Dynamical Systems via Barrier CertificatesIEEE Transactions on Automatic Control10.1109/TAC.2024.338444869:10(6920-6934)Online publication date: Oct-2024
https://doi.org/10.1109/TAC.2024.3384448
Biewer SBaum KSterz SHermanns HHetmank SLanger MLauber-Rönsberg ALehr F(2024)Software doping analysis for human oversightFormal Methods in System Design10.1007/s10703-024-00445-2Online publication date: 4-Apr-2024
https://doi.org/10.1007/s10703-024-00445-2
Bonnah ENguyen LHoque K(2024)Efficient SMT-Based Model Checking for HyperTWTLFormal Methods and Software Engineering10.1007/978-981-96-0617-7_19(332-352)Online publication date: 29-Nov-2024
https://doi.org/10.1007/978-981-96-0617-7_19
Show More Cited By

Recommendations

Formal verification of hyperproperties for control systems
CAADCPS '21: Proceedings of the Workshop on Computation-Aware Algorithmic Design for Cyber-Physical Systems

In recent years, there has been a great deal of interest and research in verifying complex cyber-physical systems (CPS) against rich and expressive specifications [2] such as safety and liveness, to provide formal guarantees for safety-critical systems. ...
Hyperproperties
7th International Workshop on Issues in the Theory of Security (WITS'07)

Trace properties, which have long been used for reasoning about systems, are sets of execution traces. Hyperproperties, introduced here, are sets of trace properties. Hyperproperties can express security policies, such as secure information flow and ...
Hyperproperties
CSF '08: Proceedings of the 2008 21st IEEE Computer Security Foundations Symposium

Properties, which have long been used for reasoning about systems, are sets of traces. Hyperproperties, introduced here, are sets of properties. Hyperproperties can express security policies, such as secure information flow, that properties cannot. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

MEMOCODE '17: Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design

September 2017

192 pages

ISBN:9781450350938

DOI:10.1145/3127041

General Chair:
Jean-Pierre Talpin
INRIA, France
,
Program Chairs:
Patricia Derler
National Instruments
,
Klaus Schneider
University of Kaiserslautern, Germany

Copyright © 2017 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

SIGBED: ACM Special Interest Group on Embedded Systems
SIGDA: ACM Special Interest Group on Design Automation
IEEE CAS
IEEE CEDA

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 29 September 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article

Funding Sources

National Science Foundation (NSF)
Air Force Office of Scientific Research (AFOSR)
Air Force Research Laboratory (AFRL)

Conference

MEMOCODE '17

Sponsor:

MEMOCODE '17: 15th ACM-IEEE International Conference on Formal Methods and Models for System Design

September 29 - October 2, 2017

Vienna, Austria

Acceptance Rates

MEMOCODE '17 Paper Acceptance Rate 22 of 48 submissions, 46%;

Overall Acceptance Rate 34 of 82 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

30
Total Citations
View Citations
818
Total Downloads

Downloads (Last 12 months)193
Downloads (Last 6 weeks)20

Reflects downloads up to 17 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Anand MMurali VTrivedi AZamani M(2024)Verification of Hyperproperties for Dynamical Systems via Barrier CertificatesIEEE Transactions on Automatic Control10.1109/TAC.2024.338444869:10(6920-6934)Online publication date: Oct-2024
https://doi.org/10.1109/TAC.2024.3384448
Biewer SBaum KSterz SHermanns HHetmank SLanger MLauber-Rönsberg ALehr F(2024)Software doping analysis for human oversightFormal Methods in System Design10.1007/s10703-024-00445-2Online publication date: 4-Apr-2024
https://doi.org/10.1007/s10703-024-00445-2
Bonnah ENguyen LHoque K(2024)Efficient SMT-Based Model Checking for HyperTWTLFormal Methods and Software Engineering10.1007/978-981-96-0617-7_19(332-352)Online publication date: 29-Nov-2024
https://doi.org/10.1007/978-981-96-0617-7_19
Bonnah ENguyen LHoque KZhu Qvon Hanxleden RStephen EBrandt J(2023)Model Checking Time Window Temporal Logic for HyperpropertiesProceedings of the 21st ACM-IEEE International Conference on Formal Methods and Models for System Design10.1145/3610579.3611077(100-110)Online publication date: 21-Sep-2023
https://dl.acm.org/doi/10.1145/3610579.3611077
Finkbeiner B(2023)Logics and Algorithms for HyperpropertiesACM SIGLOG News10.1145/3610392.361039410:2(4-23)Online publication date: 19-Jul-2023
https://dl.acm.org/doi/10.1145/3610392.3610394
Bartocci EMateis CNesterini ENičković D(2023)Mining Hyperproperties using Temporal LogicsACM Transactions on Embedded Computing Systems10.1145/360939422:5s(1-26)Online publication date: 31-Oct-2023
https://dl.acm.org/doi/10.1145/3609394
Bonnah ENguyen LAnuarul Hoque K(2023)Motion Planning Using Hyperproperties for Time Window Temporal LogicIEEE Robotics and Automation Letters10.1109/LRA.2023.32808308:8(4386-4393)Online publication date: Aug-2023
https://doi.org/10.1109/LRA.2023.3280830
Beutner RFinkbeiner BFrenkel HMetzger N(2023)Second-Order HyperpropertiesComputer Aided Verification10.1007/978-3-031-37703-7_15(309-332)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37703-7_15
Finkbeiner BFrenkel HHofmann JLohse J(2023)Automata-Based Software Model Checking of HyperpropertiesNASA Formal Methods10.1007/978-3-031-33170-1_22(361-379)Online publication date: 3-Jun-2023
https://doi.org/10.1007/978-3-031-33170-1_22
Tran HXiang WJohnson T(2022)Verification Approaches for Learning-Enabled Autonomous Cyber–Physical SystemsIEEE Design & Test10.1109/MDAT.2020.301571239:1(24-34)Online publication date: Feb-2022
https://doi.org/10.1109/MDAT.2020.3015712
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents