ChenJan2024

Time and Location

  • Date: Wednesday, January 24
  • Time: 11:15 AM-12:15 PM
  • Location: Info (aka Myles Brand Hall) East 150 (BLI-E150)

Abstract

Languages with gradual information-flow control combine static and dynamic techniques to prevent security leaks. Gradual languages should satisfy the gradual guarantee: programs that only differ in the precision of their type annotations should behave the same modulo cast errors. Unfortunately, Toro et al. [2018] identify a tension between the gradual guarantee and information security; they were unable to satisfy both properties in the language \(\mathrm{GSL}_\mathsf{Ref}\) and had to settle for only satisfying information-flow security. Azevedo de Amorim et al. [2020] show that by sacrificing type-guided classification, one obtains a language that satisfies both noninterference and the gradual guarantee. Bichhawat et al. [2021] show that both properties can be satisfied by sacrificing the no-sensitive-upgrade mechanism, replacing it with a static analysis.

In this talk I present our new gradual security-typed language, \(\lambda_{\mathtt{IFC}}^\star\), that satisfies both noninterference and the gradual guarantee without making any sacrifices. \(\lambda_{\mathtt{IFC}}^\star\) (1) enforces information flow security, (2) satisfies the gradual guarantee, (3) enjoys type-guided classification, and (4) utilizes NSU checking to enforce implicit flows through the heap with no static analysis required. The key to the design of \(\lambda_{\mathtt{IFC}}^\star\) is to walk back the unusual decision in \(\mathrm{GSL}_\mathsf{Ref}\) to include the unknown label among the runtime security labels. We mechanize the definition of \(\lambda_{\mathtt{IFC}}^\star\) in Agda and prove the gradual guarantee. On the technical side, the semantics of \(\lambda_{\mathtt{IFC}}^\star\) is the first gradual information-flow control language to be specified using coercion calculi (a la Henglein), thereby expanding the coercion-based theory of gradual typing.

(Tianyu is a PhD student advised by Prof. Jeremy Siek.)