Write a Blog >>
APLAS 2019
Sun 1 - Wed 4 December 2019 Bali, Indonesia
Mon 2 Dec 2019 11:30 - 12:00 at Bali Room - Types Chair(s): Tachio Terauchi

Information-flow security type systems ensure confidentiality by enforcing noninterference: a program cannot leak private data to public channels. However, in practice, programs need to selectively declassify information about private data. Several approaches have provided a notion of relaxed noninterference, supporting selective and expressive declassification while retaining a formal security property. The labels-as-functions approach provides relaxed noninterference by means of declassification policies expressed as functions. The labels-as-types approach expresses declassification policies using type abstraction and faceted types, a pair of types representing the secret and public facets of values. The original proposal of labels-as-types is formulated in an object-oriented setting where type abstraction is realized by subtyping. The object-oriented approach however suffers from limitations due to its receiver-centric paradigm. In this work, we consider an alternative approach to labels-as-types that allows us to express more advanced declassification policies, such as extrinsic policies, based on a different form of type abstraction: existential types. An existential type exposes abstract types and operations on these; we leverage this abstraction mechanism to express secrets that can be declassified using the provided operations. We formalize the approach in a core calculus with existential types, define the corresponding notion of relaxed noninterference that accounts for abstract types, and prove that well-typed programs satisfy this form of relaxed noninterference.

Mon 2 Dec

Displayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change

10:30 - 12:00
TypesResearch Papers at Bali Room
Chair(s): Tachio Terauchi Waseda University
10:30
30m
Talk
Manifest Contracts with Intersection Types
Research Papers
Yuki Nishida Kyoto University, Atsushi Igarashi Kyoto University, Japan
Pre-print
11:00
30m
Talk
A Dependently Typed Multi-Stage Calculus
Research Papers
Akira Kawata Kyoto University, Atsushi Igarashi Kyoto University, Japan
Pre-print
11:30
30m
Talk
Existential Types for Relaxed Noninterference
Research Papers
Raimil Cruz University of Chile, Éric Tanter University of Chile & Inria Paris