Abstract
In the challenge of ensuring the correct behaviour of legacy implementations of security protocols, a formally-based approach is presented to design and implement monitors that stop insecure protocol runs executed by such legacy implementations, without the need of their source code. We validate the approach at a case study about monitoring several SSL legacy implementations. Recently, a security bug has been found in the widely deployed OpenSSL client; our case study shows that our monitor correctly stops the protocol runs otherwise allowed by the faulty OpenSSL client. Moreover, our monitoring approach allowed us to detect a new flaw in another open source SSL client implementation.
This research was partially supported by the EU project SecureChange (ICT-FET-231101).
This is a preview of subscription content, log in via an institution to check access.
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
Abadi, M., Fournet, C., Gonthier, G.: Secure implementation of channel abstractions. Information and Computation 174(1), 37–83 (2002)
Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The Spi Calculus. Digital Research Report 149 (1998)
Bauer, A., Jürjens, J.: Security protocols, properties, and their monitoring. In: International Workshop on Software Engineering for Secure Systems, pp. 33–40 (2008)
Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. In: Computer Security Foundations Symposium, pp. 17–32. IEEE, Los Alamitos (2008)
Bhargavan, K., Fournet, C., Gordon, A.D., Tse, S.: Verified interoperable implementations of security protocols. In: Computer Security Foundations Workshop, pp. 139–152 (2006)
Dolev, D., Yao, A.C.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–207 (1983)
Fraser, T., Badger, L., Feldman, M.: Hardening COTS software with generic software wrappers. In: IEEE Symposium on Security and Privacy, pp. 2–16 (1999)
Hubbers, E., Oostdijk, M., Poll, E.: Implementing a formally verifiable security protocol in Java Card. In: Hutter, D., Müller, G., Stephan, W., Ullmann, M. (eds.) Security in Pervasive Computing. LNCS, vol. 2802, pp. 213–226. Springer, Heidelberg (2004)
Jeon, C.W., Kim, I.G., Choi, J.Y.: Automatic generation of the C# code for security protocols verified with Casper/FDR. In: International Conference on Advanced Information Networking and Applications, pp. 507–510 (2005)
Joglekar, S.P., Tate, S.R.: ProtoMon: Embedded monitors for cryptographic protocol intrusion detection and prevention. Journal of Universal Computer Science 11(1), 83–103 (2005)
Jürjens, J., Yampolskiy, M.: Code security analysis with assertions. In: IEEE/ACM International Conference on Automated Software Engineering, pp. 392–395 (2005)
Pironti, A., Jürjens, J.: Online resources about black-box monitoring, http://alfredo.pironti.eu/research/projects/monitoring/
Pironti, A., Sisto, R.: An experiment in interoperable cryptographic protocol implementation using automatic code generation. In: IEEE Symposium on Computers and Communications, pp. 839–844 (2007)
Pironti, A., Sisto, R.: Provably correct Java implementations of Spi Calculus security protocols specifications. Computers & Security (2009) (in press)
Roscoe, A.W., Hoare, C.A.R., Bird, R.: The Theory and Practice of Concurrency. Prentice Hall PTR, Englewood Cliffs (1997)
Schneider, S.: Security properties and CSP. In: IEEE Symposium on Security and Privacy, pp. 174–187 (1996)
Süßkraut, M., Fetzer, C.: Robustness and security hardening of COTS software libraries. In: IEEE/IFIP International Conference on Dependable Systems and Networks, pp. 61–71 (2007)
Viganò, L.: Automated security protocol analysis with the AVISPA tool. Electronic Notes on Theoretical Computer Science 155, 61–86 (2006)
Voydock, V.L., Kent, S.T.: Security mechanisms in high-level network protocols. ACM Computing Surveys 15(2), 135–171 (1983)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pironti, A., Jürjens, J. (2010). Formally-Based Black-Box Monitoring of Security Protocols. In: Massacci, F., Wallach, D., Zannone, N. (eds) Engineering Secure Software and Systems. ESSoS 2010. Lecture Notes in Computer Science, vol 5965. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11747-3_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-11747-3_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11746-6
Online ISBN: 978-3-642-11747-3
eBook Packages: Computer ScienceComputer Science (R0)