软件工程

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

瀑布模型 waterfall

在这样的模型中,软件产品的安全和质量主要侧重在后期。有些小作坊的软件公司,对软件产品并没有非常高的安全要求,只需要对软件进行必要的测试就足够了。然而,对像航天、轨道交通、卫星中的系统而言,仅仅是测试是不够的。倘若用测试的方法,一是不能够穷尽所有的可能,二是仅能对最终的软件进行测试。

V 模型

安全认证标准

关于系统和软件的安全性,有很多不同的安全评估标准,这些标准基本上是美国和欧洲多国的组织制定的。比如国际电工委员会制定的 IEC 61508标准,或者 CSSA,DO-178B/C,EN 50128,CC 标准等。不同的认证标准会有不同的等级,比如 EN 50128,就有 0 - 4 五个 SIL 等级(Software Integrity Level )。

案例

华东技术研究所开发的实时操作系统(锐化认证版)就是中国首个获得 SIL 4 标准的实时操作系统 RTOS。

另外一个比较著名的认证标准 就是 CC 标准,因为其认证标准的严格以及被认可度,成为了国内很多做软件安全公司的目标。

CC 标准

CC 安全标准(Common Criteria for Information Technology Security Evaluation)是国际标准化组织制定的对系统和软件的安全评判标准,截止到目前,版本是 3.1, 编号(ISO/IEC 15408)。CC 官网上,公开了一个已经获得认证的软件产品列表,比如华为就有几十多个产品获得了不同级别的认证。

级别 定义 英文 案例
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

CC 标准总共分为 7 级,不同等级的区别在于形式化被应用在各个阶段的比例多少。CC 标准级别越高,形式化就用得越多。

CC 标准

形式化开发

通常验证一个已有的软件产品的正确性(通俗得说,就是一段程序),一种方案是反向建立一个数理模型(抽象),与这个软件产品对应,然后在这个模型中,所有的安全性质都被精确得梳理描述,通过模型检测、定理证明等手段被证明后,我们就可以说,这个模型是正确的,满足开发者预期的。模型可以看做是软件产品的抽象,模型的行为可以对应到具体产品中的行为。通过这个方法,我们可以验证软件产品的一部分行为。

Leonard Lensink

另外一种方案是,从产品设计出发,建立对应的数理模型,然后通过代码生成,得到软件产品(这种方法是 correct by construction,也可以称为 model-based development)。我们称用形式化方法用来开发软件的过程为形式化开发。不同于传统软件的开发过程,形式化开发需要对多个开发过程进行验证,比如需求阶段和设计阶段,但是形式化开发可以省去对最终软件产品的测试。在工业界和学术界的共同努力之下,形式化方法已经可以很好的应用于软件的开发过程。一个简单的过程如下图所示:

