Lattice-Based Information Flow Control-by-Construction for Security-by-Design
Many software applications contain confidential information, which has to be prevented from leaking through unauthorized access. To enforce confidentiality, there are language-based security mechanisms that rely on information flow control. Typically, these mechanisms work post-hoc by checking whether confidential data is accessed unauthorizedly after the complete program is written. The disadvantage is that incomplete programs cannot be interpreted properly and information flow properties cannot be built in constructively. In this work, we present a methodology to construct programs incrementally using refinement rules to follow a lattice-based information flow policy. In every refinement step, confidentiality and functional correctness of the program is guaranteed, such that insecure programs are prohibited by construction. Our contribution is fourfold. We formalize refinement rules for information flow control-by-construction, prove soundness of the refinement rules, show that our approach has the same expressiveness as standard language-based mechanisms for information flow, and implement the approach in a graphical editor called CorC. Our methodology is also usable for integrity properties, which are dual to confidentiality.