Information Flow Control-by-Construction for an Object-Oriented Language Using Type Modifiers

TL;DR

This paper presents IFbCOO, a construction-based approach for secure information flow in object-oriented programming, guiding users incrementally to secure implementations with formal guarantees and practical tool support.

Contribution

It introduces a novel refinement-based method for secure information flow control during program construction, formalizes it, and demonstrates its feasibility with a tool and case studies.

Findings

Formal soundness of the refinement rules.

Successful implementation in the CorC tool.

Feasibility demonstrated through case studies.

Abstract

In security-critical software applications, confidential information must be prevented from leaking to unauthorized sinks. Static analysis techniques are widespread to enforce a secure information flow by checking a program after construction. A drawback of these systems is that incomplete programs during construction cannot be checked properly. The user is not guided to a secure program by most systems. We introduce IFbCOO, an approach that guides users incrementally to a secure implementation by using refinement rules. In each refinement step, confidentiality or integrity (or both) is guaranteed alongside the functional correctness of the program, such that insecure programs are declined by construction. In this work, we formalize IFbCOO and prove soundness of the refinement rules. We implement IFbCOO in the tool CorC and conduct a feasibility study by successfully implementing case studies.