A Type System to Ensure Non-Interference in ReScript
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.
Keywords
Cite
@article{arxiv.2410.18157,
title = {A Type System to Ensure Non-Interference in ReScript},
author = {Benjamin Bennetzen and Daniel Vang Kleist and Emilie Sonne Steinmann and Loke Walsted and Nikolaj Rossander Kristensen and Peter Buus Steffensen},
journal= {arXiv preprint arXiv:2410.18157},
year = {2024}
}
Comments
Benjamin Bennetzen: 0009-0007-1751-6862 Daniel Vang Kleist: 0009-0005-1785-2124 Emilie Sonne Steinmann: 0009-0000-4733-5842 Loke Walsted: 0009-0002-1758-4594 Nikolaj Rossander Kristensen: 0009-0005-2339-8247 Peter Buus Steffensen: 0009-0005-6410-5869