Skip to main content

Weak Behavioral Equivalences for Verifying Secure and Performance-Aware Component-Based Systems

  • Chapter
Architecting Dependable Systems VI

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5835))

  • 371 Accesses

Abstract

Component-based systems are characterized by several orthogonal requirements, ranging from security to quality of service, which may demand for the use of opposite strategies and interfering mechanisms. To achieve a balanced tradeoff among these aspects, we have previously proposed the use of a predictive methodology, which encompasses classical tools such as the noninterference approach to security analysis and standard performance evaluation techniques. The former tool, which is based on equivalence checking, is used to reveal functional dependencies among component behaviors, while the latter tool, which relies on reward-based numerical analysis, is used to study the quantitative impact of these dependencies on the system performance. In order to strengthen the relation between these two different analysis techniques we advocate the use of performance-aware notions of behavioral equivalence as a formal means for detecting functional and performance dependencies and then pinpointing the metrics at the base of a balanced tradeoff.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Acquaviva, A., Aldini, A., Bernardo, M., Bogliolo, A., Bontà, E., Lattanzi, E.: A Methodology Based on Formal Methods for Predicting the Impact of Dynamic Power Management. In: Bernardo, M., Bogliolo, A. (eds.) SFM-Moby 2005. LNCS, vol. 3465, pp. 155–189. Springer, Heidelberg (2005)

    Google Scholar 

  2. Aldini, A.: Classification of security properties in a Linda-like process algebra. Journal of Science of Computer Programming 63, 16–38 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  3. Aldini, A., Bernardo, M.: A General Framework for Nondeterministic, Probabilistic, and Stochastic Noninterference. In: Degano, P. (ed.) ARSPA-WITS 2009. LNCS, vol. 5511, pp. 18–33. Springer, Heidelberg (2009)

    Google Scholar 

  4. Aldini, A., Bernardo, M.: A Formal Approach to the Integrated Analysis of Security and QoS. Journal of Reliability Engineering & System Safety 92, 1503–1520 (2007)

    Article  Google Scholar 

  5. Aldini, A., Bernardo, M.: Mixing Logics and Rewards for the Component oriented Specification of Performance Measures. Journal of Theoretical Computer Science 382, 3–23 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  6. Aldini, A., Bravetti, M., Gorrieri, R.: A Process-Algebraic Approach for the Analysis of Probabilistic Noninterference. Journal of Computer Security 12, 191–245 (2004)

    Google Scholar 

  7. Bernardo, M., Aldini, A.: Weak Markovian Bisimilarity: Abstracting from Prioritized/Weighted Internal Immediate Actions. In: 10th Italian Conference on Theoretical Computer Science (ICTCS 2007), pp. 39–56. World Scientific, Singapore (2007)

    Google Scholar 

  8. Balsamo, S., Bernardo, M., Simeoni, M.: Performance Evaluation at the Software Architecture Level. In: Bernardo, M., Inverardi, P. (eds.) SFM 2003. LNCS, vol. 2804, pp. 207–258. Springer, Heidelberg (2003)

    Google Scholar 

  9. Bernardo, M.: TwoTowers 5.1 User Manual (2006), http://www.sti.uniurb.it/bernardo/twotowers/

  10. Bondavalli, A., Majzik, I., Pataricza, A.: Stochastic Dependability Analysis of System Architecture based on UML Designs. In: de Lemos, R., Gacek, C., Romanovsky, A. (eds.) Architecting Dependable Systems. LNCS, vol. 2677, pp. 219–244. Springer, Heidelberg (2003)

    Google Scholar 

  11. Bravetti, M., Aldini, A.: Discrete Time Generative-Reactive Probabilistic Processes with Different Advancing Speeds. Theoretical Computer Science 290, 355–406 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  12. Focardi, R., Gorrieri, R.: A Classification of Security Properties. Journal of Computer Security 3, 5–33 (1995)

    Google Scholar 

  13. van Glabbeek, R.J., Smolka, S.A., Steffen, B.: Reactive, Generative and Stratified Models of Probabilistic Processes. Information and Computation 121, 59–80 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  14. Goguen, J.A., Meseguer, J.: Security Policy and Security Models. In: Symp. on Research in Security and Privacy (SSP 1982), pp. 11–20. IEEE CS Press, Los Alamitos (1982)

    Google Scholar 

  15. Gupta, V., Lam, V., Ramasamy, H.V., Sanders, W.H., Singh, S.: Dependability and performance evaluation of intrusion-tolerant server architectures. In: de Lemos, R., Weber, T.S., Camargo Jr, J.B. (eds.) LADC 2003. LNCS, vol. 2847, pp. 81–101. Springer, Heidelberg (2003)

    Google Scholar 

  16. Hein, A., Dal Cin, M.: Performance and Dependability Evaluation of Scalable Massively Parallel Computer Systems with Conjoint Simulation. ACM Transactions on Modeling and Computer Simulation 8, 333–373 (1998)

    Article  MATH  Google Scholar 

  17. Howard, R.A.: Dynamic Probabilistic Systems. John Wiley & Sons, Chichester (1971)

    Google Scholar 

  18. McLean, J.: Security Models and Information Flow. In: Symp. on Research in Security and Privacy (SSP 1990), pp. 180–187. IEEE CS Press, Los Alamitos (1990)

    Chapter  Google Scholar 

  19. Meadows, C.: What Makes a Cryptographic Protocol Secure? The Evolution of Requirements Specification in Formal Cryptographic Protocol Analysis. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 10–21. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  20. Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  21. Roscoe, A.W., Reed, G.M., Forster, R.: The Successes and Failures of Behavioural Models. In: Millenial Perspectives in Computer Science (2000)

    Google Scholar 

  22. Ryan, P.Y.A., Schneider, S.A.: Process Algebra and Non-interference. Journal of Computer Security 9, 75–103 (2001)

    Google Scholar 

  23. Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press, Princeton (1994)

    MATH  Google Scholar 

  24. Stravridou, V., Dutertre, B.: From Security to Safety and Back. In: Workshop on Computer Security, Dependability, and Assurance: From Needs to Solutions (CSDA 1998), pp. 182–195. IEEE CS Press, Los Alamitos (1998)

    Google Scholar 

  25. Wittbold, J.T., Johnson, D.M.: Information Flow in Nondeterministic Systems. In: Symp. on Research in Security and Privacy (SSP 1990), pp. 144–161. IEEE CS Press, Los Alamitos (1990)

    Chapter  Google Scholar 

  26. Wu, F., Johnson, H., Nilsson, A.: SOLA: Lightweight Security for Access Control in IEEE 802.11. In: IT Professional, vol. 6, pp. 10–16. IEEE CS Press, Los Alamitos (2004)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Aldini, A., Bernardo, M. (2009). Weak Behavioral Equivalences for Verifying Secure and Performance-Aware Component-Based Systems. In: de Lemos, R., Fabre, JC., Gacek, C., Gadducci, F., ter Beek, M. (eds) Architecting Dependable Systems VI. Lecture Notes in Computer Science, vol 5835. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-10248-6_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-10248-6_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-10247-9

  • Online ISBN: 978-3-642-10248-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics