Browsing by Author "Hardin, David"

Now showing 1 - 4 of 4
  • Thumbnail Image
    Item
    A DSL for cross-domain security
    (High Integrity Language Technology ACM SIGAda’s Annual International Conference (HILT 2012), 2012) Hardin, David; Slind, Konrad; Whalen, Michael; Pham, Hung T.
  • Thumbnail Image
    Item
    Development of Security Software: A High-Assurance Methodology
    (Springer-Verlag, 2009) Hardin, David; Johnson, D. Randolph; Wagner, Lucas; Whalen, Michael; Hiratzka, T. Douglas
    This paper reports on a project to exercise, evaluate and enhance a methodology for developing high assurance software for an embedded system controller. In this approach, researchers at the National Security Agency capture system requirements precisely and unambiguously through functional specifications in Z. Rockwell Collins then implements these requirements using an integrated, model-based software development approach. The development effort is supported by a tool chain that provides automated code generation and support for formal verification. The specific system is a prototype high speed encryption system, although the controller could be adapted for use in a variety of critical systems in which very high assurance of correctness, reliability, and security or safety properties is essential.
  • Thumbnail Image
    Item
    Introduction to the Guardol Language and Verification System
    (2011) Hardin, David; Slind, Konrad; Whalen, Michael; Pham, Hung T.
    Guardol is a high-level programming language intended to facilitate the construction of correct network guards. The Guardol system generates Ada code from Guardol programs. It also provides specification and automated verification support: guard specifications are formally translated to SMT format and passed to a new decision procedure dealing with functions over tree-structured data. The result is that difficult properties of Guardol programs can be proved fully automatically.
  • Thumbnail Image
    Item
    The Guardol Language and Verification System
    (Springer-Verlag, 2012) Hardin, David; Slind, Konrad; Whalen, Michael; Pham, Hung T.
    Guardol is a domain-specific language designed to facilitate the construction of correct network guards operating over tree-shaped data. The Guardol system generates Ada code from Guardol programs and also provides specification and automated verification support. Guard programs and specifications are translated to higher order logic, deductively transformed to a form suitable for a SMT-style decision procedure for recursive functions over tree-structured data. The result is that difficult properties of Guardol programs can be proved fully automatically.