Security Modeling and Correctness Proof Using Specware and Isabelle

Abstract

Security modeling is the foundation to formal verification which is a core requirement for high assurance systems. This thesis explores how security models can be built in a simple and expressive manner using the Metaslang specification language in Specware. The models are subsequently translated, via the Specware to Isabelle Interface, to be proven for correctness in Isabelle which is a generic, interactive theorem proving environment. It is found that the translation between Specware and Isabelle is almost seamless and there is much potential in the use of Isabelle/HOL to discharge proof obligations that arise in developing Specware specifications although the actual proving requires substantial knowledge and experience in logical calculus.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Dec 01, 2008
Accession Number
ADA494053

Entities

People

  • Chuan L. Koh
  • Eng S. Ng

Organizations

  • Naval Postgraduate School

Tags

Communities of Interest

  • Advanced Electronics

DTIC Thesaurus Topics

  • Algorithms
  • Calculus
  • Computer Access Control
  • Computer Programming
  • Computer Science
  • Computers
  • Construction
  • Environment
  • Graphical User Interface
  • Language
  • Lessons Learned
  • Mathematics
  • Operating Systems
  • Programming Languages
  • Software Development
  • Specifications
  • Translations

Fields of Study

  • Computer science

Readers

  • Mathematical Modeling and Probability Theory.
  • Software Engineering.