Document Type
Article
Date
1999
Embargo Period
8-29-2012
Keywords
software development, C++, higher-order logic, category theory, secure e-mail, privacy
Language
English
Disciplines
Computer Sciences
Description/Abstract
Developing systems that are assured to be secure requires precise and accurate descriptions of specifications, designs, implementations, and security properties. Formal specification and verification have long been recognized as giving the highest degree of assurance. In this paper, we describe a software development process that integrates formal verification and synthesis. We demonstrate this process by developing assured sender and receiver C++ code for a secure electronic mail system, Privacy Enhanced Mail. We use higher-order logic for system-requirements specification, design specifications and design verification. We use a combination of higher-order logic and category theory and tools supporting these formalisms to refine specifications and synthesize code. Much of our work is applicable to other secure email protocols, as our development is parameterized, component-based, and reusable.
Recommended Citation
Zhou, Dan; Kuo, Joncheng C.; Older, Susan; and Chin, Shiu-Kai, "Formal Development of Secure Email" (1999). Electrical Engineering and Computer Science. Paper 59.
http://surface.syr.edu/eecs/59