Applying Formal Methods to the Design of Smart Card Software

Michael Butler, Pieter H. Hartel, Mark Longley, Eduard de Jong

    Research output: Book/ReportReportOther research output

    13 Downloads (Pure)

    Abstract

    The goal of this work is the design of a language for the implementation of smart card applications, specifically an operating system, as high integrity software. The integrity of a piece of software is demonstrated by proving various properties of the software. The language must therefore exclude any constructs that would make such proofs unreasonably difficult. An untyped language is not only very difficult to reason about formally but also allows many unchecked run-time errors that are eliminated in a, suitably, typed language. We would like the type system of the language to be strong, expressive and simple. Unfortunately the language is required to be able implement certain routines that might normally be part of the run-time system, notably the storage allocation routines. This requirement is likely to force the adoption of a weaker type system than we would ideally prefer. In order to understand the consequences of this requirement we first had to understand in more detail the storage allocation system required. To this end we prepared an initial Z specification of a memory manager for a smart card system. We then produced an executable specification and a Miranda implementation of the memory manager. These led to a modified Z specification for the existing implementation in both an abstract and refined form. The refined form of the modified Z specification was further refined to a detailed design. This was followed by some analysis about the general requirements and implications of a storage allocation function and an example implementation in Modula-3. Finally a proposal for a type system was prepared, describing the advantages of certain choices and the problems introduced by others.
    Original languageUndefined
    Place of PublicationUniversity of Southampton
    PublisherUniversity of Southampton
    Number of pages48
    Publication statusPublished - 1997

    Publication series

    NameTechnical Report / Declarative Systmes and Software Engineering Group
    PublisherUniversity of Southampton
    No.DSSE-T

    Keywords

    • IR-55700
    • SCS-Cybersecurity
    • EWI-1102

    Cite this

    Butler, M., Hartel, P. H., Longley, M., & de Jong, E. (1997). Applying Formal Methods to the Design of Smart Card Software. (Technical Report / Declarative Systmes and Software Engineering Group; No. DSSE-T). University of Southampton: University of Southampton.
    Butler, Michael ; Hartel, Pieter H. ; Longley, Mark ; de Jong, Eduard. / Applying Formal Methods to the Design of Smart Card Software. University of Southampton : University of Southampton, 1997. 48 p. (Technical Report / Declarative Systmes and Software Engineering Group; DSSE-T).
    @book{81f1d8e816144304acdc71fe190abf85,
    title = "Applying Formal Methods to the Design of Smart Card Software",
    abstract = "The goal of this work is the design of a language for the implementation of smart card applications, specifically an operating system, as high integrity software. The integrity of a piece of software is demonstrated by proving various properties of the software. The language must therefore exclude any constructs that would make such proofs unreasonably difficult. An untyped language is not only very difficult to reason about formally but also allows many unchecked run-time errors that are eliminated in a, suitably, typed language. We would like the type system of the language to be strong, expressive and simple. Unfortunately the language is required to be able implement certain routines that might normally be part of the run-time system, notably the storage allocation routines. This requirement is likely to force the adoption of a weaker type system than we would ideally prefer. In order to understand the consequences of this requirement we first had to understand in more detail the storage allocation system required. To this end we prepared an initial Z specification of a memory manager for a smart card system. We then produced an executable specification and a Miranda implementation of the memory manager. These led to a modified Z specification for the existing implementation in both an abstract and refined form. The refined form of the modified Z specification was further refined to a detailed design. This was followed by some analysis about the general requirements and implications of a storage allocation function and an example implementation in Modula-3. Finally a proposal for a type system was prepared, describing the advantages of certain choices and the problems introduced by others.",
    keywords = "IR-55700, SCS-Cybersecurity, EWI-1102",
    author = "Michael Butler and Hartel, {Pieter H.} and Mark Longley and {de Jong}, Eduard",
    note = "Imported from DIES",
    year = "1997",
    language = "Undefined",
    series = "Technical Report / Declarative Systmes and Software Engineering Group",
    publisher = "University of Southampton",
    number = "DSSE-T",
    address = "United Kingdom",

    }

    Butler, M, Hartel, PH, Longley, M & de Jong, E 1997, Applying Formal Methods to the Design of Smart Card Software. Technical Report / Declarative Systmes and Software Engineering Group, no. DSSE-T, University of Southampton, University of Southampton.

    Applying Formal Methods to the Design of Smart Card Software. / Butler, Michael; Hartel, Pieter H.; Longley, Mark; de Jong, Eduard.

    University of Southampton : University of Southampton, 1997. 48 p. (Technical Report / Declarative Systmes and Software Engineering Group; No. DSSE-T).

    Research output: Book/ReportReportOther research output

    TY - BOOK

    T1 - Applying Formal Methods to the Design of Smart Card Software

    AU - Butler, Michael

    AU - Hartel, Pieter H.

    AU - Longley, Mark

    AU - de Jong, Eduard

    N1 - Imported from DIES

    PY - 1997

    Y1 - 1997

    N2 - The goal of this work is the design of a language for the implementation of smart card applications, specifically an operating system, as high integrity software. The integrity of a piece of software is demonstrated by proving various properties of the software. The language must therefore exclude any constructs that would make such proofs unreasonably difficult. An untyped language is not only very difficult to reason about formally but also allows many unchecked run-time errors that are eliminated in a, suitably, typed language. We would like the type system of the language to be strong, expressive and simple. Unfortunately the language is required to be able implement certain routines that might normally be part of the run-time system, notably the storage allocation routines. This requirement is likely to force the adoption of a weaker type system than we would ideally prefer. In order to understand the consequences of this requirement we first had to understand in more detail the storage allocation system required. To this end we prepared an initial Z specification of a memory manager for a smart card system. We then produced an executable specification and a Miranda implementation of the memory manager. These led to a modified Z specification for the existing implementation in both an abstract and refined form. The refined form of the modified Z specification was further refined to a detailed design. This was followed by some analysis about the general requirements and implications of a storage allocation function and an example implementation in Modula-3. Finally a proposal for a type system was prepared, describing the advantages of certain choices and the problems introduced by others.

    AB - The goal of this work is the design of a language for the implementation of smart card applications, specifically an operating system, as high integrity software. The integrity of a piece of software is demonstrated by proving various properties of the software. The language must therefore exclude any constructs that would make such proofs unreasonably difficult. An untyped language is not only very difficult to reason about formally but also allows many unchecked run-time errors that are eliminated in a, suitably, typed language. We would like the type system of the language to be strong, expressive and simple. Unfortunately the language is required to be able implement certain routines that might normally be part of the run-time system, notably the storage allocation routines. This requirement is likely to force the adoption of a weaker type system than we would ideally prefer. In order to understand the consequences of this requirement we first had to understand in more detail the storage allocation system required. To this end we prepared an initial Z specification of a memory manager for a smart card system. We then produced an executable specification and a Miranda implementation of the memory manager. These led to a modified Z specification for the existing implementation in both an abstract and refined form. The refined form of the modified Z specification was further refined to a detailed design. This was followed by some analysis about the general requirements and implications of a storage allocation function and an example implementation in Modula-3. Finally a proposal for a type system was prepared, describing the advantages of certain choices and the problems introduced by others.

    KW - IR-55700

    KW - SCS-Cybersecurity

    KW - EWI-1102

    M3 - Report

    T3 - Technical Report / Declarative Systmes and Software Engineering Group

    BT - Applying Formal Methods to the Design of Smart Card Software

    PB - University of Southampton

    CY - University of Southampton

    ER -

    Butler M, Hartel PH, Longley M, de Jong E. Applying Formal Methods to the Design of Smart Card Software. University of Southampton: University of Southampton, 1997. 48 p. (Technical Report / Declarative Systmes and Software Engineering Group; DSSE-T).