Browsing by Author "Slind, Konrad"

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
    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
    Resolute: An Assurance Case Language for Architecture Models
    (ACM, 2016) Gacek, Andrew; Backes, John; Cofer, Darren; Slind, Konrad; Whalen, Michael
    Arguments about the safety, security, and correctness of a complex system are often made in the form of an assurance case. An assurance case is a structured argument, often represented with a graphical interface, that presents and supports claims about a system's behavior. The argument may combine different kinds of evidence to justify its top level claim. While assurance cases deliver some level of guarantee of a system's correctness, they lack the rigor that proofs from formal methods typically provide. Furthermore, changes in the structure of a model during development may result in inconsistencies between a design and its assurance case. Our solution is a framework for automatically generating assurance cases based on 1) a system model specified in an architectural design language, 2) a set of logical rules expressed in a domain specific language that we have developed, and 3) the results of other formal analyses that have been run on the model. We argue that the rigor of these automatically generated assurance cases exceeds those of traditional assurance case arguments because of their more formal logical foundation and direct connection to the architectural model.
  • 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.