Skip to main content

Hybrid Typing of Secure Information Flow in a JavaScript-Like Language

  • Conference paper
  • First Online:

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

Abstract

As JavaScript is highly dynamic by nature, static information flow analyses are often too coarse to deal with the dynamic constructs of the language. To cope with this challenge, we present and prove the soundness of a new hybrid typing analysis for securing information flow in a JavaScript-like language. Our analysis combines static and dynamic typing in order to avoid rejecting programs due to imprecise typing information. Program regions that cannot be precisely typed at static time are wrapped inside an internal boundary statement used by the semantics to interleave the execution of statically verified code with the execution of code that must be dynamically checked.

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

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   34.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   44.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

Learn about institutional subscriptions

References

  1. Bichhawat, A., Rajani, V., Garg, D., Hammer, C.: Information flow control in webkit’s javascript bytecode. In: Abadi, M., Kremer, S. (eds.) POST 2014 (ETAPS 2014). LNCS, vol. 8414, pp. 159–178. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  2. Devriese, D., Piessens, F.: Noninterference through secure multi-execution. In: SP (2010)

    Google Scholar 

  3. Disney, T., Flanagan, C.: Gradual information flow typing. In: STOP (2011)

    Google Scholar 

  4. Fennell, L., Thiemann, P.: Gradual security typing with references. In: CSF (2013)

    Google Scholar 

  5. Flanagan, C.: Hybrid type checking. In: POPL (2006)

    Google Scholar 

  6. De Groef, W., Devriese, D., Nikiforakis, N., Piessens, F.: Flowfox: a web browser with flexible and precise information flow control. In: CCS (2012)

    Google Scholar 

  7. Hedin, D., Birgisson, A., Bello, L., Sabelfeld, A.: JSFlow: tracking information flow in JavaScript and its APIs. In: SAC (2014)

    Google Scholar 

  8. Hedin, D., Sabelfeld, A.: Information-flow security for a core of JavaScript. In: CSF (2012)

    Google Scholar 

  9. Maffeis, S., Taly, A.: Language-based isolation of untrusted JavaScript. In: CSF (2009)

    Google Scholar 

  10. Matthews, J., Findler, R.B.: Operational semantics for multi-language programs. In: ACM TOPLAS (2009)

    Google Scholar 

  11. Microsoft. TypeScript language specification. Technical report, Microsoft (2014)

    Google Scholar 

  12. Rastogi, A., Swamy, N., Fournet, C., Bierman, G., Vekris, P.: Safe & efficient gradual typing for TypeScript. In: POPL (2015)

    Google Scholar 

  13. Russo, A., Sabelfeld, A.: Dynamic vs. static flow-sensitive security analysis. In: CSF (2010)

    Google Scholar 

  14. Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5–19 (2003)

    Article  Google Scholar 

  15. Santos, J.F.: Online materials - hybrid type system 2015. http://www.doc.ic.ac.uk/~jfaustin

  16. Santos, J.F., Rezk, T.: An information flow monitor-inlining compiler for securing a core of javascript. In: Cuppens-Boulahia, N., Cuppens, F., Jajodia, S., Abou El Kalam, A., Sans, T. (eds.) SEC 2014. IFIP AICT, vol. 428, pp. 278–292. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  17. Thiemann, P.: Towards a type system for analyzing javascript programs. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 408–422. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  18. Volpano, D.M., Irvine, C.E., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2), 167–187 (1996)

    Google Scholar 

  19. Wright, A., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38–94 (1994)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgments

We acknowledge funding from the EPSRC grant reference EP/K032089/1 (Fragoso Santos) and the ANR project AJACS ANR-14-CE28-0008 (Jensen, Rezk, and Schmitt). No new data was collected in the course of this research.

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to José Fragoso Santos .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Fragoso Santos, J., Jensen, T., Rezk, T., Schmitt, A. (2016). Hybrid Typing of Secure Information Flow in a JavaScript-Like Language. In: Ganty, P., Loreti, M. (eds) Trustworthy Global Computing. TGC 2015. Lecture Notes in Computer Science(), vol 9533. Springer, Cham. https://doi.org/10.1007/978-3-319-28766-9_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-28766-9_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-28765-2

  • Online ISBN: 978-3-319-28766-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics