Programs in the presence of nondeterminism or underspecification may mask the presence of insecure information flow between variables. This may re¬sult in the refinement paradox when such programs are refined to a de¬terministic implementation. Hence nondeterministic programs that satisfy possibilistic security properties like Generalised Noninterference (GNI) may, on refinement, fail corresponding deterministic security properties such as Noninterference (NI). We propose in this thesis an automatable information flow analysis frame-work to capture information flow between variables and flag flows that breach information flow policies defined as a multi-level secure lattice-based system. We separate the problem of satisfaction of the refinement relation from the problem of preservation of security properties of interest at every refinement step, and focus on the latter problem. We formalise our core analysis on standalone B Machines, develop the proof obligations of the framework, and introduce security conditions that must be satisfied to guarantee secure information flow between the vari¬ables within a single B machine (Chapter 3). We show that our analysis is more robust than standard flow-insensitive security type systems like the one developed by Volpano, Smith, and Irvine [76], since our analysis is flow-sensitive, i.e., responsive to information flow. For example, our frame-work correctly analyses a program whose overall flow is secure as secure, even when some of its subprograms may be insecure, whereas [76] will er¬roneously classify such programs as insecure, a problem commonly termed false negative. We also show the correctness of our framework in Chapter 3. A natural sequel to our core information flow analysis of standalone B Machines is an extension of the framework to analyse structured B Machines, i.e., information flow arising from the use of B structuring mechanisms such as SEES, INCLUDES, etc (Chapter 4). The third major part of the thesis (Chapter 5) involves the analysis of information flow between the variables in a hypothetical case study using the C++ implementation of the information flow analyser formalised in the preceding chapters. We also discuss our intuitions on future extensions.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:628183 |
| Date | January 2012 |
| Creators | Onunkun, T. J. |
| Publisher | King's College London (University of London) |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | https://kclpure.kcl.ac.uk/portal/en/theses/confidentiality-properties-and-the-b-method(bf7c1354-a81f-486d-a321-d66f66a6af6b).html |
Page generated in 0.002 seconds