Correctness Properties of the Viper Block Model: The Second Level

Abstract

Viper [7,8,9,11,23] is a microprocessor designed by W. J. Cullyer, C. Pygott and J. Kershaw at the Royal Signals and Radar Establishment in Malvern, England (RSRE), and is now commercially available. Viper was intended for use in safety-critical applications such as civil aviation and nuclear power plant control. It is currently being evaluated (as part of the “VENOM” project [10]) for use as an input-output controller in the deployment of weapons from tactical aircraft. To satisfy requirements of safety-criticality, Viper has a particularly simple design about which it is relatively easy to reason using current techniques and models. The designers at RSRE, who deserve much credit for the promotion of formal methods, intended from the start that Viper be formally verified. The verification project has been carried out at the University of Cambridge. The University was and is not involved with any of the applications of Viper, civil or otherwise, and the whole verification project is and has been fully in the public domain. This report describes the partially completed correctness proof, in the HOL system, of the Viper ‘block model’ with respect to Viper’s top level functional specification. The (fully completed) correctness proof of the Viper ‘major state’ model has already been reported in [5]. This paper describes the analysis of the block model in some detail (in Sections 6 to 9), so is necessarily rather long. Section 2 is a discussion of the scope and limits of the word ‘verification’, and cautions against careless use of the term. The paper includes a very brief introduction to HOL (Section 4), but does not attempt a description or rationalization of Viper’s design.The possible uses of the paper are as follows:

• It includes enough detail to support an attempt to repeat the proof in HOL, or possibly in other theorem-proving systems;

• It serves as a guide for future analyses of Viper;

• It complements the existing Viper documentation;

• It covers some general issues in hardware verification;

• It illustrates some problems in managing large HOL proofs.