Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Mon, 23 Nov 1992 19:18:42 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA07275; Mon, 23 Nov 92 11:02:15 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from nene.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA07270; Mon, 23 Nov 92 11:02:04 -0800 Received: from coot.cl.cam.ac.uk (user pc (rfc931)) by nene.cl.cam.ac.uk with SMTP (PP-6.3) to cl; Mon, 23 Nov 1992 19:01:21 +0000 To: info-hol@edu.uidaho.cs.ted Subject: Paper Date: Mon, 23 Nov 92 19:01:15 +0000 From: Paul Curzon Message-Id: <"nene.cl.ca.960:23.11.92.19.01.22"@cl.cam.ac.uk> The following paper is now available by ftp from ftp.cl.cam.ac.uk in the directory hvg/papers. It is in the file WhyCompilerSpec.ps.Z. It will appear as University of Cambridge, Computer Laboratory Technical Report Number 274. Of What Use is a Verified Compiler Specification? Paul Curzon Program verification is normally performed on source code. However, it is the object code which is executed and so which ultimately must be correct. The compiler used to produce the object code must not introduce bugs. The majority of the compiler correctness literature is concerned with the verification of compiler specifications rather than executable implementations. We discuss different ways that verified specifications can be used to obtain implementations with varying degrees of security. In particular, we describe how a specification can be executed by proof. We discuss how this method can be used in conjunction with an insecure production compiler so as to retain security without slowing the development cycle of application programs. A verified implementation of a compiler in a high-level language is not sufficient to obtain correct object code. The compiler must itself be compiled into a low-level language before it can be executed. At first sight it appears we need an already verified compiler to obtain a secure low-level implementation of a compiler. We describe how a low-level implementation of a compiler can be securely obtained from a verified compiler specification. Paul.