Isabelle在分析安全操作系统状态机模型中的应用

为了解决已有的状态机模型的形式化框架在分析安全操作系统状态机模型时不够直观．简洁的问题，提出了一套使用Isabelle工具对安全操作系统模型状态中的类型、变量、常量、关系、映射、函数，以及模型中的安全不变量和状态迁移规 则进行形式化描述的新方法．通过实际验证一种典型的安全操作系统状态机模型——可信进程模型，总结出了有效地使用Isabelle辅助形式化设计、分析、验证模型的策略．

基于Isabelle定理证明器算法程序的形式化验证

形式化验证对保证软件的正确性和可靠性具有十分重要的意义.定理机械证明是形式化验证的一个重要研究领域,Isabelle系统是一个被广泛运用的定理证明辅助工具.本文在分析Dijkstra最弱前置谓词理论的基础上,根据PAR方法开发的算法程序循环不变式,提出了一种使用Isabelle定理证明器对算法程序进行机械验证的方法.该方法既克服了传统手工验证过程的繁琐性和易错性等缺点,又达到"提高验证效率和保证算法程序高可信"的目标,具有很好的实用价值.

一种改进的数据求精证明规则

提出一种改进的数据求精规则，并用关系模式进行描述。引入全局状态来描述程序所有可能的输入和输出，允许非平凡的初始化，允许前向模拟和后向模拟，能应用于消除具体模型的不确定性晚于消除抽象模型的不确定性的情况。并用实例说明了在Isabelle定理证明器中规则的应用方法。

Application of Dempster-Shafer evidence theory to unsupervised classification in multisource remote sensing

The aim of this paper is to show that Dempster-Shafer evidence theory may be successfully applied to unsupervised classification in multisource remote sensing. Dempster-Shafer formulation allows for consideration of unions of classes, and to represent both imprecision and uncertainty, through the definition of belief and plausibility functions. These two functions, derived from mass function, are generally chosen in a supervised way. In this paper, the authors describe an unsupervised method, based on the comparison of monosource classification results, to select the classes necessary for Dempster-Shafer evidence combination and to define their mass functions. Data fusion is then performed, discarding invalid clusters (e.g. corresponding to conflicting information) thank to an iterative process. Unsupervised multisource classification algorithm is applied to MAC-Europe'91 multisensor airborne campaign data collected over the Orgeval French site. Classification results using different combinations of sensors (TMS and AirSAR) or wavelengths (L- and C-bands) are compared. Performance of data fusion is evaluated in terms of identification of land cover types. The best results are obtained when all three data sets are used. Furthermore, some other combinations of data are tried, and their ability to discriminate between the different land cover types is quantified

新型网络环境中访问控制模型的研究

