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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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)
Aldini, A.: Classification of security properties in a Linda-like process algebra. Journal of Science of Computer Programming 63, 16–38 (2006)
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)
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)
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)
Aldini, A., Bravetti, M., Gorrieri, R.: A Process-Algebraic Approach for the Analysis of Probabilistic Noninterference. Journal of Computer Security 12, 191–245 (2004)
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)
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)
Bernardo, M.: TwoTowers 5.1 User Manual (2006), http://www.sti.uniurb.it/bernardo/twotowers/
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)
Bravetti, M., Aldini, A.: Discrete Time Generative-Reactive Probabilistic Processes with Different Advancing Speeds. Theoretical Computer Science 290, 355–406 (2003)
Focardi, R., Gorrieri, R.: A Classification of Security Properties. Journal of Computer Security 3, 5–33 (1995)
van Glabbeek, R.J., Smolka, S.A., Steffen, B.: Reactive, Generative and Stratified Models of Probabilistic Processes. Information and Computation 121, 59–80 (1995)
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)
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)
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)
Howard, R.A.: Dynamic Probabilistic Systems. John Wiley & Sons, Chichester (1971)
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)
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)
Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)
Roscoe, A.W., Reed, G.M., Forster, R.: The Successes and Failures of Behavioural Models. In: Millenial Perspectives in Computer Science (2000)
Ryan, P.Y.A., Schneider, S.A.: Process Algebra and Non-interference. Journal of Computer Security 9, 75–103 (2001)
Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press, Princeton (1994)
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)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)