skip to main content
article

Information flow in hybrid systems

Published: 01 November 2004 Publication History

Abstract

Our aim is to study the information flow problem in hybrid systems, namely systems consisting of a discrete program with an analog environment. Information flows compromise the security of a system because they cause leakage of protected information. In order to tackle information flow in real-life systems, we introduce new classes of hybrid systems that extend the known ones while preserving their properties. Then, we define a logic to specify information flow. By means of some examples, we show that, by this logic, we are able to express information flows in hybrid systems and to certify that some suspect behaviors of these systems do not give rise to any information flow. We give a model checking procedure for our logic, and we prove that it gives a correct answer whenever it terminates. Moreover, for a particular class of hybrid systems, we give a version of the procedure that always terminates.

References

[1]
Alur, R., Courcoubetis, C., and Dill, D. L. 1994. Model checking in dense real time. Inform. Comput. 104, 2--34.]]
[2]
Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T. A., Ho, P. H., Nicollin, X., Olivero, A., Sifakis, J., and Yovine, S. 1995. The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138, 3--34.]]
[3]
Alur, R. and Dill, D. L. 1994. A theory of timed automata. Theor. Comput. Sci. 126, 183--235.]]
[4]
Alur, R. and Dill, D. L. 1996. Automata-theoretic verification of real-time systems. In Formal Methods for Real-Time Computing, Trends in Software Series. John Wiley & Sons, New York, 55--82.]]
[5]
Alur, R., Etessami, K., La Torre, S., and Peled, D. 1999. Parametric temporal logic for model measuring. In International Colloquium on Automata, Languages, and Programming. Lecture Notes in Computer Science, vol. 1664. Springer, Berlin, 159--168.]]
[6]
Alur, R. and Henzinger, T. A. 1992. Logic and models of real time: A survey. In Real-Time: Theory in Practice, REX Workshop. Lecture Notes in Computer Science, vol. 600. Springer, Berlin, 74--106.]]
[7]
Alur, R. and Henzinger, T. A. 1994. A really temporal logic. Journal of the ACM 41, 81--204.]]
[8]
Alur, R., Henzinger, T. A., and Ho, P. H. 1996. Automatic symbolic verification of embedded systems. IEEE Trans. Softw. Engng. 22, 181--201.]]
[9]
Bell, D. and La Padula, L. J. 1976. Secure Computer Systems: Unified Exposition and Multics Interpretation. Tech. Rep. ESD-TR-75-301, MITRE MTR-2997.]]
[10]
Bieber, P. and Cuppens, F. 1994. A logical view of secure dependencies. J. Comput. Secur. 1, 99--129.]]
[11]
Bouyer, P., Dufourd, C., Fleury, E., and Petit, A. 2000a. Are timed automata updatable? In International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 1855. Springer, Berlin, 464--479.]]
[12]
Bouyer, P., Dufourd, C., Fleury, E., and Petit, A. 2000b. Expressiveness of updatable timed automata. In International Symposium on Mathematical Foundations of Computer Science. Lecture Notes in Computer Science, vol. 1893. Springer, Berlin, 232--242.]]
[13]
Bruyère, V., Dall'Olio, E., and Raskin, J. F. 2003. Durations, parametric model-checking in timed automata with Presburger arithmetic. In International Symposium on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science, vol. 2607. Springer, Berlin, 687--698.]]
[14]
Burch, J. R., Clarke, E. M., McMillan, K. L., Dill, D. L., and Hwang, L. J. 1992. Symbolic model checking: 1020 states and beyond. Inform. Comput. 98, 142--170.]]
[15]
CASCADE. Chip Architecture for Smart Cards and Portable Intelligent Devices. Available at http://www.dice.ucl.ac.be/crypto/cascade.]]
[16]
Chaochen, Z., Hansen, M. R., and Sestoft, P. 1993. Decidability and undecidability results for Duration Calculus. In International Symposium on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science, vol. 665. Springer, Berlin, 58--68.]]
[17]
Clarke, E. M. and Emerson, E. A. 1982. Design and synthesis of synchronization skeletons using branching time temporal logic. In International Workshop on Logic of Programs. Lecture Notes in Computer Science, vol. 131. Springer, Berlin, 52--71.]]
[18]
Dhem, J. F., Koeune, F., Leroux, P. A., Mestré, P., Quisquater, J. J., and Willems, J. L. 1998. A practical implementation of the timing attack. In International Conference on Smart Card Research and Applications. Lecture Notes in Computer Science, vol. 1820. Springer, Berlin, 167--182.]]
[19]
Felten, E. W. and Schneider, M. A. M. 2000. Timing attacks on web privacy. In ACM Conference on Computer and Communications Security. ACM Press, New York, 25--32.]]
[20]
Focardi, R. and Gorrieri, R. 1995. A classification of security properties for process algebras. J. Comput. Secur. 3, 5--33.]]
[21]
Focardi, R. and Gorrieri, R. 1997. The compositional security checker: A tool for the verification of information flow security properties. IEEE Trans. Softw. Engng 23, 550--571.]]
[22]
Focardi, R. and Gorrieri, R. 2001. Classification of security properties (Part I: Information flow). In Foundations of Security Analysis and Design Summer School. Lecture Notes in Computer Science, vol. 2171. Springer, Berlin, 331--396.]]
[23]
Focardi, R., Gorrieri, R., and Martinelli, F. 2000. Information flow analysis in a discrete time process algebra. In IEEE Computer Security Foundation Workshop. IEEE Computer Society Press, Los Alamitos, 170--184.]]
[24]
Focardi, R. and Rossi, S. 2002. Information flow security in dynamic contexts. In IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos, 307--319.]]
[25]
Fränzle, M. 1999. Analysis of hybrid systems: An ounce of realism can save an infinity of states. In International Workshop on Computer Science Logic. Lecture Notes in Computer Science, vol. 1683. Springer, Berlin, 126--140.]]
[26]
Fränzle, M. 2001. What will be eventually true of polynomial hybrid automata. In International Symposium on Theoretical Aspects of Computer Software. Lecture Notes in Computer Science, vol. 2215. Springer, Berlin, 340--359.]]
[27]
Gorrieri, R., Lanotte, R., Maggiolo-Schettini, A., Martinelli, F., Tini, S., and Tronci, E. 2004. Automated analysis of timed security: A case study on web privacy. Int. J. Inform. Secur. 2, 168--186.]]
[28]
Gruska, D. P., Lanotte, R., and Maggiolo-Schettini, A. 2002. A Contribution to a Classification of Timing Attacks on Privacy. Tech. Rep. NS-02-3, BRICS, Aarhus, Denmark.]]
[29]
Handschuh, H. and Heys, H. M. 2002. A timing attack on RC5. In Selected Areas in Cryptography. Lecture Notes in Computer Science, vol. 1556. Springer, Berlin, 306--318.]]
[30]
Henzinger, T. A., Nicollin, X., Sifakis, J., and Yovine, S. 1994. Symbolic model checking for real-time systems. Inform. Comput. 111, 193--244.]]
[31]
Hevia, A. and Kiwi, M. 1999. Strength of two data encryption standard implementations under timing attacks. ACM Trans. Inform. Syst. Secur. 2, 416--437.]]
[32]
Johnson, D. M. and Thayer, F. J. 1988. Security and the composition of machines. In IEEE Computer Security Foundation Workshop. IEEE Computer Society Press, Los Alamitos, 72--89.]]
[33]
Kocher, P. C. 1996. Timing attacks on implementations of Diffie-Hellman, RSA, DSS and other systems. In International Cryptology Conference. Lecture Notes in Computer Science, vol. 1109. Springer, Berlin, 104--113.]]
[34]
Koeune, F. and Quisquater, J. J. 1999. A timing attack against Rijndael. Tech. Rep. CG-1999/1, Université Catholique de Louvain, Louvain-la-Neuve, Belgium.]]
[35]
Lakhneche, Y. and Hooman, J. 1995. Metric temporal logic with durations. Theor. Comput. Sci. 138, 169--199.]]
[36]
Lanotte, R. 2002. An Automaton-Theoretic Approach to Safety and Security in Real-Time Systems. Ph.D. Thesis, University of Pisa, Pisa, Italy.]]
[37]
Lanotte, R. 2003. Expressive power of hybrid systems with parameters, variables and arrays. In International Workshop on Expressiveness on Concurrency. Electronic Notes in Theoretical Computer Science, vol. 72. Elsevier, Amsterdam.]]
[38]
Lanotte, R., Maggiolo-Schettini, A., and Tini, S. 2002. Privacy in real-time systems. In Models for Time-Critical Systems. Electronic Notes in Theoretical Computer Science, vol. 52. Elsevier, Amsterdam.]]
[39]
McCollough, D. 1988. Noninterference and the composability of security properties. In IEEE Symposium on Security and Privacy. IEEE Computer Society Press, Los Alamitos, 177--186.]]
[40]
Millen, J. K. 1990. Hookup security for synchronous machines. In IEEE Computer Security Foundation Workshop. IEEE Computer Society Press, Los Alamitos, 84--90.]]
[41]
Pnueli, A. and Sifakis, J. 1995. Special issue on hybrid systems. Theor. Comput. Sci. 138.]]
[42]
Queille, J. and Sifakis, J. 1995. Specification and verification of concurrent systems in CESAR. In International Symposium on Programming. Lecture Notes in Computer Science, vol. 137. Springer, Berlin, 337--351.]]
[43]
Song, D. X., Wagner, D., and Tian, X. 2001. Timing analysis of keystrokes and timing attacks on SSH. In USENIX Security Symposium.]]
[44]
Sutherland, D. 1986. A model of information. In National Computer Security Conference. 175--183.]]
[45]
Tarski, A. 1951. A decision method for elementary algebra and geometry. Tech. rep., University of California, Berkeley, California.]]
[46]
Weispfenning, V. 1999. Mixed real-integer linear quantifier elimination. In ACM International Symposium on Symbolic and Algebraic Computation. ACM Press, New York, 129--136.]]
[47]
Wittbold, J. T. and Johnson, D. M. 1990. Information flow in nondeterministic systems. In IEEE Symposium on Research in Security and Privacy. IEEE Computer Security Press, Los Alamitos, 144--161.]]

Cited By

View all
  • (2007)Expressive power of hybrid systems with real variables, integer variables and arraysJournal of Automata, Languages and Combinatorics10.5555/1463079.146308212:3(373-405)Online publication date: 1-Jan-2007

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Embedded Computing Systems
ACM Transactions on Embedded Computing Systems  Volume 3, Issue 4
November 2004
203 pages
ISSN:1539-9087
EISSN:1558-3465
DOI:10.1145/1027794
Issue’s Table of Contents
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]

Publisher

Association for Computing Machinery

New York, NY, United States

Journal Family

Publication History

Published: 01 November 2004
Published in TECS Volume 3, Issue 4

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Hybrid systems
  2. information flow

Qualifiers

  • Article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)2
  • Downloads (Last 6 weeks)0
Reflects downloads up to 20 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2007)Expressive power of hybrid systems with real variables, integer variables and arraysJournal of Automata, Languages and Combinatorics10.5555/1463079.146308212:3(373-405)Online publication date: 1-Jan-2007

View Options

Login options

Full Access

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media