安全是现代软件系统不可缺少的一部分,但目前的软件系统建模时很少涉及安全,系统安全策略和安全机制往往作为开发人员在系统开发后期对系统的补充和完善的措施。这种不规范的安全需求处理方法为系统后期安全维护及系统之间的集成带来莫大隐患。如果在系统开发的早期阶段就考虑安全需求,可以发现潜在的安全问题,及早地消除系统安全隐患。人们曾通过研究形式化方法与证明来保障早期安全机制设计的安全性,但是完全证明一个系统的安全性是不现实的,而且由于软件开发者并不希望为此专门学习形式化方法,原因是缺乏足够的时间和训练。所以人们希望使用那些在业界软件开发中逐渐形成的经典方法:它不仅很容易学会和使用,而且可以在开发的每一个阶段,从需求到设计、实现、测试和部署都能考虑安全。由Jan Jürjens所著的这本书就是这样一本好书。
本书通过采用已经广泛适用的、通用的、标准统一建模语言UML,将安全特性很自然地融入整个系统设计过程之中,扩展为UMLsec方法。UMLsec提供一种不同于传统“渗透测试和打补丁”或“形式化规范和验证”的方法,它采用可视化的UML建模语言,从不同的视角描述系统的不同侧面,并通过一些扩展语义的UML规范、求精、验证过程,使得即使不是安全专家的开发人员也可以把安全集成到软件工程过程的每一个阶段。全书系统和详细地阐述了UMLsec的方法和语义,并且提供了说明方法有效性的实例分析,以及支持UMLsec的验证工具及其开发方法等,是学习、研究和实践安全软件工程方法的一本好书。
纵览全书,不难发现,本书汇集了作者大量的研究成果和教学成果,它既是一部优秀的专著,也是一部很好的教材。本书涵盖了作者与德国银行、汽车制造商、电信公司等多家企业合作项目的成果,以及他在牛津大学和慕尼黑工业大学的教学成果。
参与本书翻译和校对的是沈晴霓博士和季庆光博士。本书的翻译工作自始至终都得到了中科院软件所研究员、北京大学软件与微电子学院信息安全系主任、国内外信息安全专家卿斯汉教授的大力支持,并且卿老师在百忙之中帮助审校了译稿,特此致谢。同时,在本书初稿的翻译过程中,硕士生李岩、阮安邦、翟恩南、张亚航、韩啸等同学做了许多有益的工作,在此也向他们表示感谢。
由于译者水平和学识有限,加上时间仓促,翻译中难免有错误和不妥之处,敬请广大读者批评指正。UML安全系统开发FOREWORD前 言 那些投身于开发、部署或评价新的IT系统的人们,可能认为这些过程中出现的安全问题都是技术发展直接导致的。其实并非完全如此。新技术能为新的应用创造机会,但有时很难预测该技术在什么时候开始得到应用。例如电子邮件,当前Internet及其早期形态上第一个主要的应用,最初只用于“严肃”的学术合作;再比如SMS(短消息服务),一个成功的应用,最初也只被看成第二代移动电信系统额外增加的一个很小的服务。
此外,新的技术和新的应用也促使和提供了制造各种各样恶作剧的机会,于是产生了“安全技术”需求,以阻止(至少减少)对那些新应用不受欢迎的使用。仍以电子邮件为例,目前垃圾邮件已经成为一大危害,所以成功抵制垃圾邮件是提供正常电子邮件服务所必需的。
对于软件系统,在20世纪90年代初期,对社会公众开放商用Internet是一件意义深远的事情,它的影响至今仍然无法估量。它首先引发人们对封闭式环境中分布式应用的开发,封闭式环境将Internet作为一个开放通信网络。在这个领域,安全需求主要(但不完全)与通信安全相关,虚拟专用网(VPN)就是一个很好的例子。但是,我们也需要处理无控制/授权中心的开放环境,这就需要一些可获得安全性的新方法。事实上,不同的应用要满足不同的安全需求,这也是安全协议设计困难并容易产生错误的主要原因之一。
以上这些都让我们开始考虑安全性。安全专家们通常强调“安全不能只被看成一种新增特性,系统也不能只在设计后期考虑添加一些所谓的安全特性来达到安全性”。在一定程度上,安全需求与应用相关,所以应用设计者的任务是在早期规范中考虑包括这些需求,而设计过程的任务是要确保实现了恰当的保护机制。因此对设计方法就有了一个明确的要求:帮助规范安全需求和确保实现了恰当的安全机制。
在安全性方面还有一种普遍看法,即针对安全挑战,很难有正确的答案,只有相对较好的或较差的答案。在提出安全设计方法时,如果让没有安全意识的应用程序作者去决定安全性问题,那么我们就相当于在走钢丝。在安全需求很好理解并能通过一套标准化的安全机制来满足的应用领域,我们有理由相信这些方法会得到很好的应用。但是,在一些应用中(尤其是一些比较新的应用中),我们并不总是能够预知其安全需求,而且严格的工程实践过程也会变化。例如,抵抗拒绝服务攻击的鲁棒性和身份的保护(抗抵赖性),近年来已经成为密钥建立协议设计的一些新属性,正如关于网络密钥交换协议(IKE)后续版本的讨论。
本书为建立良好的安全工程设计方法做出了有价值的贡献。通过建立于一种被广泛采纳的、像UML这样的规范语言之上,使对安全方面的考虑能够以一种非常自然的方式适用于设计过程。本书提出的方法具有坚实的理论基础,能够采用一种精确的设置来验证一个设计是否具有其期望的安全属性。这些基础性的定义本身就构成了本书工作的一部分,但本书的工作远不止这些。常言道:“布丁味道怎么样,吃了才知道!”对于任何想获得实际影响力的设计方法来说,事实胜于雄辩。本书在这个方面也进行了详尽的讨论,其中就包括几个已应用了本方法学的实例研究,并且介绍了为支持这种方法而开发的一些工具。
UML安全系统开发如果认为这本书只是迈向一个很有前景方向的第一步,那么就严重低估了这本书的成就。读者朋友们完全可以把这本书作为一个典范,因为它展示了如何使应用软件设计者接受安全系统设计的形式化方法,读者必将看到它随着方法的成熟而得到进一步发展。
Hamburg, Dieter GollmannFOREWORD序 在现代社会和现代经济中,为通信、金融、能源分布和交通运输服务的计算机网络面临着攻击,这些攻击严重地威胁到人们和组织机构的经济和物质利益。由于急剧增长的系统互连,这些攻击可以从一个安全的距离、匿名地发起,所以要保证网络化计算机的安全。
高质量地开发安全关键系统是很困难的。有许多系统被开发、部署和使用,但是它们并不能满足各自的关键性需求,有时还会导致很严重的攻击。
开发安全系统上的部分困难常常来自正确性目标与低开销目标的冲突。完善而严密的系统设计方法往往带来人员培训和使用上的高开销,这些其实都是可以避免的。
统一建模语言(UML)为开发高质量的、低成本和耗时少的安全系统提供了很好的机会。
作为实际行业建模标准,很多开发者在UML方面接受过正规培训。
与先前一些具有一定用户规模的标记语言相比,UML的定义比较精确。
现在已经有多种工具提供了使用UML所需的基本功能(如画UML图的工具).
但为了利用好这个机会,我们也面临着一些挑战:其一,人们需要改写UML,使其适合安全关键系统的应用领域,并推动在这个应用领域内正确使用UML;其二,人们必须开发一些先进的工具,以支持用UML开发安全系统,比如依据安全需求对UML规范进行自动化分析,这就要求解决UML模型语义的灵活性和非二义性之间的矛盾。本书的目标就是克服这些困难。
我们提出了支持开发安全系统的UML扩展--UMLsec,它使用了标准的UML扩展机制。高层抽象的可能性以及对一个系统不同角度形成的各种图,可以对系统上下文中的安全关键组件建模。这样,人们就可以自动化评估UML规范的脆弱性,只要有基于我们提供的UML1.5简化版形式化语义的UMLsec工具支持。人们也可以封装严格安全工程建立的规则,让开发者可以使用。因此,本方法目标在于对安全专家和可能不是安全方面专家的开发者都有帮助。我们会通过一些实例来说明UMLsec的使用。例如,我们开发了一个安全通道规范,并发现了一个已公布Internet协议TLS的变体和通用电子钱包规范中的缺陷,并提出了修正意见、进行了验证。我们在银行应用环境中和Java安全环境中使用了UMLsec。我们提出了构造工具支持所需的概念和技术,用于分析满足复杂需求的UML模型,比如UMLsec规范中的约束。这种工具支持基于一种XML变体(XMI), XMI允许UML模型之间进行交互。
本书的基础是一篇博士论文、一部分受邀报告和暑期学校课程、一系列(约三十份)国际会议演讲和来自会议参与者的反馈,也包括在国际期刊和国际会议上发表的约三十篇文章,与行业伙伴(包括一个德国银行、汽车制造商和电信公司)合作的项目反馈,以“UML基于模型的安全工程” 为主题的国际研讨会上的探论,指导的约三十位硕士和学士的论文,以及由牛津大学、慕尼黑工业大学提供的相关主题高级研究项目和7门课程,其中包括了本书的部分主题。与本书相关的其他资料都在网站\上给出(将不断更新),包括以下资料:
部分来自上述课程和演讲的幻灯片和录音。
其他的学习和教学资料,包括练习和答案。
模型分析工具的Web接口,它对用行业UML建模工具写成的UMLsec模型(可以通过Internet上载)进行安全需求分析。
需要说明的是,尽管本书提及的UML扩展目标也包括为不太熟悉安全的开发者提供帮助(例如,通过一种安全的方式,使他们能够使用安全机制),但是本书的部分内容涉及高级应用(如密码协议分析),此时具备安全方面的背景知识将会有所帮助。
UML安全系统开发序在此,我要对所有参与本书编写工作的人们表达我最真诚的谢意。包括: Samson Abramsky,我博士论文的导师,感谢他的远见卓识、建议、鼓励和耐心;Manfred Broy,慕尼黑工业大学软件与系统工程组的领导,感谢与他有趣的讨论、在形式化方法和软件工程方面共享他丰富的经验,以及他为大家提供的非常有创造力的工作环境;鼓励我完成本书的合著者和同事,感谢能与他们进行卓有成效的合作,以及与他们在安全或UML方面启发式的讨论;感谢我的学生们在工具支持上与我的有益合作,以及对本书提出的质疑;阅读了本书草稿各节并提出有益评论和建议的人们;与本书相关的学术论文的评审人员;本书讲解时的几百位学习者,安全或UML相关演讲时的听众,他们也提出了有益的评论和问题。在此,还要感谢我参加的各组织的成员,包括德国信息学会(GI)下属的安全形式化方法与软件工程工作组FoMSESS、GI的安全分部、巴伐利亚安全技术中心、巴伐利亚地方政府电子安全工作组,以及IFIP工作组1.7“安全性分析与设计理论基础”,我与他们在安全方面进行了有趣的讨论;还有来自慕尼黑工业大学的技术支持,包括系统管理员和学生助理,特别是Britta Liebscher。我还要特别感谢Spinger-Verlag的编辑Ralf Gerstner先生,感谢他对本书的极大兴趣,以及他的耐心和理解。同时,向那些我一时想不起名字的人们道歉,下面是我记得的感谢名单:Martín Abadi、Lionel Van Aertryck、Ewgeny Alter、Axelle Apvrille、David Basin、Peter Braun、Matthias Braun、Ruth Breu、Alexander Chatzigeorgiou、Dominique Chauveau、Pierpaolo Degano、Martin Deubler、Rik Eshuis、Andreas Fedrizzi、Eduardo B.Fernandez、Rober France、Onno Garms、Geri Georg、Andreas Gilg、Dieter Gollmann、Roberto Gorrieri、Susanne Graf、Johannes Grünbauer、Joshua Guttman、Sebastian Hohn、Helia Hollmann、Siv Hilde Houmb、Anna Ioshpe、Gergely Kokavecz、Dimitri Kopjev、Thomas Kuhn、Simon Kulla、Markus Lehrhuber、Britta Liebscher、Wolfgang Linsmeier、Volkmar Lotz、Gavin Lowe、Frank Marschall、Shasha Meng、Carlo Montangero、Haris Mouratidis、Gerhard Popp、Max Raith、Jan Romberg、Bernhard Rumpe、Rober Sandner、Rober Schmidt、Marillyn Schwaiger、Stephan Schwarzmüller、Bran Selic、Pasha Shabalin、Shunwei Shen、Oscar Slotosch、Perdita Stevens、Martin Strecker、Guido Wimmel和Bo Zhang。最后,我要特别感谢我的父母和兄弟,他们一直以来给予了我精神上的大力支持。
这项工作得到了多方资助,包括德国人民奖学金、计算机科学基础实验室(爱丁堡大学)、贝尔实验室(朗讯科技)、计算实验室(牛津大学)、软件与系统工程系(慕尼黑工业大学)、FairPay项目(德国财政部)、HypoVereins银行(慕尼黑)和Verisoft项目(德国教育与研究部)等。在此,特别感谢以上单位的支持。
欢迎你提出与本书内容相关的意见和问题,也可以通过本书的网站\和我们交流。
München, Jan Jürjens