Skip to main content
SpringerLink
Log in

Static Enforcement of Information Flow Policies for a Concurrent JVM-like Language

  • Conference paper
Trustworthy Global Computing (TGC 2011)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7173))

Included in the following conference series:

Abstract

An essential security goal of mobile code platforms is to protect confidential data against untrusted third-party applications; yet, prevailing mechanisms for ensuring confidentiality of mobile code are limited to sequential programs, whereas existing applications are generally concurrent. To bridge this gap, we develop a sound information-flow type system for a JVM-like, low-level concurrent object-oriented language. The type system builds upon existing solutions for object-oriented languages and concurrency, solving a number of intricate issues in their combination. Moreover, we connect the type system for bytecode programs to a type system for Java programs, extending the results of type-preserving compilation developed in earlier works.

Partially funded by European Projects FP7-231620 HATS and FP7-256980 NESSoS, Spanish project TIN2009-14599 DESAFIOS 10, Madrid Regional project S2009TIC-1465 PROMETIDOS.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.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. Banerjee, A., Naumann, D.: Stack-based access control for secure information flow. Journal of Functional Programming 15, 131–177 (2005); Special Issue on Language-Based Security

    Article  MathSciNet  MATH  Google Scholar 

  2. Barthe, G., Cavadini, S., Rezk, T.: Tractable enforcement of declassification policies. In: IEEE Computer Security Foundations Symposium (June 2008)

    Google Scholar 

  3. Barthe, G., Naumann, D., Rezk, T.: Deriving an information flow checker and certifying compiler for Java. In: Symposium on Security and Privacy. IEEE Press (2006)

    Google Scholar 

  4. Barthe, G., Pichardie, D., Rezk, T.: A Certified Lightweight Non-interference Java Bytecode Verifier. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 125–140. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  5. Barthe, G., Rezk, T., Russo, A., Sabelfeld, A.: Security of multithreaded programs by compilation. ACM Trans. Inf. Syst. Secur. 13(3) (2010)

    Google Scholar 

  6. Le Guernic, G.: Automaton-based confidentiality monitoring of concurrent programs. In: CSF, pp. 218–232. IEEE Computer Society (2007)

    Google Scholar 

  7. Le Guernic, G., Banerjee, A., Jensen, T., Schmidt, D.A.: Automata-Based Confidentiality Monitoring. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 75–89. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  8. Kobayashi, N., Shirane, K.: Type-based information analysis for low-level languages. In: Asian Programming Languages and Systems Symposium, pp. 302–316 (2002)

    Google Scholar 

  9. Myers, A.C.: JFlow: Practical mostly-static information flow control. In: Principles of Programming Languages, pp. 228–241. ACM Press (1999), Ongoing development at http://www.cs.cornell.edu/jif/

  10. Nair, S.K., Simpson, P.N.D., Crispo, B., Tanenbaum, A.S.: A virtual machine based information flow control system for policy enforcement. Electr. Notes Theor. Comput. Sci. 197(1), 3–16 (2008)

    Article  Google Scholar 

  11. Rezk, T.: Verification of confidentiality policies for mobile code. PhD thesis, Université de Nice Sophia-Antipolis (2006)

    Google Scholar 

  12. Russo, A., Sabelfeld, A.: Securing interaction between threads and the scheduler. In: Computer Security Foundations Workshop, pp. 177–189 (2006)

    Google Scholar 

  13. Russo, A., Sabelfeld, A.: Security for Multithreaded Programs Under Cooperative Scheduling. In: Virbitskaite, I., Voronkov, A. (eds.) PSI 2006. LNCS, vol. 4378, pp. 474–480. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  14. Smith, G., Volpano, D.: Secure Information Flow in a Multi-threaded Imperative Language. In: Principles of Programming Languages, pp. 355–364 (1998)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IMDEA Software Institute, Madrid, Spain

    Gilles Barthe & Exequiel Rivas

Authors
  1. Gilles Barthe
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Exequiel Rivas
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Science Department, University of Pisa, Largo Bruno Pontecorvo 3, 56127, Pisa, Italy

    Roberto Bruni

  2. ECS, University of Southampton, University Road, SO17 1BJ, Southampton, UK

    Vladimiro Sassone

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Barthe, G., Rivas, E. (2012). Static Enforcement of Information Flow Policies for a Concurrent JVM-like Language. In: Bruni, R., Sassone, V. (eds) Trustworthy Global Computing. TGC 2011. Lecture Notes in Computer Science, vol 7173. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30065-3_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-30065-3_5

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation