REVIEW: "High Integrity Software", John Barnes

Discussion in 'Computer Security' started by Rob Slade, doting grandpa of Ryan and Trevor, Nov 3, 2003.

  1. 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
    %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


    "If you do buy a computer, don't turn it on." - Richards' 2nd Law
    ============= for back issues:
    [Base URL] site
    or mirror
    CISSP refs: [Base URL]mnbksccd.htm
    Security Dict.: [Base URL]secgloss.htm
    Security Educ.: [Base URL]comseced.htm
    Book reviews: [Base URL]mnbk.htm
    [Base URL]review.htm
    Security Educ.:
    Review mailing list: send mail to
    Rob Slade, doting grandpa of Ryan and Trevor, Nov 3, 2003
    1. Advertisements

Ask a Question

Want to reply to this thread or ask your own question?

You'll need to choose a username for the site, which only take a couple of moments (here). After that, you can post your question and our members will help you out.