Development of Security Software: A High-Assurance Methodology

Hardin, David
Johnson, D. Randolph
Wagner, Lucas
Whalen, Michael
Hiratzka, T. Douglas
2009
Thumbnail Image

View/Download File

hardin-icfem09-proof.pdf (604.38 KB)

Persistent link to this item

https://hdl.handle.net/11299/217424
Statistics
View Statistics

Journal Title

Journal ISSN

Volume Title

Title

Development of Security Software: A High-Assurance Methodology

Authors

Published Date

2009

Publisher

Springer-Verlag

Type

Report

Abstract

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.

Keywords

Description

Associated research group: Critical Systems Research Group

Related to

Replaces

License

Collections

University of Minnesota Software Engineering Center (UMSEC) Publications

Series/Report Number

Funding information

Isbn identifier

Doi identifier

Previously Published Citation

Proceedings of the 11th International Conference of Formal Engineering Methods (ICFEM 2009).

Suggested citation

Hardin, David; Johnson, D. Randolph; Wagner, Lucas; Whalen, Michael; Hiratzka, T. Douglas. (2009). Development of Security Software: A High-Assurance Methodology. Retrieved from the University Digital Conservancy, https://hdl.handle.net/11299/217424.

Content distributed via the University Digital Conservancy may be subject to additional license and use restrictions applied by the depositor. By using these files, users agree to the Terms of Use. Materials in the UDC may contain content that is disturbing and/or harmful. For more information, please see our statement on harmful content in digital repositories.