Adaptation of information flow concepts in a capability-based functional language

The average cost of a data breach in 2019 was estimated at $3.92 million USD. Some of these breaches were caused through the exploitation of software vulnerabilities. Analysis indicates information leaks are the third most common of these vulnerabilities. Information leaks are caused when data flows violate a security policy. Leaks can be identified by information flow analysis, which tracks how data flows through a program to protect sensitive data. Static, dynamic and hybrid approaches exist, tagging data or locations with security levels. Typically these approaches are external to the core language, provided through libraries and tools. In this thesis we explore core language mechanisms as a means to enforce a security policy that prevents the declassification of data, language-wide. Leveraging the type system, we encode security levels and simultaneously enforce the policy. We introduce an existing security-focused, functional language, Cooma, which uses capabilities to represent permissions and side-effects. By default, Cooma programs have no capabilities so users must explicitly provide them at run-time. Embedding information flow analysis in Cooma’s type system, we present Cooma_IF. We prove well-typed Cooma_IF programs don’t violate our security policy and demonstrate the security guarantees Cooma_IF provides.