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.

Share

COinS