• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文学位 >High-confidence development of secure e -mail systems.
【24h】

High-confidence development of secure e -mail systems.

机译：高安全性开发安全电子邮件系统。

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Building systems that are assured to be secure requires precise and accurate descriptions of system security properties, which must then be accounted for at the implementation level. It is thus essential to have both a correct system specification satisfying these properties and a valid refinement of this specification into actual working code.;In this thesis a software development methodology is adopted that addresses these concerns. The methodology uses a combination of higher-order logic, algebraic specifications, and category theory to integrate formal specification and verification, and code generation. It supports the reuse of specification, verification, and implementation through composition, parameterization, and component-based design. Higher-order logic provides a means to assure the correctness of design, and acts as a bridge between code generation and refinement verification. Algebraic specifications provide the framework for component reuse. Category theory furnishes the means for composing specifications and refinements.;As a concrete illustration of this methodology, it is applied to the electronic mail system, complying with "Internet Engineering Task Force (IETF) standard Privacy Enhanced Mail." This system's top-level security properties and protocols are first defined through higher-order logic, verified to satisfy the required security properties, and instantiated by adding specific data structures and operations. These instantiations are then verified to be correct using higher-order logic. Finally, the design specifications are refined to C++ code through stepwise refinements and compositions of these refinements.
机译：确保安全的构建系统需要对系统安全属性进行准确的描述，然后必须在实现级别进行说明。因此，既要有一个满足这些特性的正确的系统规范，又要对该规范进行有效的完善以使其成为实际的工作代码，这是至关重要的。本文采用了一种软件开发方法来解决这些问题。该方法结合了高阶逻辑，代数规范和类别理论，以集成形式规范和验证以及代码生成。它通过组成，参数化和基于组件的设计支持规范，验证和实现的重用。高阶逻辑提供了一种确保设计正确性的方法，并充当了代码生成和优化验证之间的桥梁。代数规范提供了组件重用的框架。类别理论为构成规范和细化提供了手段。作为该方法的具体说明，它被应用于电子邮件系统，符合“ Internet工程任务组（IETF）标准隐私增强邮件”。该系统的顶级安全属性和协议首先通过高阶逻辑进行定义，经过验证以满足所需的安全属性，然后通过添加特定的数据结构和操作进行实例化。然后使用高阶逻辑将这些实例验证为正确的。最后，通过逐步完善和完善这些构成，将设计规范完善为C ++代码。

著录项

  • 作者

    Zhou, Dan.;

  • 作者单位

    Syracuse University.;

  • 授予单位 Syracuse University.;
  • 学科 Computer Science.;Engineering System Science.
  • 学位 Ph.D.
  • 年度 1999
  • 页码 352 p.
  • 总页数 352
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号