DROPS

Document

DOI: 10.4230/LIPIcs.ECOOP.2016.9

LJGS: Gradual Security Types for Object-Oriented Languages

Authors: Luminous Fennell and Peter Thiemann

Published in: LIPIcs, Volume 56, 30th European Conference on Object-Oriented Programming (ECOOP 2016)

Abstract

LJGS is a lightweight Java core calculus with a gradual security type system. The calculus guarantees secure information flow for sequential, class-based, typed object-oriented programming with mutable objects and virtual method calls. An LJGS program is composed of fragments that are checked either statically or dynamically. Statically checked fragments adhere to a security type system so that they incur no run-time penalty whereas dynamically checked fragments rely on run-time security labels. The programmer marks the boundaries between static and dynamic checking with casts so that it is always clear whether a program fragment requires run-time checks. LJGS requires security annotations on fields and methods. A field annotation either specifies a fixed static security level or it prescribes dynamic checking. A method annotation specifies a constrained polymorphic security signature. The types of local variables in method bodies are analyzed flow-sensitively and require no annotation. The dynamic checking of fields relies on a static points-to analysis to approximate implicit flows. We prove type soundness and non-interference for LJGS.

Cite as

Luminous Fennell and Peter Thiemann. LJGS: Gradual Security Types for Object-Oriented Languages. In 30th European Conference on Object-Oriented Programming (ECOOP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 56, pp. 9:1-9:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{fennell_et_al:LIPIcs.ECOOP.2016.9,
  author =	{Fennell, Luminous and Thiemann, Peter},
  title =	{{LJGS: Gradual Security Types for Object-Oriented Languages}},
  booktitle =	{30th European Conference on Object-Oriented Programming (ECOOP 2016)},
  pages =	{9:1--9:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-014-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{56},
  editor =	{Krishnamurthi, Shriram and Lerner, Benjamin S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2016.9},
  URN =		{urn:nbn:de:0030-drops-61031},
  doi =		{10.4230/LIPIcs.ECOOP.2016.9},
  annote =	{Keywords: gradual typing, security typing, Java, hybrid information flow control}
}

Document

DOI: 10.4230/DARTS.2.1.4

LJGS: Gradual Security Types for Object-Oriented Languages (Artifact)

Authors: Luminous Fennell and Peter Thiemann

Published in: DARTS, Volume 2, Issue 1, Special Issue of the 30th European Conference on Object-Oriented Programming (ECOOP 2016)

Abstract

JGS-check is the accompanying artifact to "LJGS: Gradual Security Types for Object-Oriented Languages". LJGS is a Java-like language with gradual security typing. It features a constraint based information flow type system that includes a type dynamic and type casts. Dynamically typed fragments are liberally accepted by the type checker and rely on run-time enforcement for security. JGS-check is a type checker for the subset of Java that corresponds to the calculus presented in the paper and that implements the constraint generation and satisfiability checks of LJGS' type system. It's purpose is to illustrate and substantiate the behavior of our gradual security type system. It takes a directory of Java source code as input and reports methods that violate the typing rules. JGS-check is merely a type checker and does not implement code generation. The submission archive includes the compiled type checker, the code of the example section (Section 2) as well additional examples and testcases that did not fit into the paper. The user should also be able to check custom code as long as it corresponds the subset of Java that is covered by LJGS.

Cite as

Luminous Fennell and Peter Thiemann. LJGS: Gradual Security Types for Object-Oriented Languages (Artifact). In Special Issue of the 30th European Conference on Object-Oriented Programming (ECOOP 2016). Dagstuhl Artifacts Series (DARTS), Volume 2, Issue 1, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{fennell_et_al:DARTS.2.1.4,
  author =	{Fennell, Luminous and Thiemann, Peter},
  title =	{{LJGS: Gradual Security Types for Object-Oriented Languages (Artifact)}},
  pages =	{4:1--4:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2016},
  volume =	{2},
  number =	{1},
  editor =	{Fennell, Luminous and Thiemann, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.2.1.4},
  URN =		{urn:nbn:de:0030-drops-61253},
  doi =		{10.4230/DARTS.2.1.4},
  annote =	{Keywords: gradual typing, security typing, Java, hybrid information flow control}
}

Search Results

Documents authored by Fennell, Luminous

LJGS: Gradual Security Types for Object-Oriented Languages

Abstract

Cite as

LJGS: Gradual Security Types for Object-Oriented Languages (Artifact)

Abstract

Cite as

Thanks for your feedback!

Could not send message