基于模型检验的软件安全静态分析研究

技术创新

中文核心期刊《微计算机信息》（管控一体化）２００７年第２３卷第１０－３期信息安全

基于模型检验的软件安全静态分析研究

ＲｅｓｅａｒｃｈＯｎＭｏｄｅｌＣｈｅｃｋｉｎｇＢａｓｅｄＳｏｆｔｗａｒｅＳｅｃｕｒｉｔｙＳｔａｔｉｃＡｎａｌｙｓｉｓ

（华中科技大学）黄锦陈晓苏肖道举刘辉宇

ＨＵＡＮＧＪＩＮＣＨＥＮＸＩＡＯＳＵＸＩＡＯＤＡＯＪＵＬＩＵＨＵＩＹＵ

摘要：软件安全静态分析是检测软件安全漏洞的一种手段。本文在总结现有的软件安全静态分析方法的基础上，将在硬件设计领域得到成功应用的模型检验方法引入到软件产品的检验中，给出了一种基于自动机理论的检测软件安全的模型检验方法，阐述了其原理和工作流程，并用实例进行了验证说明。

关键词：静态分析；模型检验；漏洞挖掘；软件安全

中图分类号：ＴＰ３９３．０８文献标识码：Ａ

Ａｂｓｔｒａｃｔ：Ｓｏｆｔｗａｒｅｓｅｃｕｒｉｔｙｓｔａｔｉｃａｎａｌｙｓｉｓｉｓａｎｉｍｐｏｒｔａｎｔｗａｙｏｆｓｏｆｔｗａｒｅｖｕｌｎｅｒａｂｉｌｉｔｙｃｈｅｃｋｉｎｇ．Ｔｈｉｓｐａｐｅｒｓｕｍｍａｒｉｚｅｓｔｈｅｃｕｒｒｅｎｔｓｔａｔｉｃａｎａｌｙｓｉｓｍｅｔｈｏｄｓａｎｄｔｈｅｎｉｍｐｏｒｔｓｔｈｅｍｏｄｅｌｃｈｅｃｋｉｎｇｍｅｔｈｏｄｗｈｉｃｈｈａｓｂｅｅｎｓｕｃｃｅｓｓｆｕｌｌｙｕｓｅｄｉｎｈａｒｄｗａｒｅｄｅｓｉｇｎ．Ｄｅｓｃｒｉｂｅｓａｎａｕｔｏｍａｔａｔｈｅｏｒｙｂａｓｅｄｍｏｄｅｌｃｈｅｃｋｉｎｇｍｅｔｈｏｄｆｏｒｓｏｆｔｗａｒｅｖｕｌｎｅｒａｂｉｌｉｔｙｃｈｅｃｋｉｎｇ．Ｔｈｅｎｅｘｐｌａｉｎｓｉｔｓｐｒｉｎｃｉｐｌｅｓａｎｄｗｏｒｋｉｎｇｆｌｏｗ，ａｎｄａｔｌａｓｔｖａｌｉｄａｔｅｓｉｔｂｙｕｓｉｎｇｅｘａｍｐｌｅ．

Ｋｅｙｗｏｒｄｓ：ｓｔａｔｉｃａｎａｌｙｓｉｓ，ｍｏｄｅｌｃｈｅｃｋｉｎｇ，ｖｕｌｎｅｒａｂｉｌｉｔｙｄｉｇ，ｓｏｆｔｗａｒｅｓｅｃｕｒｉｔｙ

文章编号：１００８－０５７０（２００７）１０－３－００８６－０２

１引言

随着计算机系统广泛应用，系统安全性越来越得到重视。

软件安全漏洞是现代计算机系统的毒瘤，多数恶意攻击都源自

软件产品各种各样的漏洞。由于安全漏洞具有相当的隐蔽性，

如何检测软件中可能存在的安全漏洞已成为信息安全关注的

焦点。目前对于软件漏洞检测的研究有静态分析和动态检测两

个分支，其中静态分析是主要的研究方向。静态分析通过对源

代码的扫描和分析来检测漏洞，不需要改动源代码；动态检测

则通过在程序执行期间对内存和堆栈的监测来检测漏洞，需要

添加并重新编译源代码，增加了系统开销。

模型检验是一种重要的自动化验证方法，它最早由Ｃｌａｒｋｅ

和Ｅｍｅｒｓｏｎ提出，主要通过显式状态搜索或隐式不动点计算来

验证系统的有穷状态和命题性质。模型检验在硬件设计领域的

应用已经比较成熟，在软件安全静态分析上的应用也有研究人

员进行了一些有意义的探索，如基于进程演算的模型检验方

法、基于程序时序逻辑的模型检验方法等等。

软件安全静态分析的难点在于如何定义程序的安全属性以

及如何制定对源代码的约束条件。为了能够更好的描述程序的安

全属性并运用某种形式化的方法对其进行验证，本文基于自动机

的相关理论，通过将软件的源代码和安全属性分别建模为相应的

自动机模型，探讨了一种检测软件安全的模型检验方法。

２现有静态分析方法

静态分析方法的优点在于对目标软件或系统的分析不必

运行系统，可以在系统开发阶段进行。静态分析方法主要有以

下几种：

（１）词法分析和语法分析。该方法通过词法分析和语法分析

建立抽象语法树，抽象语法树只包含和程序实际执行内容相关

的细节，然后在此基础上进行安全性分析。

（２）图形化方法。该方法主要是通过构造程序的控制流图、

数据流图和程序依赖关系图进行安全性分析。

（３）静态切片。该方法将程序分解为较小的称之为“片”的代

码段，使关注点确定在一个较小范围内而不必关注整个程序，

然后借助程序依赖关系图进行安全性分析。

３一种检测软件安全的模型检验方法

３．１基本概念

有限自动机ＦＳＡ（ＦｉｎｉｔｅＳｔａｔｅＡｕｔｏｍａｔａ）：一个用来描述正则

语言的数学模型，由五元组（Ｋ，∑，δ，ｑ０，Ｆ）组成，其中Ｋ是状态

的有限集合；∑是有限输入字母表；δ是Ｋ∑到Ｋ的一个映射，

表示自动机在某状态接受某个输入后的状态转换；ｑ０是初始状

态；ＦＫ是终止状态集合。

下推自动机ＰＤＡ（ＰｕｓｈｄｏｗｎＡｕｔｏｍａｔａ）：一个用来描述上下

文无关文法的数学模型，它在有限自动机的基础上增加了一个

先进后出的存储结构——

—下推栈，使得其分析识别输入的能力

比有限自动机强大。

安全属性模型检验程序包ＭＯＰＳ（ＭｏｄｅｌＣｈｅｃｋｉｎｇＰｒｏｇｒａｍｓ

ｆｏｒＳｅｃｕｒｉｔｙＰｒｏｐｅｒｔｉｅｓ）：包含了检测程序安全属性的体系结构以

及相关工具包。

３．２软件安全建模及检验的基本思想

通常，程序都会执行一些与安全相关的操作，而安全属性

则定义了这些操作的顺序，违背该顺序的操作序列可能导致潜

在的安全漏洞。软件安全检验的目标就是验证程序是否很好地

满足了安全属性。问题的关键在于如何以恰当的形式来定义和

描述安全属性，使得其便于验证。

为简洁起见，对软件安全问题进行抽象，可描述为：

（１）设Ａ是所有与安全属性相关的操作的集合，则Ａ＊（＊表黄锦：硕士研究生

基金项目：国家８６３计划项目，项目号（２００３ＡＡ７１２０２２）

技

术创新

信息安全

您的论文得到两院院士关注

示集合的幂操作）是所有操作序列的集合。

（２）设Ｂ是违背安全属性的所有操作序列的集合，是Ａ＊的

一个子集。

