Skip to main content

Security-By-Contract for the Future Internet

  • Conference paper
Future Internet – FIS 2008 (FIS 2008)

Part of the book series: Lecture Notes in Computer Science ((LNCCN,volume 5468))

Included in the following conference series:

  • 1765 Accesses

Abstract

With the advent of the next generation java servlet on the smartcard, the Future Internet will be composed by web servers and clients silently yet busily running on high end smart cards in our phones and our wallets. In this brave new world we can no longer accept the current security model where programs can be downloaded on our machines just because they are vaguely “trusted”. We want to know what they do in more precise details.

We claim that the Future Internet needs the notion of security-by-contract: In a nutshell, a contract describes the security relevant interactions that the smart internet application could have with the smart devices hosting them. Compliance with contracts should verified at development time, checked at depolyment time and contracts should be accepted by the platform before deployment and possibly their enforcement guaranteed, for instance by in-line monitoring.

In this paper we describe the challenges that must be met in order to develop a security-by-contract framework for the Future Internet and how security research can be changed by it.

Research partly supported by the Projects EU-FP6-IST-STREP-S3MS, EU-FP6-IP-SENSORIA, and EU-FP7-IP-MASTER. We would like to thank Eric Vetillard for pointing to us the domain of Next Generation Java Card as the Challenge for the Future Internet.

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. Channel 4. 4od (2008), http://www.channel4.com/4od/index.html

  2. Aktug, I., Naliuka, K.: Conspec - a formal language for policy specification. In: Proc. of the 1st Workshop on Run Time Enforcement for Mobile and Distributed Systems, REM 2007 (2007)

    Google Scholar 

  3. Atkinson, B., Della-Libera, G., Hada, S., Hondo, M., Hallam-Baker, P., Klein, J., LaMacchia, B., Leach, P., Manferdelli, J., Maruyama, H., Nadalin, A., Nagaratnam, N., Prafullchandra, H., Shewchuk, J., Simon, D.: Web Services Security. Microsoft, IBM, VeriSign, 1st edn (April 2002) (October 25, 2005), http://www-128.ibm.com/developerworks/webservices/library/ws-secure/

  4. Bauer, L., Ligatti, J., Walker, D.: Edit automata: Enforcement mechanisms for run-time security policies. Int. J. of Inform. Sec. 4(1-2), 2–16 (2005)

    Article  Google Scholar 

  5. Bielova, N., Dalla Torre, M., Dragoni, N., Siahaan, I.: Matching policies with security claims of mobile applications. In: Proc. of the 3rd Int. Conf. on Availability, Reliability and Security (ARES 2008). IEEE Press, Los Alamitos (2008)

    Google Scholar 

  6. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)

    Google Scholar 

  7. Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. Formal Methods in Sys. Design 1(2-3), 275–288 (1992)

    Article  MATH  Google Scholar 

  8. Dam, M., Lundblad, A.: A proof carrying code framework for inlined reference monitors in Java bytecode (submitted, 2008)

    Google Scholar 

  9. Della-Libera, G., Gudgin, M., Hallam-Bakerand, P., Hondo, M., Granqvist, H., Kaler, C., Maruyama, H., McIntosh, M., Nadalin, A., Nagaratnam, N., Philpott, R., Prafullchandra, H., Shewchuk, J., Walter, D., Zolfonoon, R.: Web Services Security Policy Language. IBM and Microsoft and RSA Security and VeriSign (2005)

    Google Scholar 

  10. Desmet, L., Joosen, W., Massacci, F., Philippaerts, P., Piessens, F., Siahaan, I., Vanoverberghe, D.: Security-by-contract on the.net platform. Information Security Technical Report 13(1), 25–32 (2008)

    Article  Google Scholar 

  11. Dragoni, N., Massacci, F., Naliuka, K., Siahaan, I.: Security-by-Contract: Toward a Semantics for Digital Signatures on Mobile Code. In: López, J., Samarati, P., Ferrer, J.L. (eds.) EuroPKI 2007. LNCS, vol. 4582, pp. 297–312. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  12. Erlingsson, U., Schneider, F.B.: SASI enforcement of security policies: A retrospective. In: WNSP: New Security Paradigms Workshop. ACM Press, New York (2000)

    Google Scholar 

  13. Erlingsson, U., Schneider, F.B.: IRM enforcement of Java stack inspection. In: IEEE Symposium on Security and Privacy, pp. 246–255 (2000)

    Google Scholar 

  14. Ferrari, G.L., Gnesi, S., Montanari, U., Pistore, M.: A model-checking verification environment for mobile processes. ACM Trans. Softw. Eng. Methodol. 12(4), 440–473 (2003)

    Article  Google Scholar 

  15. Gong, L., Ellison, G., Dageforde, M.: Inside Java 2 Platform Security: Architecture, Api Design, and Implementation. Addison-Wesley Professional, Reading (2003)

    Google Scholar 

  16. Goth, G.: The ins and outs of it outsourcing. IT Professional 1, 11–14 (1999)

    Google Scholar 

  17. Hamlen, K.W., Morrisett, G., Schneider, F.B.: Computability classes for enforcement mechanisms. TOPLAS 28(1), 175–205 (2006)

    Article  Google Scholar 

  18. Handy, C.: Trust and the virtual organization. Harvard Business Review 73, 40–50 (1995)

    Google Scholar 

  19. Hendry, M.: Smart Card Security and Applications, 2nd edn. Artech House (2001)

    Google Scholar 

  20. Howard, M., LeBlanc, D.: Writing Secure Code, 2nd edn. Microsoft Press, Redmond (2002)

    Google Scholar 

  21. Kaminski, M., Francez, N.: Finite-memory automata. Theor. al Comp. Sci. 134(2), 329–363 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  22. Karabulut, Y., Kerschbaum, F., Massacci, F., Robinson, P., Yautsiukhin, A.: Security and trust in it business outsourcing: a manifesto. In: Etalle, S., Samarati, P. (eds.) Proceedings of STM 2006. ENTCS. Elsevier, Amsterdam (2006)

    Google Scholar 

  23. Karjoth, G., Pfitzmann, B., Schunter, M., Waidner, M.: Service-oriented Assurance - Comprehensive Security by Explicit Assurances. In: Proc. of QoP 2005 (2005)

    Google Scholar 

  24. LaMacchia, B., Lange, S.:NET Framework security. Addison Wesley, Reading (2002)

    Google Scholar 

  25. Massacci, F., Siahaan, I.: Matching midlet’s security claims with a platform security policy using automata modulo theory. In: Proc. of The 12th Nordic Workshop on Secure IT Systems, NordSec 2007 (2007)

    Google Scholar 

  26. Massacci, F., Siahaan, I.S.R.: Simulating midlet’s security claims with automata modulo theory. In: Proc. of the 2008 workshop on Prog. Lang. and analysis for security, pp. 1–9. ACM, New York (2008)

    Google Scholar 

  27. Montanari, U., Pistore, M.: History-dependent automata. Technical Report TR-98-11, Dip. Informatica, University of Pisa, 5 (1998)

    Google Scholar 

  28. Necula, G.C.: Proof-carrying code. In: Proc. of the 24th ACM SIGPLAN-SIGACT Symp. on Princ. of Prog. Lang, pp. 106–119. ACM Press, New York (1997)

    Google Scholar 

  29. CNET Networks. Channel 4’s 4od: Tv on demand, at a price. Crave Webzine (January 2007)

    Google Scholar 

  30. Neven, F., Schwentick, T., Vianu, V.: Finite state machines for strings over infinite alphabets. TOCL 5(3), 403–435 (2004)

    Article  MathSciNet  Google Scholar 

  31. Schneider, F.B.: Enforceable security policies. TISSEC 3(1), 30–50 (2000)

    Article  Google Scholar 

  32. Sekar, R., Venkatakrishnan, V.N., Basu, S., Bhatkar, S., DuVarney, D.C.: Model-carrying code: a practical approach for safe execution of untrusted applications. In: Proc. of the 19th ACM Symp. on Operating Sys. Princ., pp. 15–28. ACM Press, New York (2003)

    Google Scholar 

  33. Smans, J., Jacobs, B., Piessens, F.: Static verification of code access security policy compliance of.net applications. Journal of Object Technology 5(3), 35–58 (2006)

    Article  Google Scholar 

  34. Talhi, C., Tawbi, N., Debbabi, M.: Execution monitoring enforcement under memory-limitation constraints. Inform. and Comp. 206(2-4), 158–184 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  35. Vanoverberghe, D., Philippaerts, P., Desmet, L., Joosen, W., Piessens, F., Naliuka, K., Massacci, F.: A flexible security architecture to support third-party applications on mobile devices. In: Proc. of the 1st ACM Comp. Sec. Arch. Workshop (2007)

    Google Scholar 

  36. Vanoverberghe, D., Piessens, F.: A caller-side inline reference monitor for an object-oriented intermediate language. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 240–258. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  37. Vanoverberghe, D., Piessens, F.: Security enforcement aware software development. Information and Software Technology (2008), doi:10.1016/j.infsof.2008.01.009

    Google Scholar 

  38. Veanes, M., Campbell, C., Schulte, W., Tillmann, N.: Online testing with model programs. In: ESEC/FSE-13: Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, pp. 273–282. ACM, New York (2005)

    Chapter  Google Scholar 

  39. Wallach, D.S., Appel, A.W., Felten, E.W.: Safkasi: a security mechanism for language-based systems. ACM Trans. Softw. Eng. Methodol. 9(4), 341–378 (2000)

    Article  Google Scholar 

  40. Yee, B.S.: A sanctuary for mobile agents. In: Vitek, J., Jensen, C.D. (eds.) Secure Internet Programming. LNCS, vol. 1603, pp. 261–273. Springer, Heidelberg (1999)

    Chapter  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 paper

Cite this paper

Massacci, F., Piessens, F., Siahaan, I. (2009). Security-By-Contract for the Future Internet. In: Domingue, J., Fensel, D., Traverso, P. (eds) Future Internet – FIS 2008. FIS 2008. Lecture Notes in Computer Science, vol 5468. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00985-3_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-00985-3_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-00984-6

  • Online ISBN: 978-3-642-00985-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics