Formal analysis of confidentiality conditions related to data leakage

The size of the financial risk, the social repercussions and the legal ramifications resulting from data leakage are of great concern. Some experts believe that poor system designs are to blame. The goal of this thesis is to use applied formal methods to verify that data leakage related confidentiality properties of system designs are satisfied. This thesis presents a practically applicable approach for using Banks's confidentiality framework, instantiated using the Circus notation.

The thesis proposes a tool-chain for mechanizing the application of the framework and includes a custom tool and the Isabelle theorem prover that coordinate to verify a given system model. The practical applicability of the mechanization was evaluated by analysing a number of hand-crafted systems having literature related confidentiality requirements.

Without any reliable tool for using BCF or any Circus tool that can be extended for the same purpose, it was necessary to build a custom tool. Further, a lack of literature related descriptive case studies on confidentiality in systems compelled us to use hand-written system specifications with literature related confidentiality requirements.

The results of this study show that the tool-chain proposed in this thesis is practically applicable in terms of time required. Further, the efficiency of the proposed tool-chain has been shown by comparing the time taken for analysing a system both using the mechanised approach as well as the manual approach.