White Rose University Consortium logo
University of Leeds logo University of Sheffield logo York University logo

Formal analysis of confidentiality conditions related to data leakage

SHIYAM, IBRAHIM (2016) Formal analysis of confidentiality conditions related to data leakage. PhD thesis, University of York.

This is the latest version of this item.

Thesis.pdf - Examined Thesis (PDF)
Available under License Creative Commons Attribution-Noncommercial-No Derivative Works 2.0 UK: England & Wales.

Download (3617Kb) | Preview


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.

Item Type: Thesis (PhD)
Academic Units: The University of York > Computer Science (York)
Identification Number/EthosID: uk.bl.ethos.745707
Depositing User: MR IBRAHIM SHIYAM
Date Deposited: 11 Jun 2018 09:36
Last Modified: 24 Jul 2018 15:24
URI: http://etheses.whiterose.ac.uk/id/eprint/20377

Available Versions of this Item

  • Formal analysis of confidentiality conditions related to data leakage. (deposited 11 Jun 2018 09:36) [Currently Displayed]

You do not need to contact us to get a copy of this thesis. Please use the 'Download' link(s) above to get a copy.
You can contact us about this thesis. If you need to make a general enquiry, please see the Contact us page.

Actions (repository staff only: login required)