Why ProofPower?

ICL completed in 1993 its contribution to a collaborative R&D project part funded by the DTI and entitled ``Foundations and Tools for Formal Verification''. The main result of the ICL contribution to this project was the tool now commercially marketed as ``ProofPower'', a proof tool supporting Higher Order Logic and Z. Why did ICL undertake this project, what were the technical and commercial objectives of the work and what was the rationale behind the decisions which made ProofPower what it is? An insider tells all.

In the summer of 1988 my then manager at ICL, Patrick O'Loughlin, came to me for my views on a suggestion from Peter Harrison of Imperial College that we participate in an R&D project. After giving some consideration to the proposal I recommended that if money was available for this kind of work then it would be better to put together a project targeted more directly at the perceived needs of the business in which we were then engaged.

At that time ICL was engaged in developing under contract to GCHQ a device permitting information to flow securely from untrusted sources into highly secure computer systems. The requirement was for a device developed to the highest attainable level of assurance, and ICL had contracted to implement the security critical parts of the device entirely in hardware and to formally verify the system against the security policy. A machine checked formal proof was under development of the proposition that if components satisfying identified formal requirements were connected together in the manner prescribed by a detailed wiring diagram (produced by a DA tool) then the resulting device would conform to the formal statement of the security requirements.

The specification and verification of the OWR were undertaken using Higher Order Logic, and a slightly modified version of the Cambridge HOL proof tool now known as HOL88.

Though GCHQ preferred the use of Z as a specification language, with the tools then available proofs about specifications written in Z could not be fully machine checked since machine checking of any kind would involve transcription into a notation supported by a proof tool. This would inevitably weaken the assurance obtained. For this reason we used HOL on the OWR project as the language in which the definitive specifications were to be written, rather than as a language into which specifications were transcribed for proof checking. Nonetheless the preferences of the customer were well understood and later were to be received with even greater emphasis. Proofs in HOL were acceptable pro-tem, but in due course specification and proof in Z were required. There was therefore in out minds the need for a good Z proof tool, and no prospect in sight that any other group was likely to produce one.

The use made of Z for security modelling at ICL has been distinctive methodologically from the mainstream methods then being taught at Oxford. Two principal factors explain the differences. Firstly, from the documentation then available to us in 1986 it was difficult to establish clearly the intended semantics of schemas when used to describe operations (their principal use in most Z specifications). The second factor arose from the nature of the application. The problem facing us was that of using formal specifications in such a way as to enable formal proofs to be constructed of claims about the security off specified systems.

The first step in this process was to capture formally what it means to claim informally that a system is `secure'. To some extent this is found to involve arbitrary choices, and is therefore usually regarded as a policy formalisation exercise, undertaken in close liason with those with responsibility for the relevant policy.

Though intended to do so in somewhat abstract ways, the purpose of the methods associated with Z was to describe specific systems. They provide no good means of defining what it is which distinguishes secure systems from insecure systems. Though systems could be specified and alleged to be secure, any attempt to prove such an allegation would need first to formalise the content of the claim. Furthermore, methodologically it is preferred to establish requirements, especially critical requirements such as security requirements, prior to undertaking other aspects of system specification design or implementation.

The important distinction drawn here is that between describing a system which just happens to have, or even is intended to have, some particular characteristic, and specifying what that characteristic (or property) is. The distinction between specifying a system and a property of systems.