Hybrid Information Flow Control for Low-Level Code

Abstract

Failure to ensure data confidentiality can have a significant financial and reputational impact on companies. To aggravate the issue, frequently used methods like testing are insufficient when proving data confidentiality in software systems. Existing information flow based approaches require heavy implementation and specification efforts or lack the expressiveness programmers desire. To tackle the issues, we propose a novel hybrid system for information flow control in low-level languages. By combining an information flow monitor with a type system that instruments programs with runtime security checks, we support value-dependent security types in a low-level setting. We formalise our type system and monitor using a TAL-like calculus and prove that they guarantee termination-insensitive non-interference. We present the first hybrid type system for information flow control with support for value-dependent types. We also introduce the first value-dependent hybrid mechanism for a low-level intermediate representation.