A ProofPower Application: the Front End Filter Project

---

Introduction

SWORD was an experimental prototype of a multi-level secure database that was the subject of research undertaken by the UK's Defence Research Agency in the early 1990s. The query language for the SWORD database was Secure SQL (SSQL) an extension of standard SQL whose semantics support a notion of security classification. Data in the database would be a assigned a classification drawn from some lattice e.g., UNCLASSIFIED < COMPANY-IN-CONFIDENCE < COMPANY-RESTRICTED < SECRET. Database users would be assigned a security clearance constraining the classification of the data they are allowed to access.

In early 1992, the Formal Methods Unit at ICL's Defence Technology Centre had completed the first production version of their system ProofPower for formal specification and verification in higher-order logic (HOL) with a surface syntax designed to be familiar to users of the Z specification language. ProofPower was subsequently enhanced to support a semantic embedding of the full Z language in addition to HOL and is now an open source system provided by Lemma 1 Ltd. .

From April 1992 to April 1994, the ICL Formal Methods Unit applied ProofPower to the formal specification and verification of the high-level security properties of SSQL and the SWORD prototype implementation. The work was done in three stages:

• In stage 1 the security policy and the semantics of SSQL were specified and it was proved that the semantics satisfied the security policy;
• In stage 2, a model of the SWORD implementation of SSQL was specified and it was proved that the resulting implementation satisfies the security requirements. SWORD implemented SSQL as a front-end to a conventional SQL database that contained additional columns giving the security classification of the data. The front-end translated an SSQL query into an SQL query whose results were filtered to remove sensitive data (hence the name of the project: Front-End Filter or FEF);
• Stage 3 was rather more theoretical: it addressed modelling isssues for an extension of SSQL in which the queries themselves were multi-level secure objects. A formal security policy for such objects was formalised and an abstract labelling property formalised and proved.

General Documents

• Project Overview Document

  A managerial overview of the project and its documentation [FEF/001]

• Index of Theories

  A listing of all the constants, types and aliases, with their defining theories, that are available for use in the fef project [FEF/008]

• ProofPower Theory Listings

  Consolidated istings of all the ProofPower theories used in the DRA front end filter project [FEF/017]

The following links to the descriptions of the documents may be helpful in connection with the index of theories and the consolidated listings. The gaps are documents that were superseded.

Stage 1

• Errors in the SSQL Specification

  A record of errors found in the SSQL specification, and changes made from Annex 2 of the ITT [FEF/002]

• Formal Security Policy

  The formalisation of the security conjecture is in this document [FEF/003]

• Specification of SSQL Semantics I

  The formal specifications of the main functionality of the SSQL semantics [FEF/004]

• Specifications of hide and updateState

  The formal specifications of the functions hide and updateState [FEF/005]

• Security Conjectures for the SSQL Abstract Machine

  The formal specification of the SSQL abstract machine and the conjecture to be proven in order to prove its security [FEF/006]

• Proof Strategy

  A proof strategy for proving the conjecture of DS/FMU/FEF/005 [FEF/007]

• Proof of Security (I)

  A formal proof of the unwinding result, part of the proof of security of the SSQL Abstract Machine[FEF/009]

• Proof of Security (IIa)

  A formal proof of the security property on hide, part of the proof of security of the SSQL Abstract Machine[FEF/010]

• Proof of Security (IIb)

  A formal proof conjuncts three and four of the security property on the relationship between hide and updateState, part of the proof of security of the SSQL Abstract Machine[FEF/011]

• Proof of Security (IIc)

  A formal proof of conjunct one of the security property on the relationship between hide and updateState, part of the proof of security of the SSQL Abstract Machine[FEF/012]

• Proof of Security (IId)

  A formal proof of conjunct two of the security property on the relationship between hide and updateState[FEF/013]

• Specification of SSQL Semantics II

  The formal specification of the function processQuery. This completes the specification of the main functionality of the SSQL semantics [FEF/014]

• Proof of Security (IIe)

  A formal proof that updateState maintains the invariant on the state. This result, together with the proofs from DS/FMU/FEF/011, DS/FMU/FEF/012 and DS/FMU/FEF/013, is used to prove the security property on the relationship between hide and updateState. This result in turn is used together with the proofs from DS/FMU/FEF/009 and DS/FMU/FEF/010 to complete the Phase 1 security proof, namely that behaviours SSQLam belongs to the set secure of secure systems. [FEF/015]

