软件工程

软件开发经过长时间的发展,已经成为一种工程,跟制造业中造车造房子一样,很多的大型软件都是由各个小的模块组成,各模块之间的交互通过 API 接口,相当于螺丝和螺帽的关系。在软件开发过程中,要保证软件的质量和安全,每个开发环节都至关重要。传统的软件工程中,开发模型有很多种,从需求出发,经过多次的迭代,从而到最终的软件产品,比如熟知的 V 字模型(V-model,是瀑布模型的扩展版本),就包含这样几个阶段:需求分析、概要设计、详细设计、软件编码、单元测试、集成测试、系统测试、验收测试。

瀑布模型 waterfall

在这样的模型中,软件产品的安全和质量主要侧重在后期。

V 模型

通常验证一个已有的软件产品的正确性(通俗得说,就是一段程序),一种方案是建立一个数理模型,与这个软件产品对应,然后在这个模型中,所有的安全性质都被证明,我们就可以说,这个模型是正确的。模型可以看做是软件产品的抽象,模型的行为肯定可以对应到具体产品中的行为。通过这个方法,我们可以验证软件产品的一部分行为。另外一种方案是,从数理模型出发,然后得到软件产品。

安全认证标准

DO-178B

CC 标准

CC 安全标准(Common Criteria for Information Technology Security Evaluation)是国际标准化组织制定的对系统和软件的安全评判标准,截止到目前,版本是 3.1, 编号(ISO/IEC 15408)。

华为有三十多个产品获得了认证

CC 标准总共分为 7 级。

级别 定义 英文
EAL 1 功能测试 Functionally Tested
EAL 2 结构测试 Structurally Tested
EAL 3 系统性测试和检查 Methodically Tested and Checked
EAL 4 系统性设计、测试、复查 Methodically Designed, Tested and Reviewed SUSE Linux Server, Red Hat Linux
EAL 5 部分形式化的设计和测试 Semiformally Designed and Tested IBM System z
EAL 6 部分形式化验证的设计和测试 Semiformally Verified Design and Tested integrity-178B RTOS
EAL 7 形式化的设计和测试 Formally Verified Design and Tested

形式化方法