A formal approach to contract verification for high-integrity applications

K-REx Repository

Show simple item record

dc.contributor.author Zhang, Zhi
dc.date.accessioned 2016-08-10T21:21:57Z
dc.date.available 2016-08-10T21:21:57Z
dc.date.issued 2016-08-01 en_US
dc.identifier.uri http://hdl.handle.net/2097/32880
dc.description.abstract High-integrity applications are safety- and security-critical applications developed for a variety of critical tasks. The correctness of these applications must be thoroughly tested or formally verified to ensure their reliability and robustness. The major properties to be verified for the correctness of applications include: (1) functional properties, capturing the expected behaviors of a software, (2) dataflow property, tracking data dependency and preventing secret data from leaking to the public, and (3) robustness property, the ability of a program to deal with errors during execution. This dissertation presents and explores formal verification and proof technique, a promising technique using rigorous mathematical methods, to verify critical applications from the above three aspects. Our research is carried out in the context of SPARK, a programming language designed for development of safety- and security-critical applications. First, we have formalized in the Coq proof assistant the dynamic semantics for a significant subset of the SPARK 2014 language, which includes run-time checks as an integral part of the language, as any formal methods for program specification and verification depend on the unambiguous semantics of the language. Second, we have formally defined and proved the correctness of run-time checks generation and optimization based on SPARK reference semantics, and have built the certifying tools within the mechanized proof infrastructure to certify the run-time checks inserted by the GNAT compiler frontend to guarantee the absence of run-time errors. Third, we have proposed a language-based information security policy framework and the associated enforcement algorithm, which is proved to be sound with respect to the formalized program semantics. We have shown how the policy framework can be integrated into SPARK 2014 for more advanced information security analysis. en_US
dc.description.sponsorship US Air Force Office of Scientific Research under contract FA9550-09-1-0138 en_US
dc.language.iso en_US en_US
dc.publisher Kansas State University en
dc.subject Formal Methods en_US
dc.subject Language Semantics en_US
dc.subject Program Verification en_US
dc.title A formal approach to contract verification for high-integrity applications en_US
dc.type Dissertation en_US
dc.description.degree Doctor of Philosophy en_US
dc.description.level Doctoral en_US
dc.description.department Department of Computing and Information Sciences en_US
dc.description.advisor John M. Hatcliff en_US
dc.date.published 2016 en_US
dc.date.graduationmonth August en_US

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search K-REx

Advanced Search


My Account


Center for the

Advancement of Digital


118 Hale Library

Manhattan KS 66506

(785) 532-7444