A Type System to Ensure Non-Interference in ReScript

TL;DR

This paper introduces a type system for a subset of ReScript that guarantees non-interference, ensuring confidential data does not influence public data, with a proof of soundness and an implementation overview.

Contribution

It presents the first type system for ReScript that enforces non-interference, including a soundness proof and a prototype type checker.

Findings

Type system guarantees non-interference for type-able expressions

Soundness proof confirms security property enforcement

Prototype type checker demonstrates practical implementation

Abstract

Protecting confidential data from leaking is a critical challenge in computer systems, particularly given the growing number of observers on the internet. Therefore, limiting information flow using robust security policies becomes increasingly vital. We focus on the non-interference policy, where the goal is to ensure that confidential data can not impact public data. This paper presents a type system, for a subset of the ReScript syntax, designed to enforce non-interference. We conclude with a proof of soundness for the type system, demonstrating that if an expression is type-able, it is inherently non-interferent. In addition, we provide a brief overview of a type checker that implements the previously mentioned type system.