Dear All,
In early 1992, when the world was young and 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 by the UK Defence Research Agency to
investigate the formal specification and verification of the critical security
properties of the semantics of a multi-level secure database query language.
This so-called FEF project turned into an interesting industrial research
programme over 2 years that grew to verify a model of a prototype
implementation and aspects of the theory of a more complex language. Although
everybody involved always intended to make the results of this work public,
organisational upheavals and other commitments have conspired to delay
dissemination of the results a little.
I am happy to announce that the results of the FEF project are now available
for all to see at:
http://www.lemma-one.com/ProofPower/fef/fef.html
The web page gives an overview and a guide to the project documentation which
you can read in PDF format. The material is also a working case study for
ProofPower. The project source files are available for download under the GNU
General Public Licence. If you have OpenProofPower installed you can 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.
------------------------------------------------------------------------------
Return on Information:
Google Enterprise Search pays you back
Get the facts.
http://p.sf.net/sfu/google-dev2dev
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
