3 Search Results for "Fennell, Luminous"


Document
SCICO Journal-first
Abstracting Gradual References (SCICO Journal-first)

Authors: Matías Toro and Éric Tanter

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)


Abstract
Gradual typing is an effective approach to integrate static and dynamic typing, which supports the smooth transition between both extremes via the (programmer-controlled) precision of type annotations [Jeremy Siek and Walid Taha, 2006; Siek et al., 2015]. Imprecision is normally introduced via the unknown type ?, e.g. function type Int → Bool is more precise than ? → ?, and both more precise than ?. Gradual typing relates types of different precision using consistent type relations, such as type consistency (resp. consistent subtyping), the gradual counterpart of type equality (resp. subtyping). For instance, ? → Int is consistent with Bool → ?. This approach has been applied in a number of settings, such as objects [Jeremy Siek and Walid Taha, 2007], subtyping [Jeremy Siek and Walid Taha, 2007; Ronald Garcia et al., 2016], effects [Bañados Schwerter et al., 2014; Bañados Schwerter et al., 2016], ownership [Ilya Sergey and Dave Clarke, 2012], typestates [Roger Wolff et al., 2011; Ronald Garcia et al., 2014], information-flow typing [Tim Disney and Cormac Flanagan, 2011; Luminous Fennell and Peter Thiemann, 2013; Matías Toro et al., 2018], session types [Igarashi et al., 2017], refinements [Nico Lehmann and {É}ric Tanter, 2017], set-theoretic types [Castagna and Lanvin, 2017], Hoare logic [Johannes Bader et al., 2018], parametric polymorphism [Amal Ahmed et al., 2011; Ahmed et al., 2017; Ina and Igarashi, 2011; Igarashi et al., 2017; Ningning Xie et al., 2018; Matías Toro et al., 2019], and references [Jeremy Siek and Walid Taha, 2006; Herman et al., 2010; Siek et al., 2015]. In particular, gradual typing for mutable references has seen the elaboration of various possible semantics: invariant references [Jeremy Siek and Walid Taha, 2006], guarded references [Herman et al., 2010], monotonic references [Siek et al., 2015], and permissive references [Siek et al., 2015]. Invariant references are a form of references where reference types are invariant with respect to type consistency. Guarded references admit variance thanks to systematic runtime checks on reference reads and writes; the runtime type of an allocated cell never changes during execution. Guarded references have been formulated in a space-efficient coercion calculus, which ensures that gradual programs do not accumulate unbounded pending checks during execution. Hereafter, we refer to this language as HCC. Monotonic references favor efficiency over flexibility by only allowing reference cells to vary towards more precise types. This allows reference operations in statically-typed regions to safely proceed without any runtime checks. Permissive references are the most flexible approach, in which reference cells can be initialized and updated to any value of any type at any time. These four developments reflect different design decisions with respect to gradual references: is the reference type constructor variant under consistency? Can the programmer specify a precise bound on the static type of a reference, and hence on the corresponding heap cell type? Can the heap cell type evolve its precision at runtime, and if yes, how? There is obviously no absolute answer to these questions, as they reflect different tradeoffs such as in efficiency and precision. This work explores the semantics that results from the application of a systematic methodology to gradualize static type systems. Currently we can find in the literature two methodologies to gradualize statically-typed languages: Abstracting Gradual Typing (AGT) [Ronald Garcia et al., 2016], and the Gradualizer [Matteo Cimini and Jeremy Siek, 2016]. In this work, we consider the AGT methodology as it naturally scales to auxiliary structures such as a mutable heap. The AGT methodology helps to systematically construct gradually-typed languages by using abstract interpretation [Cousot and Cousot, 1977] at the type level. In brief, AGT interprets gradual types as an abstraction of sets of possible static types, formally captured through a Galois connection. The static semantics of a gradual language are then derived by lifting the semantics of a statically-typed language through this connection, and the dynamic semantics follow by Curry-Howard from proof normalization of the type safety argument. The AGT methodology has been shown to be effective in many contexts: records and subtyping [Ronald Garcia et al., 2016], type-and-effects [Bañados Schwerter et al., 2014; Bañados Schwerter et al., 2016], refinement types [Nico Lehmann and Éric Tanter, 2017; Niki Vazou et al., 2018], set-theoretic and union types [Castagna and Lanvin, 2017; Matías Toro and Éric Tanter, 2017], information-flow typing [Matías Toro et al., 2018], and parametric polymorphism [Matías Toro et al., 2019]. However, this methodology has never been applied to mutable references in isolation. Although Toro et al. [Matías Toro et al., 2018] apply AGT to a language with references, they only gradualize security levels of types (e.g. Ref Int_?), not whole types (e.g. Ref ? is not supported). In this article we answer the following open questions: Which semantics for gradually-type references follows by systematically applying AGT? Does AGT justify one of the existing approaches, or does it suggest yet another design? Can we recover other semantics for gradual references, if yes, how? This article first reviews the different existing gradual approaches to mutable references through examples. It then presents the semantics for gradual references that is obtained by applying AGT, and how to accommodate the other semantics. More specifically, this work makes the following contributions: - We present λ_REF~, a gradual language with support for mutable references. We derive λ_REF~ by applying the AGT methodology to a fully-static simple language with mutable references called λ_REF. This is the first application of AGT that focuses on gradually-typed mutable references. - We prove that λ_REF~ satisfies the gradual guarantee of Siek et al. [Siek et al., 2015]. We also present the first formal statement and proof of the conservative extension of the dynamic semantics of the static language [Siek et al., 2015], for a gradual language derived using AGT. - We prove that the derived language, λ_REF~, corresponds to the semantics of guarded references from HCC. Formally, given a λ_REF~ term and its compilation to HCC^+ (an adapted version of HCC extended with conditionals and binary operations) we prove that both terms are bisimilar, and that consequently they either both terminate, both fail, or both diverge. - We observe that λ_REF~ and HCC^+ differ in the order of combination of runtime checks. As a result, HCC is space efficient whereas λ_REF~ is not: we can write programs in λ_REF~ that may accumulate an unbounded number of checks. We formalize the changes needed in the dynamic semantics of λ_REF~ to achieve space efficiency. This technique to recover space efficiency is in fact independent from mutable references, and is therefore applicable to other gradual languages derived with AGT. - We formally describe how to support other gradual reference semantics in λ_REF~ by presenting λ_REF~^𝗉𝗆, an extension that additionally supports both permissive and monotonic references. Finally, we prove for the first time that monotonic references satisfy the dynamic gradual guarantee, a non-trivial result that requires careful consideration of updates to the store. Additionally, we implemented λ_REF~ as an interactive prototype that displays both typing derivations and reduction traces. All the examples mentioned in this paper are readily available in the online prototype available at https://pleiad.cl/grefs. As a result, this paper sheds further light on the design space of gradual languages with mutable references and contributes to deepening the understanding of the AGT methodology.

Cite as

Matías Toro and Éric Tanter. Abstracting Gradual References (SCICO Journal-first). In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 33:1-33:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{toro_et_al:LIPIcs.ECOOP.2020.33,
  author =	{Toro, Mat{\'\i}as and Tanter, \'{E}ric},
  title =	{{Abstracting Gradual References}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{33:1--33:4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.33},
  URN =		{urn:nbn:de:0030-drops-131900},
  doi =		{10.4230/LIPIcs.ECOOP.2020.33},
  annote =	{Keywords: Gradual Typing, Mutable References, Abstract interpretation}
}
Document
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
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}
}
  • Refine by Author
  • 2 Fennell, Luminous
  • 2 Thiemann, Peter
  • 1 Tanter, Éric
  • 1 Toro, Matías

  • Refine by Classification
  • 1 Theory of computation → Program semantics
  • 1 Theory of computation → Type structures

  • Refine by Keyword
  • 2 Java
  • 2 gradual typing
  • 2 hybrid information flow control
  • 2 security typing
  • 1 Abstract interpretation
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 2 2016
  • 1 2020