Abstract
In this work, we investigate the combination of controller synthesis and test generation techniques for the testing of open, partially observable systems with respect to security policies. We consider two kinds of properties: integrity properties and confidentiality properties. We assume that the behavior of the system is modeled by a labeled transition system and assume the existence of a black-box implementation. We first outline a method allowing to automatically compute an ideal access control ensuring these two kinds of properties. Then, we show how to derive testers that test the conformance of the implementation with respect to its specification, the correctness of the real access control that has been composed with the implementation in order to ensure a security property, and the security property itself.
This work was partially supported by the Politess RNRT project.
Chapter PDF
Similar content being viewed by others
References
Alur, R., Černý, P., Zdancewic, S.: Preserving secrecy under refinement. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 107–118. Springer, Heidelberg (2006)
Badouel, E., Bednarczyk, M., Borzyszkowski, A., Caillaud, B., Darondeau, P.: Concurrent secrets. Discrete Event Dynamic Systems 17, 425–446 (2007)
Bishop, M.: Introduction to computer security. Addison-Wesley Professional, Reading (2004)
Blanchet, B., Abadi, M., Fournet, C.: Automated Verification of Selected Equivalences for Security Protocols. In: 20th IEEE Symposium on Logic in Computer Science (LICS 2005), Chicago, IL, June 2005, pp. 331–340 (2005)
Bryans, J.W., Koutny, M., Mazaré, L., Ryan, P.: Opacity generalised to transition systems. International Journal of Information Security 7(6), 421–435 (2008)
Cassandras, C., Lafortune, S.: Introduction to Discrete Event Systems. Kluwer Academic Publishers, Dordrecht (1999)
Constant, C., Jéron, T., Marchand, H., Rusu, V.: Integrating formal verification and conformance testing for reactive systems. IEEE Transactions on Software Engineering 33(8), 558–574 (2007)
Darmaillacq, V., Fernandez, J.-C., Groz, R., Mounier, L., Richier, J.-L.: Test generation for network security rules. In: Uyar, M.Ü., Duale, A.Y., Fecko, M.A. (eds.) TestCom 2006. LNCS, vol. 3964, pp. 341–356. Springer, Heidelberg (2006)
Dubreil, J., Darondeau, Ph., Marchand, H.: Opacity enforcing control synthesis. In: Workshop on Discrete Event Systems, WODES 2008, Gothenburg, Sweden (2008)
Dubreil, J., Darondeau, Ph., Marchand, H.: Supervisory control for opacity. Technical Report 1921, IRISA (February 2009)
Dubreil, J., Jéron, T., Marchand, H.: Monitoring information flow by diagnosis techniques. In: European Control Conference, ECC (August 2009)
Giacobazzi, R., Mastroeni, I.: Abstract non-interference: parameterizing non-interference by abstract interpretation. In: POPL 2004: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 186–197. ACM, New York (2004)
Lowe, G.: Towards a completeness result for model checking of security protocols. Journal of Computer Security 7(2-3), 89–146 (1999)
Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3(1), 30–50 (2000)
Tretmans, J.: Testing concurrent systems: A formal approach. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 46–65. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Marchand, H., Dubreil, J., Jéron, T. (2009). Automatic Testing of Access Control for Security Properties. In: Núñez, M., Baker, P., Merayo, M.G. (eds) Testing of Software and Communication Systems. FATES TestCom 2009 2009. Lecture Notes in Computer Science, vol 5826. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-05031-2_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-05031-2_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-05030-5
Online ISBN: 978-3-642-05031-2
eBook Packages: Computer ScienceComputer Science (R0)