methods:
The OWR was specified in HOL with transcripts supplied in Z.
It was a hardware device, designed by ICL to meet the security requirement.
The design was formally proven against the security requirement using a specially modified version of Classic HOL.
This involved formal reasoning about information flow bandwidths.
|
|
modifying HOL:
HOL was modified, to make it more secure, and to permit loose constant specifications.
"new_axiom" and "mk_thm" were hidden from users.
Loose specifications were enabled by permitting the deletion of definitions, using a definition using the choice function, deriving a theorem of the form "x.P x P c" and then deleting the definition.
|
|
reals:
We had a look at implementing reals in HOL (this was 1988), using represention of real numbers as open downward-closed cuts in pre-rationals represented as triples of natural numbers ((a,b,c) represents the rational ((a-b)/(c+1)).
This was pretty heavy going (no linear arithmetic).
Long before we had the reals we had a way of talking about bandwidth without them, so we had to give up that little project and get on with the real work.
|
|