Racets: Faceted Execution in Racket

TL;DR

Racets introduces a library-based implementation of faceted execution in Racket, enabling policy-agnostic programming for secure data handling without modifying language runtime, demonstrated through a web-based Battleship game.

Contribution

It presents Racets, a lightweight, macro-based implementation of faceted execution in Racket, facilitating policy-agnostic programming without runtime modifications.

Findings

Enables privacy policy enforcement independently of application code

Demonstrates practical use with a web-based Battleship game

Highlights interactions with non-faceted code

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.