（３）痕迹ｔ∈Ａ＊表示程序中所有可能的执行路径ｐ执行的操作序列。如果ｐ是程序中的实际执行路径，则称ｔ是可实现

的痕迹。

（４）Ｔ包含于Ａ＊，表示所有可实现痕迹的集合。

经过上述抽象，软件安全检验问题即转换为判断Ｔ∩Ｂ是否为空集。如果为空集，则表明软件满足所有的安全属性；否则，表明软件中的某些执行路径违背了安全属性。

通常Ｔ是不可数集，故Ｔ∩Ｂ难以判定，但可以通过限制Ｔ和Ｂ的形式来使Ｔ∩Ｂ可以被判定。由于绝大多数的安全属性可以用正则语言来描述，故可将Ｂ限制为正则语言，而对于正则语言Ｂ，必然存在能够接受Ｂ的ＦＳＡ，设为Ｍ，则有Ｂ＝Ｌ（Ｍ）。Ｌ

（Ｍ）代表有限自动机Ｍ描述的语言，从而可以借助有限自动机

来描述安全属性。

但是必须看到，正则语言不能很好地描述跨函数调用的执行路径，所以Ｔ不能够被限定为正则语言。在这种情况下，函数调用者需要有一个堆栈来存放返回地址，由此而产生的带有堆栈的语言是上下文无关语言。因此，可以将Ｔ建模为上下文无关语言，这样就必然存在一个能够接受Ｔ的ＰＤＡ，设为Ｐ，则有Ｔ＝Ｌ（Ｐ），Ｌ（Ｐ）代表下推自动机Ｐ描述的语言。Ｐ由状态集、栈符号、输入符号和转换函数组成，转换函数定义Ｐ在接收到输入符号时如何进行状态转换。

通过对Ｂ和Ｔ的定义，即可将软件安全检验问题转化为判定Ｌ（Ｍ）∩Ｌ（Ｐ）是否为空。设Ｃ＝Ｌ（Ｍ）∩Ｌ（Ｐ），则Ｃ是正则语言Ｌ（Ｍ）和上下文无关语言Ｌ（Ｐ）的交集，因此Ｃ是上下文无关语言。根据自动机理论，存在许多有效的算法来计算ＰＤＡ和ＦＳＡ的交集，并判定其是否为空。

模型检验流程如图１所示。利用ＭＯＰＳ提供的源代码分析工具从源代码的执行路径里提取所有可实现痕迹，得到程序的控制流图，建模为ＰＤＡ源代码模型，同时将安全属性建模为

ＦＳＡ安全属性模型，然后利用ＭＯＰＳ模型检验语法进行检验。

图１模型检验流程

３．３安全属性的提取

安全属性定义了程序安全操作的顺序，它通过分析系统的规范、约束来提取。这里用一个例子来说明安全属性提取的基本思路。在Ｕｎｉｘ系统中，每一个Ｕｎｉｘ进程都有３个用户ｉｄ：真实用户ＩＤ（ｒｅａｌｕｉｄ）、有效用户ＩＤ（ｅｆｆｅｃｔｉｖｅｕｉｄ）和存储用户ＩＤ

（ｓａｖｅｄｕｉｄ）。真实用户ＩＤ定义了进程的所有者，有效用户ＩＤ则

定义了进程的访问权限。当一个进程具有０级特权的有效用户

ＩＤ，则该进程就具有最高级权限。例如：一个用户执行了ｓｅｔｅｕｉｄ

类进程后，进程的有效用户ＩＤ可能变为０级特权，若真实用户

ＩＤ不具有０级特权，此时就可能允许一个不受信任的具有０级

特权的程序运行，对系统构成潜在威胁。针对上述问题可构造一条安全属性Ｓ：禁止一个有效用户ＩＤ是０级特权的ｓｅｔｅｕｉｄ类进程调用ｅｘｅｃｖ（）去执行不受信任的程序。

３．４安全属性的描述

提取安全属性后，接下来的工作是对其进行数学建模。具体方法是先将其转化为ＦＳＡ，然后将这些ＦＳＡ用ＭＯＰＳ语法进行编码。对上述安全属性Ｓ进行建模并构造ＦＳＡ的过程如下：先创建一个ＦＳＡ来描述一个ｓｅｔｅｕｉｄ进程的有效用户ＩＤ在ｅｕ－ｉｄ＿０状态和ｅｕｉｄ＿１状态之间的迁移，如图２所示。该ＦＳＡ含有两个状态，一个代表有效用户ＩＤ的值为０，另一个为非０。ＦＳＡ通过调用ｓｅｔｅｕｉｄ（０）和ｓｅｔｅｕｉｄ（ｇｅｔｕｉｄ）进行状态的迁移。类似地可以创建另外一个ＦＳＡ来描述一个进程是否调用了ｅｘｅｃｖ，如图３所示。该ＦＳＡ含有两个状态，ａｆｔｅｒ代表进程刚刚调用了ｅｘ－

ｅｃｖ，ｂｅｆｏｒｅ则代表其他的情况。

图２用ＦＳＡ描述ｓｅｔｅｕｉｄ

图３用ＦＳＡ描述ｅｘｅｃｖ

然后将上述的两个ＦＳＡ合并创建一个元ＦＳＡ。一个元ＦＳＡ描述的是多个ＦＳＡ的乘积，元ＦＳＡ的状态空间是所有ＦＳＡ的状态空间的笛卡尔积。本例中的元ＦＳＡ文件ｓｅｔｕｉｄｅｘｅｃｖ．ｍｆｓａ如下：

ｓｅｔｅｕｉｄ．ｆｓａｅｘｅｃｖ．ｆｓａ

ｑｅｕｉｄ＿０ｂｅｆｏｒｅｆｅｕｉｄ＿０ａｆｔｅｒ

该元ＦＳＡ文件由三部分组成，第一行描述的是ｓｅｔｕｉｄ．ｆｓａ和ｅｘｅｃ．ｆｓａ两个ＦＳＡ，元ＦＳＡ由两者之积构成。第二行描述的是元ＦＳＡ的起始状态，ｑ是一个多元组，由来自ＦＳＡｓｅｔｕｉｄ．ｆｓａ的状态ｅｕｉｄ＿０和来自ｅｘｅｃｖ．ｆｓａ的状态ｂｅｆｏｒｅ组成。第三行描述的是元ＦＳＡ的终止状态ｆ，是一个多元组，由来自ＦＳＡｓｅｔｅｕｉｄ．ｆｓａ的状态ｅｕｉｄ＿０和来自ＦＳＡｅｘｅｃｖ．ｆｓａ的状态ａｆｔｅｒ组成。

３．５利用ＭＯＰＳ验证安全属性

构建出描述安全属性的元ＦＳＡ后，就可以利用ＭＯＰＳ工具包对源代码进行验证，验证步骤如下：

（１）预处理并生成控制流图。假设待处理文件为ｆｏｏ．ｃ，则预处理命令为：ｃｐｐｆｏｏ．ｃｆｏｏ．ｌ，生成控制流图的命令为ｒｃ／ｃｃｌ–ｏｆｏｏ．ｃｆｇｆｏｏ．ｌ。ｃｐｐ是ＭＯＰＳ提供的源代码预处理工具，ｃｃｌ是ＭＯＰＳ提供的控制流图生成工具。

（２）合并和压缩控制流图。如果有多个源代码文件，则需要将生成的控制流图进行合并，命令为：ｊａｖａＣｆｇＭｅｒｇｅｆｏｏ．ｃｆｇｆｏｏ１．ｃｆｇｆｏｏ２．ｃｆｇｆｏｏ３．ｃｆｇ。另外如果Ｃ源文件比较大，可以将控制流图参照安全属性进行压缩，命令为：ｊａｖａＣｆｇＣｏｍｐａｃｔｓｅｔｕｉｄｅｘｅｃｖ．ｍｆｓａｆｏｏ．ｃｆｇｍａｉｎｆｏｏ．ｓ．ｃｆｇ。其中ｓｅｔｕｉｄｅｘｅｃｖ．ｍｆｓａ是先前构建的安全属性元ＦＳＡ。

