arpa-bboard@ucbvax.ARPA (07/31/85)
From: Boebert@MIT-MULTICS.ARPA The Honeywell Secure Computing Technology Center is seeking individuals or organizations who would be interested in refereeing the proofs of security of the Secure Ada Target (SAT) machine. These proofs were intended from the outset to be refereeable and are accordingly machine-checked but not machine-generated. They should therefore be intellectually accessible to parties familiar with the general topics of computer security and program verification. The proofs are currently expressed in the theory of the Gypsy Verification Environment and have been checked by the Gypsy tools. Care has been taken to minimize the use of distinctive Gypsy features and we are reasonably confident that the proofs could be checked using any contemporary program proof environment. We are interested in a traditional mathematical refereeing process, that is, a re-examination of our reasoning from first principles, and *not* a simple re-running of the automated proof checks. This should be a interesting project for individuals or teams seeking problems in program verification. We currently have no means of financially supporting such an effort, but we are very optimistic that we could obtain support once a qualified set of referees were identified. Please send expressions of interest to Boebert @ MIT-Multics.