Racets: Faceted Execution in Racket

EasyChair Preprint 502

Abstract

Faceted Execution is a linguistic paradigm for dynamic information-flow control. Under faceted execution, secure program data is represented by faceted values: decision trees that encode how the data should appear to its owner (represented by a label) versus everyone else. When labels are allowed to be first-class (i.e., predicates that decide at runtime which data to reveal), faceted execution enables policy-agnostic programming: a programming style that allows privacy policies for data to be enforced independently of code that computes on that data.

To date, implementations of faceted execution are relatively heavyweight: requiring either changing the language runtime or the application code (e.g., by using monads). Following Racket's languages-as-libraries approach, we present Racets: an implementation of faceted execution as a library of macros. Given Racket's highly-expressive macro system, our implementation follows relatively directly from the semantics of faceted execution. To demonstrate how Racets can be used for policy-agnostic programming, we use it to build a web-based game of Battleship. Our implementation sheds light on several interesting issues in interacting with code written without faceted execution. Our Racets implementation is open source, under development, and available online.

Keyphrases: Security, faceted execution, information flow, languages as libraries, macros

@booklet{EasyChair:502,
  author    = {Kristopher Micinski and Zhanpeng Wang and Thomas Gilray},
  title     = {Racets: Faceted Execution in Racket},
  doi       = {10.29007/lqkv},
  howpublished = {EasyChair Preprint 502},
  year      = {EasyChair, 2018}}