（３）对安全属性和控制流图进行模型检验。

检测命令为：ｊａｖａｃｈｅｃｋｓｅｔｕｉｄｅｘｅｃｖ．ｍｆｓａｆｏｏ．ｓ．ｃｆｇｍａｉｎｆｏｏ．ｓ．ｔｒａ。

（４）将压缩后的控制流图转化为对应的程序路径并查看结果。转化命令为：ｊａｖａＴｒａｎｓｆｏｒｍｆｏｏ．ｃｆｇｆｏｏ．ｓ．ｔｒａｆｏｏ．ｔｒａ。然后违背安全属性的路径就会被写入ｆｏｏ．ｔｒａ文件，可以用ｅｍａｃｓ或ｖｉ等编辑器来查看结果。（下转第４９页）

技术创新

控制管理

您的论文得到两院院士关注

５未来改善

等待微软公司发表更多的关于ＭＳＮＭｅｓｓｅｎｇｅｒ音频／视频协议定义的技术细节，这样我们就可以直接发送伴有文本警报信息的音频／视频流到ＭＳＮＭｅｓｓｅｎｇｅｒ多媒体播放器上，使系统功能更加完善。

论文的创新点：本论文集成了ＭＳＮ、Ｊａｖａ等新技术，实现在线动态音频／视频的监测报警，并通过ＭＳＮＭｅｓｓｅｎｇｅｒ多媒体播放器进行播放验证。现等待微软公司发表更多的关于ＭＳＮ

Ｍｅｓｓｅｎｇｅｒ音频／视频协议定义的技术细节，近一步改进本系统。参考文献：

［１］刘和．数字图象处理及应用．北京：中国电力出版社．２００６

［２］许军峰．联网型智能小区防盗报警系统：西安，

西安交通大学，２００３

［３］殷兆麟．Ｊａｖａ网络编程基础．北京：北方交通大学出版社．２００４．１［４］ＤｉｇｉｔａｌＩｍａｇｅＰｒｏｃｅｓｓｉｎｇ．Ｃａｓｔｌｅｍａｎ，Ｋ．Ｒ．北京：电子工业出版社．２００２．２

［５］张利辉，龚建华，

黄明祥，曲建华基于ｊａｖａ手机的遥感影像协同识别野外作业系统框架设计与实现微计算机信息，２００６，Ｖｏｌ．１０Ｎｏ．１，ｐ２１１－２１４

作者简介：李凤荣（１９６６—），女，汉族，天津工业大学信息与通信

工程学院，副教授，主要从事图像处理、模式识别及计算机网络方面的研究。

Ｂｉｏｇｒａｐｈｙ：ＬｉＦｅｎｇｒｏｎｇ（１９６６－）ｆｅｍａｌｅ（ＨａｎＮａｔｉｏｎａｌｉｔｙ）ＳｃｈｏｏｌｏｆＩｎｆｏｒｍａｔｉｏｎａｎｄＣｏｍｍｕｎｉｃａｔｉｏｎＥｎｇｉｎｅｅｒｉｎｇＴｉａｎｊｉｎＰｏｌｙｔｅｃｈ－ｎｉｃＵｎｉｖｅｒｓｉｔｙａｄｊｕｎｃｔＰｒｏｆｅｓｓｏｒ，ｎｏｗｉｎｖｏｌｖｅｉｎｉｍａｇｅｐｒｏｃｅｓｓ－ｉｎｇｐａｔｔｅｒｎｒｅｃｏｇｎｉｔｉｏｎａｎｄＣｏｍｐｕｔｅｒＮｅｔｗｏｒｋ．

（３００１６０天津市天津工业大学信息与通信工程学院）李凤荣通讯地址：（３００１６０天津天津市河东区程林路６３号天津工业大学信息与通信工程学院）李凤荣

（收稿日期：２００７．７．０３）（修稿日期：２００７．９．０５）

（上接第８７页）

４结束语

模型检验是一种自动化验证方法，避免了建立复杂的证明过程，能够有效地对系统的安全性进行验证，一些公司如Ｉｎｔｅｌ、

ＩＢＭ、Ｍｏｔｏｒｏｌａ等已经在尝试把模型检验作为软件产品设计开

发过程的一部分。但是应该看到，模型检验在应用中仍不成熟，还存在不少问题有待解决：

（１）解决状态空间爆炸的方法相对于实际系统规模仍有差距；

（２）实时系统的模型检验方法还处于理论研究阶段，实用性不强；（３）模型检验工具要求使用者掌握特定的系统规范语言，使

用难度较大。

在下一步研究中，将进一步分析一些开放源代码系统的安全属性，用本文提出的方法进行形式化描述，利用模型检验技术对其隐含的不安全因素进行分析，同时对解决状态空间爆炸的方法作一些研究。

本文作者创新点：将在硬件设计领域得到成功应用的模型检验方法引入到软件产品的检验中，给出了一种基于自动机理论的检测软件安全的模型检验方法，并对其进行了验证。

项目经济效益１５万元。

参考文献：

［１］徐良华，

孙玉龙，高丰，朱鲁华，基于逆向工程的漏洞挖掘技术，微计算机信息，２００６，２５９－２６１［２］ＣｌａｒｋｅＥＭ，ＥｍｅｒｓｏｎＥＡ．Ｄｅｓｉｇｎａｎｄｓｙｎｔｈｅｓｉｓｏｆｓｙｎｃｈｒｏｎｉｚａｔｉｏｎｓｋｅｌｅｔｏｎｓｕｓｉｎｇｂｒａｎｃｈｉｎｇｔｉｍｅｔｅｍｐｏｒａｌｌｏｇｉｃ．ＬｏｇｉｃｏｆＰｒｏｇｒａｍｓ，Ｂｅｒｌｉｎ，１９８１

［３］ＬｉｎＨＭ．Ｍｏｄｅｌｃｈｅｃｋｉｎｇｖａｌｕｅ－ｐａｓｓｉｎｇｐｒｏｃｅｓｓｅｓ．Ｉｎ：Ｐｒｏｃｅｅｄｉｎｇｓｏｆｔｈｅ８ｔｈＡｓｉａ－ＰａｃｉｆｉｃＳｏｆｔｗａｒｅＥｎｇｉｎｅｅｒｉｎｇＣｏｎｆｅｒｅｎｃｅ．ＩＥＥＥＰｒｅｓｓ，２００１．

［４］ＨａｏＣｈｅｎ，ＤａｖｉｄＷａｇｎｅｒ，ＤｒｅｗＤｅａｎ．Ｓｅｔｕｉｄｄｅｍｙｓｔｉｆｉｅｄ．ＩｎＰｒｏｃ．ｏｆｔｈｅＥｌｅｖｅｎｔｈＵｎｉｘＳｅｃｕｒｉｔｙＳｙｍｐｏｓｉｕｍ，ＳａｎＦｒａｎｃｉｓｃｏ，ＣＡ，２００２．

作者简介：黄锦，男（１９８２－），硕士研究生，华中科技大学计算机学院，主要研究方向计算机网络应用与网络安全技术，Ｅｍａｉｌ：ｊｉｎｈｕａｎｇｈｕｓｔ＠ｇｍａｉｌ．ｃｏｍ；陈晓苏，男（１９５３－），教授，华中科技大

学计算机学院，研究方向计算机网络应用和网络安全技术；肖道举，男（１９５４－），副教授，华中科技大学计算机学院，主要研究方向计算机网络应用技术；刘辉宇，男（１９７８－），博士研究生，华中科技大学计算机学院，主要研究方向计算机网络应用与网络安全技术。

