安全软件理论与软硬件协同设计可行性研究报告

1、安全软件理论与软硬件协同设计可行性研究报告一、项目定义1项目名称安全软件理论与软硬件协同设计2项目领域本项目属于基础产业和高新技术领域，涉及计算机软件与理论，系统芯片设计及计算机应用等学科。二、项目背景1项目背景软件可靠性一直是计算机界关心的关键课题，1967年欧洲软件工程先驱者Floyd提出用归纳断言法来验证程序的正确性；1969年图灵奖获得者Hoare提出使用程序公理系统来验证程序的性质。七十年代的典型程序语言的数学理论并不涉及程序的规范说明，因此不能用于软件的设计和开发。同时期的工作包括着重于程序性质的后验证的方法，被用于一些常用算法的分析与正确性证明，但缺乏支持规范分析和指导安全软件设

2、计的演算技术。长期以来国际上不少软件公司投入了大量的人力、物力和财力探索软件设计可靠性技术。设计严格安全软件系统需要解决下述二项关键技术问题: 建立程序和软件规范的演算系统，在软件开发生命周期各阶段均使用数学演算技术来建立软件设计和开发文档。 设计完整的演算法则用来指导下述关键开发任务：（a）从用户需求导出软件系统各部件的规范说明；（b）从部件的规范说明演算出低层软件模块过程的功能说明。在软件设计中用数学理论来指导严格安全软件系统设计，包括： 同一数学框架中处理程序和软件规范； 用符号演算实现程序和软件规范间的演算； 用谓词演算验证设计方法的正确性； 用代数方法从软件部件的抽象规范说明推算出低

3、层次程序模块各个过程的规范说明。学科负责人自1985年起对设计严格安全软件的完备演算理论进行了深入研究，取得了重大突破。主要创新点有： 演算理论强调了设计正确软件的开发方法和使用数学演算来支持从软件到程序代码的转换； 首先提出程序分解算式并第一次提出了求解规范方程的演算法则； 首次给出程序设计语言的一套完备的代数定律； 首先给出并证明由抽象数据类型产生具体数据类型的完备演算法则； 首次为海量并行程序语言BSP语言建立指称语义和代数转化方法。主要学术成果包括： 首次建立规范的数学模型，并发现求解规范方程(X;Q)S 和 (P;X)S 的演算法则； 创建基于“上下仿真映照对”数据精化完备理论； 创

4、建程序代数(He-Hoare代数)，并用它来支持编译器原型的设计和证明； 提出编程统一理论和连接各类程序理论的数学法则。软件演算理论和数据精化规则被誉为是面向模型软件开发的一个里程碑，是国际标准规范语言Z的精化理论基础，是欧洲系统设计语言B的软件开发方法的理论及基础。学科负责人还参与了包括欧共体“硬件编译器”项目在内的若干国际项目的研究，在前面理论工作的基础上，提出了“软硬件混合计算系统”这一研究方向，同时，在欧洲创立了协同设计研究方向，是1996年协同设计程序委员会主席。这里提出的协同设计系统与原先的设计方法不同，如高速铁路的硬件控制系统，可采用可编程器件，应用软件方法开发一个高速铁路的控制

5、系统模型，看是否达到要求。若不行，只要修改所开发的软件(可由软件描述直接产生硬件的线路图)，直到设计出一个满意的模型化的高速铁路，再实际生产。另外，象西门子公司的自动读电表的硬件控制系统，汽车上的导航控制系统，洗衣机自动控制的芯片等硬件系统的特点是：要使硬件价格便宜，设计时间短，又要保证硬件设计系统准确无误，这导致原先的设计方法很难满足这种要求。事实上，尽管已有若干工作，但迄今为止，软硬件混合系统的分析和设计是一个困难的课题，这是现代控制系统的复杂性和可用芯片发展速度的局限导致的。目前常用的硬件描写语言（例如VHDL和VERILOG）允许设计者在抽象设计的不同层次间进行自由的混合，在低层设计方

6、面，如：基本电路(例：晶体管、门电路、寄存器)分层的、结构化的网链；在高层设计方面，如：设计操作的行为表达。但实际上缺乏行为语句。多数设计方法依赖于仿真器的支持，设计中的问题通过多次使用仿真程序来发现，因而开发周期和产品的可靠性都受到了很大的限制。近年来也有应用计算逻辑方法来验证微处理器的正确性的尝试，包括高阶逻辑验证工具HOL、函数编程和抽象状态机等技术。然而此类形式的技术不能用来替代传统的仿真技术。目前急切需要的是一个基于形式化方法的设计技术，包括使用仿真技术来支持整个设计的可视化和开发过程。形式化的法则可以让硬件工程师来选择各类设计参数和细节结构，而最后产品的体系结构仍然由工程设计人员来

