High-Integrity Software Software Science and Engineering Series Editor: Richard A. DeMilio Purdue University, West Lafayette, Indiana High-Integrity Software c. T. Sennett A Continuation Order Plan is available for this series. A continuation order \\"ill bring deli"ery of each ne\\" ,olume immediately upon publication. Volumes are billed only upon actual shipment. For further informalion please contact the publisher. High-Integrity Software Edited by C T Sennett Royal Signals and Radar Establishment Malvern, UK Plenum Press . New York and London ISBN-13: 978-1-4684-5777-3 e-ISBN-13: 978-1-4684-5775-9 001: 10.1007/978-1-4684-5775-9 Library of Congress Catalog Card Number 89-043671 PLENUM PRESS A Division of Plenum Publishing Corporation 233 Spring Street, New York, NY 10013 © Chapters 1,2,3,6,9, 12: Crown Copyright 1989 © Chapters 5, 7, 8, 10, 11: Pitman Publishing 1989 Softcover reprint of the hardcover 1s t edition 1989 First published in Great Britain 1989 by Pitman Publishing A Division of Longman Group UK Limited All rights reserved. No part of this publication may be reproduced, stored in a retrieval system, or transmitted, in any form or by any means, electronic, mechanical, photocopying, recording and/or otherwise without the prior written permission of the Publishers Contents Introduction 1 C. T. Sennett, Royal Signals and Radar Establishment 2 Formal specification and implementation 6 C. T. Sennett, Royal Signals and Radar Establishment 2.1 Introduction to formal methods 6 2.2 Formal specification using Z 9 2.3 Formal implementation from Z 17 2.4 Conclusion 37 3 Designing for high integrity: The software fault tolerance approach 39 M. R. Moulding, Royal Military College of Science 3.1 Introduction 39 3.2 Overview of software fault tolerance 40 3.3 Towards an implementation framework for software fault tolerance 45 3.4 Robust software using Ada's exception handling facilities 48 3.5 N-version programming 52 3.6 Recovery blocks 55 3.7 Comparison of N-version programming and recovery blocks 61 3.8 Practical application of N-version programming and recovery blocks 63 3.9 Summary 65 4 Practical experience with a formal verification system 69 Paul Smith, Secure Information Systems Ltd., and Nick Bleech, SD-Scicon pic 4.1 I Ill! Odudiull 6Y v 4.2 Background 69 4.3 The Gypsy language 72 4.4 The Gypsy Verification Environment 73 4.5 A simple example 81 4.6 Specification data types 91 4.7 Future directions 95 4.8 Conclusions 100 5 Reliable programming in standard languages 102 Bernard Carre, Program Validation Ltd. 5.1 Introduction 102 5.2 Language requirements for high-integrity programming 103 5.3 The use of standard languages 108 5.4 Programming in Pascal and Ada 110 1'19 5.5 Practical experiences 6 NewSpeak: a reliable programming language 122 I. F. Currie, Royal Signals and Radar Establishment 6.1 Introduction 122 6.2 Types and values 127 6.3 Declarations and variables 132 6.4 Guarded declarations 134 6.5 Cases and conditionals 136 6.6 Loops 138 6.7 Procedures 140 6.8 Assertions 145 6.9 Timing 147 6.10 Conclusion 149 6.11 Appendix 1: summary of syntax 150 6.12 Appendix 2: type lattice and widening 156 7 Program analysis and systematic testing 159 M. A. Hennell, University of Liverpool, and D. Hedley and I. J. Riddell, Liverpool Data Research Associates Ltd. 7.1 Introduction 159 7.2 The basic requirement 160 7.3 The Liverpool experience 161 7.4 The Liverpool experiments 162 7.5 The LDRA Testbeds 163 7.6 Interpretation 169 7.7 Applicability and benefits 171 7.8 Safety-critical systems 173 VI 8 Program analysis and verification 176 Bernard Carre, Program Validation Ltd. 8.1 Introduction 176 8.2 Program modelling 178 8.3 Flow analysis 184 8.4 Formal verification 190 8.5 Conclusions 195 9 The algebraic specification of a target machine: Ten1S 198 J. M. Foster, Royal Signals and Radar Establishment 9.1 Introduction 198 9.2 Types and operation 206 9.3 Features of the Ten15 machine 214 9.4 The formal method 218 9.5 Formal definition of Ten15 220 9.6 Conclusions 224 10 Assurance in high-integrity software 226 John McDermid, University oj York 10.1 Introduction 226 10.2 Requirements and technical basis for assurance measures 229 10.3 Development 237 10.4 Requirements 242 10.5 Architecture 245 10.6 Evaluation 250 10.7 Configuration control 254 10.8 Complexity 256 10.9 Human computer interaction 257 10.10 Staff issues 260 10.11 Tools 261 10.12 Towards assurance measures 265 10.13 Conclusions 270 11 Modelling real-world issues for dependable software 274 John Dobson, University oj Newcastle-upon-Tyne 11.1 Introduction 274 11.2 The importance of policies 276 11.3 Multiple levels of representation 279 11.4 Models for a communication system 284 11.5 Dependability breaches 289 11.6 Outline of the A TM system 289 11.7 Axegrinder fIlles 292 11.8 Views of the system 295 11.9 Composite view of the system 298 11.10 Behavioural model of tht> ~y~tem 301 VII 1l.l1 Vulnerability analysis 304 11.12 Analysis of communication 304 1l.l3 Analysis of system conformation 306 11.14 Message analysis 308 1l.l5 Behavioural analysis 309 11.16 What enforces the rules? 314 11.17 Final summary: The analytical method in outline 315 12 Contractual specification of reliable software 317 C. T. Sennett, Royal Signals and Radar Establishment 12.1 The procurement process for high-integrity software 317 12.2 Procurement issues at the feasibility study stage 320 12.3 High-integrity considerations during project defmition 326 12.4 The development environment for trusted software 337 12.5 The formal specification of access control policies 342 Index 355 VI II Introduction 1 C. T. Sennett, Royal Signals and Radar Establishment The requirement for highly reliable software increases with every year. The benefits from the use of computers are so great that applications multiply to the extent that large sectors of modern society are totally dependent on their use. This dependence brings with it a vulnerability to serious damage if the software should fail: we are now entering an era in which software failures could have life-threatening consequences. This vulnerability compels the use of software techniques which will largely eliminate errors and it is the purpose of this book to describe some of these techniques and to set them into the context of the procurement process. The awareness of the need for high-integrity software has arisen in three different communities, the avionics industry, the defence industry and the large-scale procurers of software who are growing less and less tolerant of current standards of software reliability. The avionics industry has been the leader in the field of safety-critical applications, partly because of the need for airworthiness certification but also because of the generally high aware ness of the need to consider safety requirements in the industry. The use of "fly-by-wire" systems in which computers are interposed between the pilot and the control surface actuators has brought this problem to a head, but there are other applications, such as the use of computers to produce synthetic displays, where software failures could have intolerable conse quences. Other safety-critical applications occur in software used for the fuzing and arming of munitions, where safety-critical functions are now under software control. Nor are the safety-critical applications all confined to the military field. One can cite the cases of process control, including control of nuclear reactors, and railway signalling where systems are being designed which are vulnerable to software failure. Even in such apparently low-technology industries as water supply, computer-controlled systems are being considered whose failure could lead to large-scale water pollution. The defence community has of course a keen awareness of the need for security and the need for security accreditation has focussed on the criteria which software must satisfy ill urJer LO be tru~ted 1O process classified data. In the past, the degree of trust required has not been great as such cases have been confined to isolated systems. Now, however, there is an increasing necessity to link systems, and the operational needs are such as to require the placing of trust in the software. Typically, one can envisage the secure software as being used for an operational command and control system, for which the security needs are fairly obvious. However, the question of security also arises in the non-operational ADP systems which are used for the normal administrative purposes, because of the inferences it is possible to make from the administrative data. The defence community is also very much aware of the possibilities for denial of service. A software failure may be such that it renders a system unavailable at a time of crisis, when it is most needed. It is possible that this failure could be engineered deliberately, a possibility which is not confined to defence systems alone. The jargon of computer viruses and logic bombs indicates that there are many individuals who, from a variety of motives, are interested in subverting computer systems. This is a typical hazard for computer networks, but it is also experienced by computer-controlled telephone exchanges which are vulnerable to abuse. Telephone exchanges are also vulnerable to sudden unexpected increases in demand. The integrity requirement here is that the emergency services are not denied as a result of a sudden upsurge of demand caused by, say, a phone-in programme. The other thread to the demand for high-integrity software has been cost. Software errors are costly to correct but their occurrence can give rise to substantial losses. In the financial sector, computers control immense resources and their failure can give rise to substantial losses simply from loss of service, quite apart from actual errors. A recent example is the case of a US bank which suffered an error in its computer system which gave rise to directly attributable losses of $9000000, even though the fault was cured within one day. Similarly, satellite launch vehicles are controlled by com puters and their failure can put at risk an extremely valuable payload as well as the vehicle itself. The three threads of safety, security and cost have given rise to different emphases and techniques for addressing the integrity issue, all of which have something to offer. From the safety field emerged the ideas of fault tolerance and N-version programming. Fault tolerance has proved to be a very fruitful idea with techniques ranging from defensive programming to the use of system designs in which the trusted components constrain the behaviour of the untrusted ones. This has led to an emphasis on the quality of the design and the use of the best available techniques from the rest of the software industry. The security field has been marked by an emphasis on the use of formal methods, in particular on the use of formal proof of software. This stems partly from the early interaction with the academic community, but also from the fact that security requirements are easier to specify than safety requirements. Security requirements are simply concerned with information 2