Loading ...
Sorry, an error occurred while loading the content.

REVIEW: "High Integrity Software", John Barnes

Expand Messages
  • Rob, grandpa of Ryan, Trevor, Devon & Ha
    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,
    Message 1 of 1 , Nov 3 7:08 AM
      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@...
      %O http://www.amazon.com/exec/obidos/ASIN/0321136160/robsladesinterne
      %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

      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

      rslade@... slade@... rslade@...
      Computer Security Day, November 30 http://www.computersecurityday.com/
      victoria.tc.ca/techrev/mnbksc.htm sun.soci.niu.edu/~rslade/secgloss.htm
    Your message has been successfully submitted and would be delivered to recipients shortly.