Security modeling and correctness proof using Specware and Isabelle
Loading...
Authors
Ng, Eng Siong
Koh, Chuan Lian
Subjects
Advisors
Auguston, Mikhail
Levin, Timothy E.
Date of Issue
2008-12
Date
Publisher
Monterey, California. Naval Postgraduate School
Language
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.
Type
Thesis
Description
Series/Report No
Department
Organization
Naval Postgraduate School (U.S.)
Identifiers
NPS Report Number
Sponsors
Funding
Format
xviii, 126 p. ;
Citation
Distribution Statement
Approved for public release; distribution is unlimited.
Rights
This publication is a work of the U.S. Government as defined
in Title 17, United States Code, Section 101. As such, it is in the
public domain, and under the provisions of Title 17, United States
Code, Section 105, is not copyrighted in the U.S.