7、确定。有关想法还被应用到各种计算范例中(例：用OCCAM写的程序和硬件的微代码)，同时CSP理论得到了充分的发展，提供了自动工具(OCCAM转换系统)。该系统被用于T800浮点单元的开发中，使T800提前一年完成。 在工业界，模拟很大程度上被认为与验证是同义的，设计过程经常遵循由规范得到实现的过程，二者可通过一系列的输入来进行模拟，模拟可以重复进行，这样，错误之处将得以发现、改正。1993年至1996年，学科负责人与Intel公司硬件验证小组和Cornell大学合作，设计了一个硬件编译器。这类源语言的特征是：(1)对通过同步信息传送的并行进程、通讯作了明确的描述；(2)非常自然地描述数字系统。

8、这个项目展示了怎样使用“握手模式的规范”来为延时不敏感电路和时钟电路产生一套等价的规格说明。一个自动工具被用于检查“低层的实现是否符合了它们的规范”。该研究结果表明，应着重考虑在一个给定的系统中建立概念间的联系，这种联系在于：(a)状态图(用来描术基本电路的行为)；(b)延时不敏感代数(Delay-Insensitive Alebraic)(用来详细说明延时不敏感电路)；(c)通讯序列进程(用来描述通讯界面)；(d)时钟进程代数(用来描述同步电路)；(e)控制和数据界面(用来将控制模式和数据模式联系起来)间的关系，这清楚地说明了要一个统一构架来处理不同范式、概念间的界面的迫切性。过去几年里，学

9、科负责人在微处理器验证方面也作了一些成功的工作，有些工作采用HOL(即High Order Logic)系统，有些工作以“功能演算”和“抽象状态机”为基础，不管怎样，形式化方法始终不能替代已有的模拟方法。所需要的一种方法，是使设计过程能以形式化技术为基础，但所包含的模拟过程能使设计形象化，有助于系统的开发。形式化的规则被引用进来，能帮助硬件工程师更正确地计算参数，考虑设计细节，为工程判断上的决策提供方法。这种将形式语义和可验证的模拟器组合起来的方法将为工程设计带来更高的可靠性。解决仿真与合成的不一致性是关键问题。在软硬件混合系统设计的不同阶段所使用的系统语言是不同的。在需求分析阶段，时段逻辑语

10、言和通讯进程代数会用来描写系统的实时性质以及它和周边环境的交互功能。设计阶段会使用一个并行语言来实现需求阶段所提出的函数和非函数功能，高级分解器会将这样一个程序自动分解为软件子系统和硬件子系统的描写，机器语言和网表语言又是软件编译器和硬件综合器的目标语言。为了保证设计方法的正确性，设计过程被用到的多类语言就必须在同一语义框架中加以形式化处理。这也被用来保证多类转换器(软硬件分析器，硬件综合器，软件编译器)设计的正确性。为了支持产品的优化设计，协同设计方法还得提供一套精化法则用来实现语义等价设计之间的转换，并基于代数语义进行等价性证明。在此基础上，说明仿真器的工作与形式化描述的一致性。上述这些使

11、得系统设计可逐步引入多类优化来减少物理资源的共享和控制逻辑的切换。同时，工具也是必需的。协同设计技术所使用的多类支持工具包括：系统性能分析工具、系统分解器、交互式仿真器等。这里的主要挑战是设计一个软硬件混成系统的统一语义框架用来处理、验证多类转换系统的正确性。这是基于语义等价变换设计方法的数学基础，也是构造多类工具的逻辑基础。由于在混成型系统设计各个阶段设计人员会使用各种不同规范、编程和设计语言与范式，而多种文档之间的转换又依赖于语义等价转换软件，为这一大类语言设计共同的语义模型就成为整个设计方法的关键难点。为了减少模型的复杂性，设计方法也得建立不同的语言之间的连接技术和变换法则。语义等价性问

12、题是必须讨论和解决的。在软硬件混成系统中，硬件的并行机制是建立在共享变量和信号驱动之上的，但软硬件之间的交互依赖于同步通讯机制。这种统一的语义框架就不得不涉及一个面向通讯和状态共享的混合型并行语言。这是在国际上还未研究过的难题。硬件设计语言VERILOG包含多类在软件编程语言中从未使用过的结构和语句，它们的形式化描述和相应的精化法则被国际计算机界认为是对传统语义研究的一个挑战。为了增加该工具的灵活性，除了进行多类性能分析之外，还包括与用户直接交互的通讯手段，这也增加了该软件工具设计和实施的复杂性。还有一个技术难点涉及到软硬件子系统之间的通讯界面的设计，采用传统方法（同步或异步）使该部件结构规范

13、化，但会影响整个混成系统的性能，并且不利于系统的单芯片实现方案。为了增加系统的安全性和可移植性，本项目实施技术将不固定软硬件通讯界面的协议，而根据用户对系统的要求（处理速度、信息量）来设计面向应用的专用通讯界面。在系统的单芯片实施方案中，界面描写最终仍可用硬件来实现。在设计实时嵌入式系统中，由于可用的硬件资源限制（性能、功耗、面积），产品的优化是一个重要课题。软硬件转换器和分解器设计中将结合多类分析优化技术来减少元器件的数目，增加元器件在硬件子系统中的重用性。将对应的结构重组（Reconfigurable）也是一个技术难点。将为软硬件混合系统的可组合描写、分析和设计提供一个综合性的理论框架和设

14、计方法，它们具有下属几个特征：（1）它能处理多类函数和非函数的需求分析，提出模块化和优化的处理方案。（2）基于形式化技术，从而保证目标产品的可靠性和安全性。（3）能容纳多类不同开发语言，并提供它们之间语义等价转换的法则。与硬件系统设计密切联系的软件方面，规格说明的形式化及相应的开发方法和验证工具还未设计出来。更进一步讲，许多现有的形式化方法缺乏足够的应用范围，它们没有将许多性质(如：可靠性、安全性)进行组合考虑。软硬件混合系统关键挑战是：为硬件、软件的协同设计寻找一个统一构架，使我们的设计能跟上“半导体设备及相应软件”复杂性的飞速增加。另外，也要求我们在这相同的构架内，既要解决模拟与数字设备，

15、同时也要解决多时钟系统问题。准备采用Interval Temporal Logic(即ITL)作为高层规范的描述工具，与其它逻辑不同，ITL既能用来描述顺序系统，又能用来描述并行系统，同时ITL又强有力地支持工业界应用系统的安全性、实时性、可靠性等性质。由于模拟方法太花时间，最终不能绝对保证硬件设计的准确性。而向实际工业界应用的硬件系统，首先要保证准确，同时又要提高开发速度，所以要研究面向“这些工业系统”硬件设计的软件开发方法，“硬件规范”用ITL来描述，使设计的准确性归约到上述ITL公式的准确性。用本学科研究提供的软、硬件混合设计方法，对于硬件系统的设计而言，只要写出相应的软件描述即可。学科

16、负责人在英国工作期间已经将这类方法使用在SONY公司的VCD稳定器和西敏寺银行的智能卡设计上。前者产品成本不到一美元，后者得到了英国工贸部LEVEL-5产品安全证书（最高可靠性）。无论严格安全软件理论还是计算机软硬件协同设计，均站在国际前列。三、项目建设目标在严格安全软件理论与数据精化法则方面：具备国际级影响；形成与欧美相当水平的学派；培养出一个良好的学术梯队；并推出计算机软硬件协同设计平台，为SOC(System On Chip)的设计提供先进的开发工具。这将是典型的具有原创性和自主知识产权的产、学、研密切结合的标志性成果。我国SOC能力十分薄弱，在汽车、航天、家电、医疗行业和金融界等，这样的平台有着极为广泛的应用前景。现在，我国研究人员往往去西方发达国家学习、访问。建议重点学科若被批准，相信国外的研究人员将到这里来学习、访问。四、项目建设所需经费本项目建设总投入经费900万元，其中中央专项资金100万元（即国家计委100万元），上海市政府配套100万元，学校自筹资金（学校教育产业及事业收费收入等）700万元。具体资金投向为：设备与环境730万元；国际学术活动70万元；学科建设资料100万元。本项目拟购的代表性仪器设备有：SUN服务器、主要用于协同计算的IBM主机、用于科学计算的IBM小型机等。五、项目建设已有条件、优势和特点学科所在的软件学院是国家35所软件学院之