![简单的形式化开发过程](http://pimw1cy4t.bkt.clouddn.com/Screenshot 2018-12-05 at 14.18.04.png)

基于模型的开发,主要是寻找一种合适的形式化语言来描述系统,不同的形式化语言有不同的优劣,表达能力和描述目标。
成熟的形式化平台需要针对特定的目标,表达能力至少需要覆盖需求设计,建立的模型需要能够顺利得到验证,并且生成指导性或者工业级别的代码。

在工业级应用比较多的有 B 方法以及 SCADE。

B 方法形式化描述语言

发展历史

Jean-Raymond Abrial 在 80 年代提出 Z 语言(Z notation),用于形式化描述系统和软件,在90年代, Abrial 改进了 Z,提出了 B-Method,B-Method 的提出,是为了更好得应用于工业性的软件开发,当时 B-Method 的维护和使用主要是法国的铁路公司 RATP,他们希望将B-Method 验证轨道交通系统的正确性。后来,Alstom 和 Siemens 信号公司都开始采用 B-Method,用于辅助验证地铁信号系统。

五年前当时我还很年轻😂

B-Method 最成功的案例是验证巴黎地铁14 号线(后来还有 1 号线)控制系统,14 号线是无人驾驶的地铁线,其控制系统跑在 OpenVMS 操作系统上。当时整个控制系统的形式化模型(B 模型)就有 11 万行,这些模型生成 8 万多行的 Ada 代码。现在用 B-Method 验证系统和软件已经比较成熟,RATP 公司开发了 B-Method 开发平台 Atelier B,目前是版本 4.2.1。另外一些工业应用是 2006 年投入使用的巴黎 Roissy 机场的运输车系统,巴塞罗那地铁,法国 Societe 银行的 reconciliation系统等等。

![巴黎14号线无人驾驶](http://pimw1cy4t.bkt.clouddn.com/Screenshot 2018-12-04 at 10.27.41.png)

在巴黎留学期间,14 号线在学校刚好有一站,第一次坐就跑去了车头,车头没有驾驶室,只有透明的玻璃,穿梭在地下,感觉是现实版的 temple run 😂

但是 B-Method 用起来还是太复杂了,于是 Abrial 又提出 Event-B,Event-B 结合了 B-Method 和 Action system,更加简单和易用,能够快速得应用于工业级软件和系统的描述和验证。Event-B 被应用在很多 CC EAL6+ 的验证上,比如 Ariane 5 航天器的飞行系统 EADS [Marc09],下图是 B-Method 在全球范围里的工业应用。

![B 方法在全球的使用](http://pimw1cy4t.bkt.clouddn.com/Screenshot 2018-12-04 at 10.24.57.png)

Event-B

Event-B 是面向系统级别建模的形式化方法,其描述语言基于集合论和一阶逻辑,另外一个最大的亮点是其支持精化理论,对特别的复杂的系统,可以一步一步来完成建模。 Event-B 的模型最后也可以直接生成高级语言的代码(C,C++,Java,etc)。

![基于精化的形式化开发框架](http://pimw1cy4t.bkt.clouddn.com/Screenshot 2018-12-05 at 14.19.16.png)

为什么要精化?

一步就完成对整个系统的建模,会弄脏自己的双手和自己的容颜,会使得模型超级庞大,并且不易操控,也不易做证明。一般的过程是,描述一个非常抽象的模型(对应高层次的设计 High level design),然后一层一层得叠加条件,(对应低层次的设计 Low level design),每一层都是上一层的精化,每一层都比上一层更具体(concrete),这样可以在任何想要的抽象级别上停止,但最后一层的模型,需要对整个系统都进行了描述。

Event-B 模型

Event-B 模型可以看做是一个状态迁移系统,所有变量的一种取值看做模型的一个状态,模型的行为(事件)改变变量的值,生成一个新的状态。模型的安全性用不变式(谓词语句)来定义的,这些不变式需要在每个状态中都得到满足。所以,一个模型是否正确,只要保证在模型所有可达的状态中,不变式都能够得到保证。Event-B 模型的组成主要有静态部分(变量)和动态部分(事件)两部分。Event-B 的开发平台是 基于 eclipse 的 Rodin,在描述完模型后,自动生成证明义务(proof obligations),证明义务可以用很多 SMT(比如 Z3) 证明,复杂的义务需要人工参与证明,另外,Rodin 还支持安装模型检测插件,也可以验证时序性质。

SCADE

另一个基于模型开发的工业级应用方法就是大名鼎鼎的 SCADE(Safety-Critical Application Development Environment)了。SCADE 的目标就是为了开发高安全性的应用程序,主要是针对嵌入式软件,由法国Esterel Technologies 公司研制,并且达到欧洲航空业 DO-178B 标准A级(航空航天行业最高安全级别)。SCADE 局限了开发范围,所以没有 Event-B 那么灵活,但是其支持图形化设计开发方式,能够覆盖从需求分析到代码实现的整个软件开发流程。SCADE 的模型,通过高安全性验证的代码生成器 KCG,保证了最终的软件产品跟需求同步。

SCADE 的模型非常适用于设计与环境交互的嵌入式系统,尤其是航空航天以及汽车驾驶等系统。

与 SCADE 合作的案例

  • Crane Aerospace & Electronics

Event-B 模型的组成

形式化验证案例

处理器

  • 剑桥 ARM 处理器 [POPL’16]
  • AAMP7G 应用于航空航天的处理器 获得CC-7, DO-178B A 认证

操作系统

  • NICTA 的 seL4 [ SOSP’09]
  • 耶鲁大学的 CertiKOS[PLDI’16, POPL’15, OSDI’16]

编译器

  • 大神 Xavier Rival 的 CompCert [PLDI’09, POPL’10]

基于模型开发类工业级

  • SCADE (法国针对嵌入式系统模型开发公司)
  • prover(瑞典针对地铁系统的模型开发公司)
  • saferiver(法国模型验证公司)

程序分析类工业级

  • diffblue (英国CMBC 以及测试用例自动生成)
  • trustinsoft (法国程序C,C++程序分析)

静态部分 Contexts

Event-B 模型的静态部分由常量集合 constant 和变量集合 variables 组成,变量的取值是模型的状态,

  • 常量 constant (带公理axiom)
  • 变量 variables (类型由不变式给定)

动态部分 Machine

  • 事件