Ｂｉｏｇｒａｐｈｙ：ＨｕａｎｇＪｉｎ（１９８２－），ｍａｌｅ，ｂｏｒｎｉｎＪｉｎｇｚｈｏｕ，Ｈｕｂｅｉ，ｇｒａｄｕａｔｅｏｆｓｃｈｏｏｌｏｆｃｏｍｐｕｔｅｒｓｃｉｅｎｃｅａｎｄｔｅｃｈｎｏｌｏｇｙ，ＨｕａｚｈｏｎｇＵｎｉｖｅｒｓｉｔｙｏｆＳｃｉｅｎｃｅａｎｄＴｅｃｈｎｏｌｏｇｙ．Ｍａｊｏｒ：ｎｅｔｗｏｒｋｓｅｃｕｒｉｔｙ．Ｒｅｓｅａｒｃｈａｒｅａ：ｎｅｔｗｏｒｋａｐｐｌｉｃａｔｉｏｎａｎｄｎｅｔｗｏｒｋｓｅｃｕｒｉｔｙ．（４３００７４湖北华中科技大学计算机学院）黄锦陈晓苏

肖道举刘辉宇

通讯地址：（４３００７４湖北省武汉市珞瑜路１０３７号华中科技大学东１１舍３３２室）黄锦

（收稿日期：２００７．７．０３）（修稿日期：２００７．９．０５）

《现场总线技术应用２００例》

现场总线技术是现代工厂、商业设施、楼宇、公共设施运行、生产过程中的现场设备、仪表、执行机构与控制室的监测、控制装置及管理与控制系统之间的数字式、多点通信互连的，数据总线式智能底层控制网络。

现场总线技术保证了现代工厂、商业设施、智能楼宇、公共设

施（自来水、

污水处理、输变供电、燃气管道、自动抄表、交通管理等），高可靠、低成本、安全绿色生产运行，同时易于改变生产工艺，多品种生产过程。

本书２００个应用案例，介绍了ｐｒｏｆｉｂｕｓ、ＦＦ、ＣＡＮｂｕｓ、Ｄｅ－ｖｉｃｅＮＥＴ、ＷｏｒｌｄＦＩＰ、ＩＮＴＥＲｂｕｓ、ＣＣ－Ｌｉｎｋ、Ｌｏ－ｎＷｏｒｋｓ及ＯＰＣ、工业以太网、ＴＣＰ／ＩＰ在石油、化工、电力、冶金、铁路、制烟、造酒、制药、水泥、电力传动、机械、交通、设备管理、消防、自来水厂、电解铜、电解铝、继电保护、粮仓及储运、汽车检测、油库管理、造纸、气象、远程抄表、电缆生产、暖通空调、电梯、楼宇自动化及安防、……，各方面的应用。

本书是工程设计人员、设备维护人员、设备采购人员、技术领导干部、大、中专学校教员的案头参考书，同时也是大专院校本科生、研究生做课题、搞毕业设计的必备参考书。有志向有兴趣的高中以上文化水平的人均为本书读者。

本书已出版。大１６开，每册定价１１０元（含邮费）。

预购者请将书款及邮寄费通过邮局汇款至

地址：北京海淀区皂君庙１４号院鑫雅苑６号楼６０１室

微计算机信息编辑部邮编：１０００８１电话：０１０－６２１３２４３６０１０－６２１９２６１６（Ｔ／Ｆ）ｈｔｔｐ：／／ｗｗｗ．ａｕｔｏｃｏｎｔｒｏｌ．ｃｏｍ．ｃｎｈｔｔｐ：／／ｗｗｗ．ａｕｔｏｃｏｎｔｒｏｌ．ｃｎＥ－ｍａｉｌ：ｅｄｉｔｏｒ＠ａｕｔｏｃｏｎｔｒｏｌ．ｃｏｍ．ｃｎ；Ｅ－ｍａｉｌ：ｃｏｎｔｒｏｌ－２＠１６３．ｃｏｍ