nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Enforcing Programming Guidelines with Region Types and Effects

verfasst von : Serdar Erbatur, Martin Hofmann, Eugen Zălinescu

Erschienen in: Programming Languages and Systems

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We present in this paper a new type and effect system for Java which can be used to ensure adherence to guidelines for secure web programming. The system is based on the region and effect system by Beringer, Grabowski, and Hofmann. It improves upon it by being parametrized over an arbitrary guideline supplied in the form of a finite monoid or automaton and a type annotation or mockup code for external methods. Furthermore, we add a powerful type inference based on precise interprocedural analysis and provide an implementation in the Soot framework which has been tested on a number of benchmarks including large parts of the Stanford SecuriBench.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Capabilities for Java: Secure Access to Resources

Nächstes Kapitel Automatically Generating Secure Wrappers for SGX Enclaves from Separation Logic Specifications

Alternatively, the monoid can be generated automatically from the policy automaton (or its complement).

In Java, the \(\mathtt {NullType}\) is the type of the expression \(\mathtt {null}\), see https://docs.oracle.com/javase/specs/jls/se7/html/jls-4.html#jls-4.1.

Note that such a class always exists, as \(C\preceq \mathtt {Object}\), for any \(C\in {\textit{Cls}}\).

The implementation is available for download from one of the authors’ homepage.

https://suif.stanford.edu/~livshits/work/securibench-micro/.

https://suif.stanford.edu/~livshits/work/securibench/.

As usual, the formal description of our analysis is in terms of an idealized language, FJEUCS. The implementation takes genuine Java programs. However, it does not support certain features such as concurrency and reflection, which we discuss below.

Checkmarx. https://www.checkmarx.com

Coverity. http://www.coverity.com

Fortify. https://software.microfocus.com/en-us/software/sca

IBM AppScan. http://www.ibm.com/software/products/en/appscan-source

Barthe, G., et al.: MOBIUS: mobility, ubiquity, security. In: Montanari, U., Sannella, D., Bruni, R. (eds.) TGC 2006. LNCS, vol. 4661, pp. 10–29. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75336-0_2 CrossRef

Beringer, L., Grabowski, R., Hofmann, M.: Verifying pointer and string analyses with region type systems. Comput. Lang. Syst. Struct. 39(2), 49–65 (2013)MATH

Chess, B., West, J.: Secure Programming with Static Analysis, 1st edn. Addison-Wesley Professional, Erewhon (2007)

Christensen, A.S., Møller, A., Schwartzbach, M.I.: Precise analysis of string expressions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 1–18. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-44898-5_1 CrossRef

Crégut, P., Alvarado, C.: Improving the security of downloadable Java applications with static analysis. ENTCS 141(1), 129–144 (2005)

10.

Degen, M.: JAVA(X) a type-based program analysis framework. Ph.D. thesis, Universität Freiburg, June 2011

11.

Degen, M., Thiemann, P., Wehr, S.: Tracking linear and affine resources with Java(X). In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 550–574. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73589-2_26 CrossRef

12.

DeLine, R., Fähndrich, M.: Typestates for objects. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 465–490. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24851-4_21 CrossRef

13.

Grabowski, R., Hofmann, M., Li, K.: Type-based enforcement of secure programming guidelines — code injection prevention at SAP. In: Barthe, G., Datta, A., Etalle, S. (eds.) FAST 2011. LNCS, vol. 7140, pp. 182–197. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29420-4_12 CrossRef

14.

Hofmann, M., Chen, W.: Abstract interpretation from Büchi automata. In: CSL-LICS, pp. 51:1–51:10 (2014)

15.

Hofmann, M., Jost, S.: Type-based amortised heap-space analysis. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 22–37. Springer, Heidelberg (2006). https://doi.org/10.1007/11693024_3 CrossRef

16.

Hofmann, M., Ledent, J.: A cartesian-closed category for higher-order model checking. In: LICS, pp. 1–12 (2017)

17.

Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst. 23(3), 396–450 (2001)CrossRef

18.

Kaminski, M., Francez, N.: Finite-memory automata. Theoret. Comput. Sci. 134(2), 329–363 (1994)MathSciNetCrossRefMATH

19.

Kobayashi, N., Ong, C.L.: A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In: LICS, pp. 179–188. IEEE Computer Society (2009)

20.

Lam, P., Bodden, E., Lhoták, O., Hendren, L.: The Soot framework for Java program analysis: a retrospective. In: CETUS (2011)

21.

Lenherr, T.: Taxonomy and applications of alias analysis. Master’s thesis, ETH Zürich (2008)

22.

Lhoták, O.: Program analysis using binary decision diagrams. Ph.D. thesis, McGill University, January 2006

23.

Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)CrossRefMATH

24.

Reps, T.W., Horwitz, S., Sagiv, S.: Precise interprocedural dataflow analysis via graph reachability. In: POPL, pp. 49–61. ACM Press (1995)

25.

Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Muchnick, S.S., Jones, N.D. (eds.) Program Flow Analysis - Theory and Applications, pp. 189–233. Prentice-Hall, Englewood Cliffs (1981)

26.

Skalka, C.: Types and trace effects for object orientation. High.-Order Symbolic Comput. 21(3), 239–282 (2008)CrossRefMATH

27.

Skalka, C., Smith, S.F., Horn, D.V.: A type and effect system for flexible abstract interpretation of Java. ENTCS 131, 111–124 (2005)

28.

Skalka, C., Smith, S.F., Horn, D.V.: Types and trace effects of higher order programs. J. Funct. Program. 18(2), 179–249 (2008)MathSciNetCrossRefMATH

29.

Smaragdakis, Y., Bravenboer, M., Lhoták, O.: Pick your contexts well: understanding object-sensitivity. In: POPL, pp. 17–30 (2011)

30.

Vallée-Rai, R., Co, P., Gagnon, E., Hendren, L.J., Lam, P., Sundaresan, V.: Soot - a Java bytecode optimization framework. In: CASCON, IBM (1999)

Titel: Enforcing Programming Guidelines with Region Types and Effects
verfasst von: Serdar Erbatur
Martin Hofmann
Eugen Zălinescu
Verlag: Springer International Publishing
Buch: Programming Languages and Systems
Print ISBN: 978-3-319-71236-9

Electronic ISBN: 978-3-319-71237-6

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-71237-6_5

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner