This HTML5 document contains 21 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

Prefix	IRI
dcterms	http://purl.org/dc/terms/
n2	https://kar.kent.ac.uk/id/eprint/
n13	https://kar.kent.ac.uk/90641/
wdrs	http://www.w3.org/2007/05/powder-s#
n17	http://purl.org/ontology/bibo/status/
rdfs	http://www.w3.org/2000/01/rdf-schema#
n5	https://kar.kent.ac.uk/id/subject/
n19	https://demo.openlinksw.com/about/id/entity/https/raw.githubusercontent.com/annajordanous/CO644Files/main/
n10	doi:10.1109/
n16	http://eprints.org/ontology/
n14	https://kar.kent.ac.uk/id/eprint/90641#
n8	https://kar.kent.ac.uk/id/event/
bibo	http://purl.org/ontology/bibo/
n20	https://kar.kent.ac.uk/id/publication/
n11	https://kar.kent.ac.uk/id/org/
rdf	http://www.w3.org/1999/02/22-rdf-syntax-ns#
owl	http://www.w3.org/2002/07/owl#
n18	https://kar.kent.ac.uk/id/
xsdh	http://www.w3.org/2001/XMLSchema#
n7	https://demo.openlinksw.com/about/id/entity/https/www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/
n15	https://kar.kent.ac.uk/id/person/

Statements

Subject Item

n2:90641

rdf:type

bibo:AcademicArticle n16:EPrint bibo:Article n16:ConferenceItemEPrint

rdfs:seeAlso

n13:

owl:sameAs

n10:csf.2018.00024

dcterms:title

Types for Information Flow Control: Labeling Granularity and Semantic Models

wdrs:describedby

n7:export_kar_RDFN3.n3 n19:export_kar_RDFN3.n3

dcterms:date

2018-07-09

dcterms:creator

n15:ext-v.rajani@kent.ac.uk n15:ext-1f909178dce42d92a486408138947fb3

bibo:status

n17:peerReviewed n17:published

dcterms:publisher

n11:ext-af0a9a5baed87c407844a3f5db44597c

bibo:abstract

Language-based information flow control (IFC) tracks dependencies within a program using sensitivity labels and prohibits public outputs from depending on secret inputs. In particular, literature has proposed several type systems for tracking these dependencies. On one extreme, there are fine-grained type systems (like Flow Caml) that label all values individually and track dependence at the level of individual values. On the other extreme are coarse-grained type systems (like HLIO) that track dependence coarsely, by associating a single label with an entire computation context and not labeling all values individually. In this paper, we show that, despite their glaring differences, both these styles are, in fact, equally expressive. To do this, we show a semantics- and type-preserving translation from a coarse-grained type system to a fine-grained one and vice-versa. The forward translation isn't surprising, but the backward translation is: It requires a construct to arbitrarily limit the scope of a context label in the coarse-grained type system (e.g., HLIO's "toLabeled" construct). As a separate contribution, we show how to extend work on logical relation models of IFC types to higher-order state. We build such logical relations for both the fine-grained type system and the coarse-grained type system. We use these relations to prove the two type systems and our translations between them sound.

dcterms:isPartOf

n18:repository n20:ext-a676b5e6df64c75cd316d22bf8868741

dcterms:subject

n5:QA76

bibo:authorList

n14:authors

bibo:presentedAt

n8:ext-d1a41dd213516cea2091478b2b865028