Technical reports

Of what use is a verified compiler specification?

Paul Curzon

November 1992, 23 pages

DOI: 10.48456/tr-274

Abstract

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 implementation.

Full text

PDF (1.8 MB)

BibTeX record

@TechReport{UCAM-CL-TR-274,
  author =	 {Curzon, Paul},
  title = 	 {{Of what use is a verified compiler specification?}},
  year = 	 1992,
  month = 	 nov,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-274.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-274},
  number = 	 {UCAM-CL-TR-274}
}