• Informal Justifications for Proof of Security

  Informal justifications of those axioms which have been included in the Phase 1 formal proof of security[FEF/016]

Stage 2

• Proposal for Phase 2

  The revised proposal for Phase 2 [FEF/018]

• Specification of Query Transformations in SML (I)

  Standard ML functions and SSQL and TSQL datatype specifications required for the SSQL transformation specifications [FEF/019]

• Specification of Query Transformations in SML (II)

  Specifications of the SSQL transformations in Standard ML [FEF/020]

• Specification of TSQL

  Specifications of the TSQL abstract machine [FEF/021]

• SWORD Front End Architectural Model

  Top level specifications of a model of the SWORD Front End [FEF/022]

• A Standard ML Specification of the Output Filter

  A specification of the output filter in Standard ML for the SWORD Front End [FEF/023]

• A HOL Specification of the SWORD Output Filter

  A ProofPower-HOL specification of the SWORD output filter [FEF/024]

• Representation of an SSQL State as a TSQL State

  The formal specification of a mapping from an SSQL abstract machine state to the TSQL state which represents it [FEF/025]

• Critical Requirements on the SWORD Query Transformations

  A ProofPower-HOL specification of the Critical Requirements on the SWORD Query Transformations [FEF/026]

• Specification of Query Transformations in HOL (I)

  First part of the HOL specification of the SSQL transformation specifications [FEF/028]

• Specification of Query Transformations in HOL (II)

  Second part of the HOL specification of the SSQL transformation specifications [FEF/029]

• Presentation on FEF Phase I

  Slitex document containing overheads for FEF presentation [FEF/030]

• Execution Model Security Proofs

  Security proofs relating to the Execution Model of \cite{DS/FMU/FEF/026} [FEF/031]

• Table Computations for SWORD

  Specifications of the computations which are allowed to be performed by the Execution Model of \cite{DS/FMU/FEF/031} [FEF/032]

• Value Computation Security Proofs

  Security proofs relating to the value computations of \cite{DS/FMU/FEF/032} [FEF/033]

• Phase II Proof Strategy

  The strategy for the Phase II proofs. [FEF/034]

• Table Computation Security Proofs

  Security proofs relating to the table computations of \cite{DS/FMU/FEF/032} [FEF/035]

• Phase II Proof Finale

  Incorporation of Table Computation Security Proofs and Execution Model Security Proofs into overall partial proof for Phase II [FEF/036]

Stage 3

• Proposal and Quotation for Phase 3

  A proposal for an extension to the scope of phase 3 of the project. [FEF/039]

• Multi-level Formal Security Policy

  A formalisation of a multi-level version of the security policy. [FEF/040]

• Briefing for CLEF

  A briefing suitable for a CLEF on the FEF work. [FEF/041]

• Multi-Level Architectural Model

  A formulation of a somewhat simplified model of the multi-level SWORD database. [FEF/042]

• The Labelling Property for SWORD

  A discussion and formalisation of an abstract `labelling property' for SWORD. [FEF/044]

• Proofs About Labelling

  Formal proofs establishing various results about the multi-level policy and the labelling property for SWORD. [FEF/044]

• Phase 3 Theory Listings

  This document contains listings of the theories developed under Pphase 3 of the FEF contract, together with an index. [FEF/045]

• Technical Overview and Final Report

  This document gives an overview of the formal work carried out under the phase 3 of the FEF project and serves as the final report on that work. It also discusses the relationship between the phase 2 and phase 3 work and suggests some possible directions for future research. [FEF/046]

• FEF Project Final Report

  A final report on all aspects of the FEF contract. [FEF/047]

• Report on Phase 3 Proofs

  A report on the proof work carried out in phase 3. [FEF/048]

Download

The source of the FEF documents including all the specification and proof scripts is available here and should work with recent versions of ProofPower (last tested at time of writing on version 3.1w6).

Acknowledgments

Thanks are due to:

• The organisations QinetiQ and DSTL formerly known as the Defence Research Agency for funding the original work;
• QinetiQ and D-RisQ for continued support of ProofPower;
• Paul Caseley of DSTL and Simon Wiseman of QinetiQ for permission to publish the documents;
• Gill Prout for doing nearly all the work in the first two stages of the project.
• Roger Jones for assistance both during the project and during the preparation of this web page.

Copyright © Lemma 1 Ltd. Created by  Rob Arthan (rda@lemma-one .com) Last updated: 5th June 2016