[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:
http://www.lemma-one.com/ProofPower/fef/fef.html
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.
Regards,
Rob Arthan.
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
