Advertisement

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

  • José Fragoso SantosEmail author
  • Thomas Jensen
  • Tamara Rezk
  • Alan Schmitt
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, 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.

Keywords

Security Level Typing Environment Context Level Typing Judgement Environment Record 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Notes

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.

References

  1. 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)CrossRefGoogle Scholar
  2. 2.
    Devriese, D., Piessens, F.: Noninterference through secure multi-execution. In: SP (2010)Google Scholar
  3. 3.
    Disney, T., Flanagan, C.: Gradual information flow typing. In: STOP (2011)Google Scholar
  4. 4.
    Fennell, L., Thiemann, P.: Gradual security typing with references. In: CSF (2013)Google Scholar
  5. 5.
    Flanagan, C.: Hybrid type checking. In: POPL (2006)Google Scholar
  6. 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. 7.
    Hedin, D., Birgisson, A., Bello, L., Sabelfeld, A.: JSFlow: tracking information flow in JavaScript and its APIs. In: SAC (2014)Google Scholar
  8. 8.
    Hedin, D., Sabelfeld, A.: Information-flow security for a core of JavaScript. In: CSF (2012)Google Scholar
  9. 9.
    Maffeis, S., Taly, A.: Language-based isolation of untrusted JavaScript. In: CSF (2009)Google Scholar
  10. 10.
    Matthews, J., Findler, R.B.: Operational semantics for multi-language programs. In: ACM TOPLAS (2009)Google Scholar
  11. 11.
    Microsoft. TypeScript language specification. Technical report, Microsoft (2014)Google Scholar
  12. 12.
    Rastogi, A., Swamy, N., Fournet, C., Bierman, G., Vekris, P.: Safe & efficient gradual typing for TypeScript. In: POPL (2015)Google Scholar
  13. 13.
    Russo, A., Sabelfeld, A.: Dynamic vs. static flow-sensitive security analysis. In: CSF (2010)Google Scholar
  14. 14.
    Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5–19 (2003)CrossRefGoogle Scholar
  15. 15.
    Santos, J.F.: Online materials - hybrid type system 2015. http://www.doc.ic.ac.uk/~jfaustin
  16. 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)CrossRefGoogle Scholar
  17. 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)CrossRefGoogle Scholar
  18. 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. 19.
    Wright, A., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38–94 (1994)CrossRefMathSciNetzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • José Fragoso Santos
    • 1
    Email author
  • Thomas Jensen
    • 2
  • Tamara Rezk
    • 2
  • Alan Schmitt
    • 2
  1. 1.Imperial College LondonLondonUK
  2. 2.InriaSophia AntipolisFrance

Personalised recommendations