随着网格、P2P、无线通信网等技术的普及和飞速发展，访问控制技术取得了长足的进步，同时也面临着巨大的挑战。如何构建安全、灵活、可扩展的访问控制模型是这种新型网络环境下访问控制技术迫切需要解决的问题。本文围绕该环境中的访问控制需求，从委托模型、基于位置的访问控制模型、P2P环境下的动态信任评估模型以及访问控制模型的形式分析四个方面，对访问控制模型研究领域出现的若干关键技术展开研究，取得了以下四个方面的主要成果：第一，在分析Bertino等人提出的一个基于周期时间的访问控制模型的基础之上，指出它虽然可以清晰地表达访问权限可适用的时间范围，但模型本身并没有对已经具有权限的用户如何使用和传播权限强加任何限制，难以实施权限委托这一安全策略。针对这一缺陷，我们讨论了用户到用户的委托访问权限的限制，对权限委托的临时性、时序依赖性和受限传播性这些约束特性进行形式化建模，给出了基于周期时间的自主委托模型PDACDM的形式化定义及其一致性证明。第二，在分析前人所做的各种上下文研究工作的基础上，借助数学的形式语言，给出了一种依赖于空间上下文的访问控制模型SC-RBAC。该模型采用层次式的位置模型给空间客体建模，采用逻辑位置表达不同粒度的位置，引入了空间角色和有效会话角色等概念，证明了层次化的空间角色集合在数学上可构建格模型以实施多级安全策略和中国墙策略，提出了3类空间限制，借鉴和改进了RBAC本身的安全属性，提出了一些新的安全不变量，证明了模型的基本安全定理，并给出了一个简单的应用实例。这一研究成果为解决无线移动网络中的访问控制问题奠定了理论基础。第三，指出了设计一个P2P环境下的信任评估模型需要考虑的主要因素，如时间因素、系统稳定性等。着重分析了P2P环境下的信任模型在识别不诚实反馈、防止恶意节点的策略性动态改变行为、计算节点间相似度、激励机制等方面的不足。给出了一个基于时间窗的动态信任评估模型TWTrust，统一考虑了信任、信誉与激励三者的关系。通过仿真试验结果证明，该模型在信任计算误差和事务失败率等性能指标上有较大提高，能较好处理恶意节点策略性动态改变行为、不诚实反馈对系统的攻击和相似度计算中的稀疏性问题。这一信任模型的提出有望简化P2P下访问控制的实施。第四，在深入分析和对比目前可用于规范和验证访问控制模型的形式化方法和证明工具的基础之上，选取了证明能力强的Isabelle证明系统对支持空间上下文的SC-RBAC模型进行了形式分析，总结了用Isabelle语言对SC-RBAC模型属性和规则进行形式规范的方法，并且研究了基于Isabelle系统证明模型规范内部一致性和正确性的实用方法。

贵州赫章土法炼锌地区重金属对植物污染的初步研究

矿山开发造成的生态环境问题是一个世界性的问题，国内外许多学者对此表现出浓厚的兴趣。除矿山开发直接导致的植被破坏和耕地侵蚀等外，研究者更重视有害物质(特别是重金属)释放而导致的环境问题，特别是表生条件下矿山废弃物(矿山尾砂)的堆积，在一系列地球化学因素的作用下：如矿山尾砂的矿物成分 参考、堆积时间、厚度、气候条件及微生物（Rachel，2002）等发生风化作用，从而导致酸性矿山废水(AMD)的产生。蓄纳高浓度的重金属元素，其排放小仅对溪流、河流、湖泊水质及其沉积物产生负而影响，而且有降低土壤环境质量状况的威胁（Barbara Hohn，2005）。 贵州省赫章县是我国著名的土法炼锌集散地，地处贵州西北部，辖内煤炭资源丰富，境内的榨子厂、猫猫厂、天桥铅、锌矿(氧化矿)为“土法炼锌”提供了丰富的原料。其土法炼锌已有300多年的历史，至2000年，已有1000多个土法炼锌“马槽炉”的规模。炼锌中产生的黑色烟尘不仅使周围山坡寸草不生，山坡上、河道边到处倾倒着废渣，而且使许多早作地荒耕。本文试图以该地的土法炼锌为研究对象，探讨土法炼锌中产生的烟尘和废弃物对附近土壤和沉积物的环境影响。 1.1矿山开发中的生态环境影响 矿山的开采在很大程度上改变了矿山原有的环境。矿山开采耗费大量的土地资源，开采后破坏的土地，丧失原有的自然生态系统；废弃物堆置场是周围环境的严重污染源。矿山按其产品性质分类，有冶金矿山(黑色金属、有色金属、稀土元素、放射性元素等)和非金属矿山(煤矿、石料、陶土等)；按其开采方式分类，有露天开采矿山和地下开采矿山。不同性质的矿山和不同的开采方式，其对生态环境破坏的过程和特征有很大差异。 矿山开采引起的生态破坏，主要由以下三个过程导致：(1)开采活动对土地的直接破坏，如露天开采会直接毁坏地表土层和植被，地下开采会导致地层塌陷，从而引起土地和植被的破坏：(2)矿山开采过程中的废弃物(如尾矿、矸石等) 需要大面积的堆置场地，从而导致大量占用土地和对堆置场原有生态系统的破坏；(3)矿山废弃物中的毒性成分，可通过径流和大气飘尘，影响周围的土地、水域和大气质量（Ivanova，2001）。 在生态系统层次上，上述三个过程对采矿地区生态的破坏具有三个特征：(1)景观破坏，主要指对地貌的影响；(2)环境质量退化，对所在地区土质、水质，甚至大气质量的影响；(3)生物多样性退化，对原有生物群落的摧毁，及对当地现有生物群落的严重破坏甚至摧毁。 通常，金属矿山引起的环境质量退化以及由此导致的生物多样性退化要比非金属矿山更严重；露天开采的矿山引起的景观破坏和生物多样性退化，要比地下开采的矿山更严重。矿山开发的生态环境影响突出表现在以下几下方面： 1土地的占用与破坏 矿山开采后，将会产出大量的废石、排土和尾砂，例如露天开采1吨矿石通常削离5-10 t覆盖的岩土，堆存它们将需占用大量的土地。据报道美国的明尼苏达州北部，由于大型露天磁铁矿近半世纪的大量开采，致使当地土壤质地退化，如不进行有效的治理将有沙漠化的危险（Othman，1996）。矿区的建设也将不可避免地改变地形、自然景观和植被状况等。土地破坏的后果是：水土流失加剧，淤塞污染水体，增加扬尘，严重影响生态环境。另外，尾矿坝、废石堆场设置不当或管理不严，会造成严重的滑坡或泥石流事故，使大面积的土地受到破坏，造成水体污染，危及人身和财产的安全。 2水体污染 矿山开采后的废石堆成尾矿库若不妥善处理，可能会成为地下水污染源。废矿堆、尾矿库长期处在氧化、风蚀、溶滤过程中，其中的有毒矿物成份或有害物质可以随水转入地下、地表水体和农田、土壤之中，造成地下、地表水体受到化学污染。 采矿工业用水远远小于选矿工业的用水量，但不论是采矿还是选矿，若不注意处理其废水，会造成严重的后果。据报道，由于采矿对水体的污染，使美国长达20600km的水域和449个天然和人工湖泊不再适于养鱼（Antonio Simonetti，2000）；在国内也不乏其例，如攀枝花选矿厂（曾清如，1997）有部分尾矿废水排入金沙江，对其造成长期的严重污染。又如东鞍山矿（张宝贵，2002）由于外排废水中含有大量的细粒级悬浮物，使杨柳河的河水呈红色，不仅妨碍水生生物的生长，还影响农业灌溉，成为鞍山地区的一大公害。此外开采硫化矿床时，由于伴生的低品位黄铁矿，在自然堆放过程中，经风化、雨水浸蚀可产生有害酸性水。在我国冶金矿山中因酸性水污染造成的危害是十分严重的，如南山铁矿（许步信，1996）的酸性水波及周围1万hm2农田和渔业生产，多年来共赔偿农业损失费累计约百万元。此外，各金属矿山的外排水中浮悬药剂的污染、硝基苯的污染以及其它重金属的污染也屡见不鲜（Sastre，2002）。 井巷开掘、矿床排水疏干所形成的降压漏斗的水力影响半径有时可达数十公里，可能造成区域性水文环境的破坏，使农牧业缺水受损。另外，疏干碳酸盐围岩含水层之后，其岩溶和溶洞会成为地面塌陷下沉，地面设施被破坏的隐患；而当塌陷区或井巷地表贮水体存在水力的沟通时，则会酿成淹没矿井的重大事故；当岩层疏干影响的设计计划不周时，还可导致露天边坡、台阶的滑动和变形，从而出现相应的灾害后果（李小玉，2004） 3大气污染 在矿山生产中，氧化、风蚀作用可使废石堆场、尾矿库形成一个周期性的尘暴源。此外矿石破碎、筛分和选矿等工序也是主要尘源。矿山对大气的污染还包括公路运输过程中形成的大量扬尘。粉尘污染是冶金矿山生产过程中的一种主要污染类型。在我国，由于矿山粉尘污染而使矿区农牧业受害的情况较多。矿山开发引起的环境生态问题是全球性的问题，越来越受到科学界的关注，己成为环境地球化学研究的一个重要领域。随着对矿产资源需求的不断扩大，矿山废物的排放量大幅度增加，环境生态的恢复难度也在不断增大，因此，在科学界关注的同时，政府也要采取一定的措施来给予支持和提供方便（王文，2003）。 1.2矿区重金属污染研究 1.2.1重金属概念及环境化学行为 通常把密度大于5的金属称为重金属，如隔、铬、铜、镍、铅、锌等，砷虽然不属于金属，但由于对环境的影响与重金属类似，通常也称其为重金属。矿产开采过程中所引起的环境问题较多，特别是土壤的重金属污染（Ahmed，1998）。有害重金属通过各种途径进入土壤，不易随水淋溶，微生物难以降解，植物对其有明显的生物富集作用，影响农作物的品质和产量。土壤污染有较长的潜伏期，具有隐蔽性、不可逆性、普遍性、表聚性等特征（Isabelle，2001） 重金属是一类典型的环境污染物，在自然条件下，除了局部范围重金属含量较高之外，一般土壤中有害重金属含量都小于构成污染的临界值。由于受人类生产活动的影响，例如，农业增产措施如农药、化肥的不断使用，加之工业废水、废气、城市生活垃圾、污水及污泥与畜禽粪便等排入环境，都不断污染土壤，使重金属等在环境中的积累不断积聚。特别是最近几十年来，由于土壤环境中污染物含量不断提高，重金属污染问题已经引起学术界、政府和公众的广泛关注。 1.2.2环境中重金属的来源 重金属可以通过废水、废渣的排放，空气悬浮物的携带与运输，水体中的细微尾矿砂颗粒物的运移，食物链的传递等不同途径来引起环境的污染。污染源有以下几个方面： 工业污染源，尤其是基础工业，特别是采矿和冶炼业是向环境中释放重金属的主要污染源。如20世纪60年代，在日本的富山县神通川流域，由于铅锌冶炼厂排放的含锅废水污染水稻田，居民长期食用含偏稻米和饮用含锅水而造成锅中毒，锅进入人体后破坏人体的骨骼系统，使骨质变脆易折，也就是所谓的“骨痛病（Lorenzo，2000）。 生活污染源，主要是生活垃圾，其中含有的重金属能渗到土壤中，影响到地表水和地下水的质量，生活废水中的有机物可以吸收重金属，用这些水灌溉也可导致土壤污染。 农业污染源，主要来自厩肥、污泥、化肥、农药等，有害成分为其释放的重金属，污染物质主要集中于表层或耕层，它的分布比较广泛。污染物的种类和污染的轻重程度与土地的利用方式和耕作制度有关。 交通污染源，主要为含铅汽油的使用，使机动车排放的尾气污染大气。 自然污染源，土壤母质中的重金属本身含量高，还有火山喷发造成的土壤污染。 就矿区来说，以工业污染源为主，其它次之。 1.2.3环境中重金属的危害 尾矿、矿渣是采矿区土壤重金属的主要来源之一。当这些矿山固体垃圾从地下搬运到地表后，由于所处环境的改变，在自然条件下，极易发生风化作用(物理、化学和生物作用)，使大量有毒有害的重金属元素释放出来进入到土壤和水体中，给采矿区及周围环境带来严重的污染。 在雨水等的作用下，地下水和地表水都会受到不同程度的重金属污染。目前世界上受高砷饮水危害的国家和地区包括孟加拉国、印度恒河流域、阿根廷、智利、墨西哥、泰国、美国和中国的台湾、内蒙、山西部分地区。孟加拉国受砷危害人口有35-77百万人，占该国总人口(125百万)的一大半，几十年来联合国投入了大量财力物力进行治理，但收效甚微（Kovalchuk，1996）。有300多年开采历史的我国湖南石门雄黄矿，发生了严重的砷污染，河水砷含量达0.5－14.5 mg•L－1，居民头发砷含量为0.972-2.459ug•L-1。以河水为饮用水源的居民的砷暴露水平达到甚至超过国内外重大慢性砷中毒案例的暴露水平。 有毒气体的排放无疑会直接污染大气。如1996年玻利维亚波托西的波尔科矿山的一座铅锌尾矿坝倒塌，致使大约235，000 t有毒尾矿泥浆(包括砷、氰化物、铅和锌等有害成分)排入皮科马约河的一条支流阿瓜卡斯蒂利亚河中，导致饮用该河水和食用该河水中鱼的3名儿童死亡，其毒性影响到800km的巴拉圭一阿根廷的查科(salomons，1995)。另外，巴西亚马逊河流域附近，约17000km，的大范围金矿开采过程中，汞作为重要提金试剂，易形成合金金齐汞，直接释放进入大气，且向大气的释放量远比向河流和土壤的释放量高，占总释放量的65%-83%( salomons，1995)，对人体危害十分严重。西班牙某重金属冶炼厂尾砂坝的倒塌，使得随后的土地开发过程中大气可吸入颗粒中铜和锰的含量增加了17~36％和59一70％（Querol，2000）。 重金属在土壤中的聚集引起的危害更为严重。其进入土壤后，一方面可在植物体中累积，并通过食物链最终转移到人体内，危害人群健康，致畸致癌；另一方面，还可能导致地下水污染，超过一定限度就会危害生态系统，如上述所说的水体和大气的污染。由于重金属污染的范围广，持续时间长，又不易在生物物质循环和能量交换中分解，所以污染土壤的修复与治理迫在眉睫，也是科学界比较关注的问题之一。就世界范围来看，全世界每年平均排放汞115万t，锰1500万t，铜340万t，铅500万t，镍100万（Jane vacalet，1999）。据估计，我国仅重金属污染的耕地面积就达2000万ha，约占耕地总面积的115 ，每年因土壤污染而减产粮食1000万t；另外还有1200万t粮食重金属超标，二者的直接经济损失达200多亿元（陈同斌，1999）。在金属成矿区周围的自然扩散区域内，环境中一般含有较高浓度的重金属，加上开矿过程中的废矿水和尾矿砂，常造成严重的重金属污染问题。据报道，湖南省郴县东坡铅锌矿自然扩散晕区域内的环境污染是以铅、锌、镉、砷为主的多金属污染复合体，水体内的细微尾矿砂颗粒物是重金属的主要迁移载体，且该区域内作物中的铅、镉残留很高（曾清如，1994）。 土壤中重金属的超标同时也会使农作物和其它生物受到危害。杨居荣（1992）发现耐福的甜菜与胡萝卜在对营养元素的吸收上呈现两种不同的特征，即耐镐的甜菜往往对钙、镁、锌、铁元素的吸收量大，而胡萝卜则相反。土壤中锌/锅比例增大可显著地降低菠菜含镉量（宋菲，1996）。己有证据表明，铜矿的冶炼可以增加周围农业系统中的铜含量，使冶炼厂周围紫花首稽和柏树叶片中的铜含量明显增加。华南某矿区周围农田土壤中锌含量达690~4000 mg.kg－1；华北某污灌区土壤中锌含量超过1500 mg•kg－1，长期施用污泥的土壤中锌含量达370－470 mg•kg－1，受汞污染的面积达3.2 × 104 ha，每年生产汞米1.95×105吨。沈阳张士灌区和江西大余县等地区的粮食己经遭受严重的锡污染，其含镉量己经超过诱发“痛痛病”的标准。龙育堂等（1994）研究芝麻对稻田汞净化效果，结果表明：土壤含汞量在5－130 mg•kg－1，范围内，汞对芝麻产量和品质仍未造成显著影响；改种芝麻，土壤汞的年净化率高达41%，土壤的自净恢复年限比种植水稻缩短。食物链中重金属的高度富集最终将威胁到人类健康。