[Apologies to those who will get this via multiple mailing lists]

Dear All,

In 1992, when the world was young and what was then the Formal Methods Unit of the UK computer firm ICL had just completed the first round of development of the ProofPower toolset, we were funded to investigate formal specification and verification of the semantics of a multi-level secure database query language. This so-called FEF project turned into an interesting and successful industrial research programme and was subsequently extended to formalise a model of a prototype implementation and to look into the theory of a more complex language. The project ended in spring 1994. Although everybody involved always intended to make the results of this work public, organisational upheavals and other commitments conspired to delay dissemination of the results.

I am happy to announce that the results of the FEF project are now available on line at:


If you have OpenProofPower installed, you can download the sources of the project files and then build, inspect and experiment with the database of theories that comprise the formalisation.

While this work was undertaken many years ago, it is a large-scale example of a very direct and mathematically natural approach to non-interference security properties that I believe still has many features of interest.


Rob Arthan.

Proofpower mailing list

Reply via email to