BKHISTSA.RVW   20030913

"High Integrity Software", John Barnes, 2003, 0-321-13616-0
%A   John Barnes
%C   P.O. Box 520, 26 Prince Andrew Place, Don Mills, Ontario M3C 2T8
%D   2003
%G   0-321-13616-0
%I   Addison-Wesley Publishing Co.
%O   416-447-5101 fax: 416-443-0948 800-822-6339 bkexpress@aw.com
%O  http://www.amazon.com/exec/obidos/ASIN/0321136160/robsladesinterne
  http://www.amazon.co.uk/exec/obidos/ASIN/0321136160/robsladesinte-21
%O   http://www.amazon.ca/exec/obidos/ASIN/0321136160/robsladesin03-20
%P   430 p. + CD-ROM
%T   "High Integrity Software: The SPARK Approach to Safety and
      Security"

Once upon a time, a group set out to build a language which would
allow you to write programs that could be formally verified.  Formal
analysis and proof can be used to determine that a program will work
the way you want it to, and not do something very weird (usually at an
inopportune time).  First came the attempt to build the Southampton
Program Analysis Development Environment (or SPADE) using a subset of
the Pascal programming language.  When it was determined that Pascal
wasn't really suitable, research was directed to Ada, and the SPADE
Ada Kernel, or (with a little poetic licence) SPARK, was the result.

SPARK can be considered both a subset and extension to Ada, but is
best seen as a separate language in its own right.  SPARK forbids
language structures such as the infamous GOTO statement of Fortran and
BASIC (which cannot be formally verified).  Support for some object-
oriented features has been included in SPARK, but not for aspects like
polymorphism which would make formal proof problematic.  A great deal
of the security of SPARK lies in the idea of contracts and the use of
data specifications (usually referred to as interfaces) that prevent
problems such as the unfortunately all-too-ubiquitous buffer overflow.

Part one is an overview of the background and features of SPARK. 
Chapter one reviews some of the problems of unproven software, and the
major components of SPARK.  Support for the formal proof functions,
such as abstraction (the elimination of details not essential to the
fundamental operation of the concept or function) are dicussed in
chapter two.  The various analysis tools are listed in chapter three.

Part two outlines the SPARK language itself.  Chapter four describes
the structure of SPARK and the lexical items it contains.  Language
elements are covered in chapters five, six, and seven, successively
dealing with the type model and operators, control and data flow, and
packages and visibility (local, global, etc.) which also reviews the
object-oriented aspects of SPARK.  Interfacing of the various parts of
SPARK, and also of SPARK and other languages, is in chapter eight.

Part three looks at the various analytical utilities in SPARK and the
proof process.  Chapter nine concentrates on the main Examiner tool. 
A mathematical discussion of data flow analysis, in chapter ten, is
not necessary to the operation of SPARK, but provides background and
explanation.  Verification, and the instruments that support it, are
reviewed in chapter eleven.  Chapter twelve examines the rather vague
practice of design, and proposes the INFORMED (INformation Flow
Oriented MEthod of Design) process, although it seems to be limited to
some admittedly useful principles.  A list of similar precepts makes
up the eponymous programming "Techniques" of chapter thirteen. 
Chapter fourteen retails a number of case studies of the possible use
of SPARK for various applications: the simpler ones also contain
source code.

Both the writing in the book, and the explanations of SPARK, are
clear.  Formal methods of architecture and programming are not well
understood, and this text does provide some justification for the
exercise, although more evidence and support would be welcome.  I
recommend this work not only to those interested in more secure
applications development, but also to those needing more information
about formal methods in composition and system architecture.

copyright Robert M. Slade, 2003   BKHISTSA.RVW   20030913