0HAL Id: tel-015472860https://theses.hal.science/tel-015472860提交日期：2017年6月26日0HAL是一个多学科开放存取档案，用于存储和传播科学研究文档，无论其是否发表。这些文档可以来自法国或国外的教育和研究机构，也可以来自公共或私人研究中心。0HAL多学科开放存取档案，旨在存储和传播法国或国外教育和研究机构、公共或私人实验室发表或未发表的研究文档。0自动推理Web应用程序和协议模型以检测漏洞0Karim Hossen0引用此版本：0Karim Hossen. 自动推理Web应用程序和协议模型以检测漏洞. Cryptographie et sécurité [cs.CR].Grenoble大学, 2014. 法语. �NNT : 2014GRENM077�. �tel-01547286�0THESIS0为了获得学位0格勒诺布尔大学博士学位 专业：计算机科学0法国教育部法令：2006年8月7日0KarimHossen提交0由Roland Groz教授指导，CatherineOriat博士共同指导的论文0在格勒诺布尔计算机和数学信息科学实验室和信息技术、信息学（MSTII）中准备0自动推理Web应用程序和协议模型以检测漏洞0于2014年12月15日公开支持，评审委员会成员如下：0Marie-Laure Potet女士，Grenoble INP教授，主席 Yves LeTraon教授，卢森堡大学，评审员 Jean-ChristopheJanodet教授，Evry大学，评审员 FrédéricDadeau副教授，Franche-Comté大学，FEMTO-ST研究所，考官 KeqinLi博士，SAP Labs，邀请 Roland Groz教授，Grenoble INP，博士导师Catherine Oriat副教授，Grenoble INP，博士共同导师0致谢0在我的博士期间，我有机会与许多人一起工作，他们帮助我完成了这项工作，我想对他们表示感谢。0我的导师Roland Groz，我的共同导师Catherine Oriat和Jean-LucRichier，他们都是VASCO团队的成员，在这几年里无论是在我的课题还是在各种演讲和会议上都给予了我指导。Naeem Irfan和Mohammed AmineLabiadh是有趣而友好的办公室同事。0感谢Keqin Li和AlexandrePetrenko给我参与他们的工作的机会。我还参与了SPaCIoS项目的工作，在那里，即使我是最后加入的，我也受到了特别好的接待，这使我在英语方面取得了进步，而这之前并不是我的强项。0SPaCIoS项目的所有成员，特别是Luca Vigano，他成功地管理了我们的项目，MariusMinea和Petru Florin Mihancea在推理方面进行了合作，Johan Oudinet和MatthiasBuechler在漏洞检测方面进行了合作，Gabriele Costa在Eclipse中帮助集成工具。0感谢Akram Idani、Roland Groz、Florent Autreau和Marie LaurePotet在我的博士期间允许我进行教学和实验。0Marie Laure Potet和LaurentMounier在我完成博士学位期间接待我，并允许我在Bin-Sec项目中工作。0感谢Ensimag安全俱乐部的各位成员，在我没有时间的时候为俱乐部做出贡献。特别感谢François Desplanques、Josselin Feist和GuillaumeJeanne为俱乐部的管理工作所做的努力。0Web应用程序和协议的模型推理，用于自动漏洞检测0摘要：基于模型的测试（MBT）方法已经证明了它们在软件测试领域的有效性，但是它们需要事先拥有软件的正式模型。在大多数情况下，由于成本、时间或权利等原因，这个模型是不可用的。在SPaCIoS项目中，旨在开发一个基于模型的安全测试平台，我们的目标是为Web应用程序提供自动推理模型的工具，并基于该模型提供漏洞检测方法。0我们开发了一种适用于Web应用程序及其特性的推理算法。该方法考虑了数据及其对控制流的影响。通过数据挖掘算法，模型被补充了保护和输出函数。我们还致力于推理过程的自动化。在主动推理方法中，通常需要了解要推理的系统的完整接口以便与应用程序进行通信。通过使用针对推理进行优化的爬虫和接口提取方法，这一步骤已经自动化。这个爬虫也可以被第三方推理工具使用。0在完整的算法中，我们将推理算法和接口提取合并，以构建一个自动化的过程。我们介绍了包含这些不同算法以及在SPaCIoS项目案例研究和协议中获得的各种结果的免费软件SIMPA。0关键词：模型推理，安全测试，逆向工程，Web应用程序，协议0Web应用程序和协议的模型推理，用于自动漏洞检测0摘要：在过去的十年中，基于模型的测试（MBT）方法在软件测试领域显示出了其效率，但是需要系统测试（SUT）的正式模型，而这个模型大多数情况下是不可用的，原因有成本、时间或权利等。SPaCIoS项目的目标是使用MBT方法开发一个安全测试工具。本工作的目标是开发和实现一种适用于Web应用程序和协议的模型推理方法。从推理出的模型中，可以使用SPaCIoS的模型检查方法进行漏洞检测，或者使用我们开发的方法进行检测。0我们开发了一种适用于Web应用程序及其属性的推理算法。该方法考虑了应用程序数据及其对控制流的影响。使用数据挖掘算法，推理模型通过优化的保护和输出函数进行了细化。我们还致力于推理过程的自动化。在主动学习方法中，需要了解系统的完整接口以便与其通信。由于这一步骤可能耗时，我们使用了针对推理进行优化的爬虫和接口提取方法，使这一步骤自动化。这个爬虫也可以作为独立的第三方推理工具使用。0在完整的推理算法中，我们将推理算法和接口提取合并，构建了一个自动化的过程。我们介绍了包含这些算法的免费软件SIMPA，并展示了在SPaCIoS项目案例研究和协议上获得的一些结果。0关键词：模型推断，安全测试，逆向工程，Web应用程序，协议0目录01 引言 101.1 背景 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101.1.1 SPaCIoS项目 . . . . . . . . . . . . . . . . . . . . . . . 201.1.2 模型推断 . . . . . . . . . . . . . . . . . . . . . . . 301.1.3 Web漏洞 . . . . . . . . . . . . . . . . . . . . . . . 401.2 问题 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 501.2.1 什么类型的模型？ . . . . . . . . . . . . . . . . . . . . . 501.2.2 自动方法 . . . . . . . . . . . . . . . . . . . . . . . 701.2.3 适应的推断算法 . . . . . . . . . . . . . . . . . 801.3 贡献 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 801.4 论文结构 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 902 Web安全和模型推断 1102.1 Web应用程序的安全性 . . . . . . . . . . . . . . . . . . . . . . . 1102.1.1 Web应用程序的运行方式 . . . . . . . . . . . . . 1202.1.2 安全问题 . . . . . . . . . . . . . . . . . . . . . . . 1602.2 模型推断和安全 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2202.2.1 白盒推断和被动推断 . . . . . . . . . . . . . . . . 2402.2.2 黑盒主动推断 . . . . . . . . . . . . . . . . . . . 2803 推断有限状态机 3503.1 具有变量和非确定性参数的自动机推断 3503.1.1 通过学习进行测试 . . . . . . . . . . . . . . . . . . . . . . 3603.1.2 扩展有限状态机 . . . . . . . . . . . . . . . . . . . 3703.1.3 用于EFSM的推断方法 . . . . . . . . . . . . . . . . 4003.1.4 实验 . . . . . . . . . . . . . . . . . . . . . . . . . 4603.1.5 优点和缺点 . . . . . . . . . . . . . . . . . . . 4903.2 Z-商推断 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5003.2.1 Z-商 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5003.2.2 初始Z-商 . . . . . . . . . . . . . . . . . . . . . . . . . 5203.2.3 用于FSM的Z-商推断方法 . . . . . . . . 5503.2.4 处理反例 . . . . . . . . . . . . . . . . . . . . . . . . . . . 6003.2.5 实验 . . . . . . . . . . . . . . . . . . . . . . . . . 6203.2.6 优点和缺点 . . . . . . . . . . . . . . . . . . . 6304 创建测试适配器 6504.2 手动编写测试适配器 . . . . . . . . . . . . . . . . . 6704.2.1 对于SIP协议（非基于HTTP） . . . . . . . . . . . . . . . . 6704.2.2 对于Web应用程序（基于HTTP） . . . . . . . . . . . . . 710vi 目录04.3 自动化生成Web应用程序的测试适配器 8004.3.1 提取参数化输入 . . . . . . . . . . . . . . . . . . . . 8004.3.2 提取输出 . . . . . . . . . . . . . . . . . . . . . . 8204.3.3 提取输出参数 . . . . . . . . . . . . . . . . . . . . . 8404.3.4 应用程序遍历 . . . . . . . . . . . . . . . . . . . . . 8504.3.5 推理优化 . . . . . . . . . . . . . . . . . . . 8604.4 测试适配器生成 . . . . . . . . . . . . . . . . . . . . . . . . . . . 8705 扩展的Web应用程序自动机推理 8905.1 动机 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9005.2 带参数的EFSM模型 . . . . . . . . . . . . . . . . . . . . . . . . . 9105.3 扩展的Z-Quotient . . . . . . . . . . . . . . . . . . . . . . . . . 9405.4 扩展的Z-Quotient推理 . . . . . . . . . . . . . . . . . . . . . . . . 9605.4.1 扩展观察树 . . . . . . . . . . . . . . . . . . . . 9605.4.2 通用推理过程 . . . . . . . . . . . . . . . . . . . . . . . . . 9705.4.3 参数使用策略 . . . . . . . . . . . . . . . . . . . . . 9805.4.4 扩展观察树 . . . . . . . . . . . . . . . . . . . . 9905.4.5 随机数的检测和重用 . . . . . . . . . . . . . . . 10205.5 推理守卫和输出函数 . . . . . . . . . . . . . . . . . . . . . . . . 102 5.5.1 原始数据 . . . . . . . . .. . . . . . . . . . . . . . . 10305.5.2 修改版的ID3 . . . . . . . . . . . . . . . . . . . 10305.6 实验 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10705.7 限制 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11206 Web漏洞检测 11506.1 未经授权的行为检测 . . . . . . . . . . . . . . . . . . . 11606.1.1 简化推理模型 . . . . . . . . . . . . . . . . . . . . . . . 11606.1.2 输入图 . . . . . . . . . . . . . . . . . . . . . . . . 11706.1.3 漏洞检测 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11806.2 XSS（跨站脚本攻击） . . . . . . . . . . . . . . . . . . . . . . . . 120 6.2.1 部分过滤和反射 . .. . . . . . . . . . . . . . . . 12106.2.2 代码注入集合的缩减 . . . . . . . . . . . . . . . . . . . 12306.3 CSRF（跨站请求伪造） . . . . . . . . . . . . . . . . . . 12306.3.1 检测输入中的随机参数 . . . . . . . . . . . . . . . . . . . . 12306.4 路径搜索 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12606.5 SPaCIoS模型检测方法 . . . . . . . . . . . . . . . . . . . 12707 工具和实验 12907.1 SIMPA：一个自动机推理平台 . . . . . . . . . . . . . . . . . . . 129 7.1.1 推理算法 . . . . . .. . . . . . . . . . . . . . . . 13007.1.2 测试适配器 . . . . . . . . . . . . . . . . . . . . . . . 13107.1.3 不同的系统 . . . . . . . . . . . . . . . . . . . . . . . 13107.1.4 日志系统 . . . . . . . . . . . . . . . . . . . . . . . . . . . 13307.2 集成 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1330目录 vii07.2.1 作为Eclipse插件集成 . . . . . . . . . . . . . . . 13307.2.2 NESSoS集成 . . . . . . . . . . . . . . . . . . . . 13407.3 案例研究 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13407.3.1 WebGoat应用程序 . . . . . . . . . . . . . . . . . . . . 13507.3.2 SIP（会话初始化协议） . . . . . . . . . . . . . . . . 14308 结论... 14708.1 摘要... 14708.2 与论文相关的出版物... 14808.3 展望... 150 8.3.1 覆盖率和非回归... 15108.3.2 收集器策略... 15108.3.3 参数的详细建模... 15108.3.4 生成协议测试适配器... 15208.3.5 应用于二进制文件的推理... 1520参考文献... 1530发现的XSS漏洞... 1650A.1 Roland-Garros... 1650A.2 Ensimag... 166 A.3 adopteunmec.com... 167 A.4 IAE Grenoble... 168 A.5QueChoisir.org... 169 A.6 Direct-assurance... 1690A.7 Centerblog.net... 1700图表目录...01.1 SPaCIoS工具架构... 302.1 动态网站... 1202.2 Cookie管理... 1402.3 Web事件统计（WHID）... 1602.4 使用反射型XSS的攻击... 1802.5 使用持久型XSS的攻击... 1902.6 客户端执行的脚本... 2002.7 CSRF攻击... 2102.8 资源抽象步骤... 2602.9 分离不同操作的步骤... 2702.10 主动学习方法... 2802.11 使用Σ = a, b的观察表示例... 2902.12 使用I = { a, b }和O = { x, y }的Lm*观察表示例... 3102.13 [Cho 2010]推理平台架构... 3203.1 代表SAML的EFSM示例... 3903.2 SAML SP的控制表和数据表摘录... 4203.3 根据状态数量的请求数量复杂度... 4703.4 根据输入符号数量的请求数量复杂度... 4803.5 根据简单和变量保护的百分比的请求数量复杂度... 4803.6 FSM A... 5403.7 { a, b } - FSM A的初始商... 5403.8 观察树U... 5803.9 使用反例更新的观察树 U。03.11 使用LM � 算法的平均请求比较。04.1 测试适配器。04.2 使用SIP进行通信的步骤。04.3 SAML的工作原理图。04.4 SimpleSAMLphp的身份验证页面。04.5 PageTree示例。04.6 对应于PageTree的页面。04.7 用于定位参数的同一页面的两个版本。05.1 扩展的Z-Quotient算法示意图。05.2 决策树示例。0x 图表目录05.3 扩展观察树的根节点。05.4 应用的登录页面。05.5 员工列表。05.6 使用 I = [LOGIN] 的扩展观察树。05.7 使用 I = [LOGIN, VIEW, CREATE, DELETE, SEARCH, LOGOUT] 的扩展观察树。05.8 使用 I = [LOGIN, VIEW, CREATE, DELETE, SEARCH, LOGOUT] 和 Z = [VIEW]的扩展观察树。05.9 WebGoat Stored XSS课程的推断EFSM模型。06.1 WebGoat应用模型示例。06.2 WebGoat应用输入图的示例。06.3 WebGoat应用的彩色输入图。06.4 在SPaCIoS方法中使用推断模型。07.1 SIMPA的整体架构。07.2 Eclipse中的SIMPA菜单。07.3 在SIMPA中创建适配器。07.4 SIMPA项目的目录结构。07.5 NESSoS中的SDE SIMPA组件。07.6 NESSoS中的SIMPA调色板。07.7 Stored XSS应用的主页。07.8 WebGoat应用的推断模型。07.9 绕过数据层的推断模型。07.10 绕过业务层的推断模型。7.11 iptel.org的推断SIP协议。07.12 SIP2SIP的推断SIP协议。0A.1 rolandgarros.com上的XSS。A.2 Ensimag网站上的XSS。A.3adopteunmec.com网站上的XSS。A.4 IAE Grenoble网站上的XSS。A.5QueChoisir网站上的XSS。A.6 direct-assurance网站上的XSS。A.7Centerblog.net网站上的XSS。0表格列表04.1 SIP不同请求列表 . . . . . . . . . . . . . . . . . . . . 6904.2 SIP不同响应列表 . . . . . . . . . . . . . . . . . . . . 6906.1 CSRF令牌格式表格 . . . . . . . . . . . . . . . . . . 1250第1章 引言0本章介绍了本论文的背景，首先是资助后续章节工作的SPaCIoS项目，然后是对需要新的Web应用程序安全测试方法的原因进行了描述，包括服务互联网（IoS）和与Web安全相关的问题。最后，我们介绍了各种贡献以及论文的结构。0目录01.1 背景 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101.1.1 SPaCIoS项目 . . . . . . . . . . . . . . . . . . . . . . . 201.1.2 模型推理 . . . . . . . . . . . . . . . . . . . . . . . 301.1.3 Web漏洞 . . . . . . . . . . . . . . . . . . . . . . 401.2 问题 . . . . . . . . . . . . . . . . . . . . . . . . . . . 501.2.1 什么样的模型？ . . . . . . . . . . . . . . . . . . . . . 501.2.2 自动方法 . . . . . . . . . . . . . . . . . . . . . 701.2.3 适应性推理算法 . . . . . . . . . . . . . . . . . 801.3 贡献 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 801.4 论文结构 . . . . . . . . . . . . . . . . . . . . . . . 901.1 背景0据估计，2013年全球使用互联网的人数约为27亿人[Sanou2013]，占全球人口的39%。另一方面，Netcraft [Netcraft2014]在2014年记录了近10亿个活跃的网站和同样数量的潜在易受攻击的Web应用程序。与Web相关的技术、服务和访问手段的发展，如智能手机，为此做出了贡献，但作为回报，Web已成为一个即使最微小的漏洞也可以卖给最高出价者并被用于金融、政治或仅仅是展示黑客能力的地方。0社交网络、在线账户和电子邮件已成为黑客的首选目标。对这些应用程序的安全测试需求越来越大，但由于技术的不断发展，这变得更加复杂。SPaCIoS项目[Vigano 2013]试图回应这个问题。Le projet SPaCIoS (Secure Provision and Consumption in the Internet of Ser-vices) est un projet europ´een constitu´e de 7 partenaires, 5 provenant du mondeacad´emique (l’universit´e de V´erone, ETH Zurich, l’Institut Polytechnique de Gre-noble, l’universit´e de Gˆenes, l’Institute e-Austria de Timisoara et l’universit´e tech-nique de Munich) et 2 du monde industriel (Siemens et SAP).0第1章 引言0SPaCIoS项目（Secure Provision and Consumption in the Internet ofServices）是一个由7个合作伙伴组成的欧洲项目，其中5个来自学术界（维罗纳大学、苏黎世联邦理工学院、格勒诺布尔理工学院、热那亚大学、蒂米什瓦拉电子奥地利研究所和慕尼黑工业大学），2个来自工业界（西门子和SAP）。01.1.1 SPaCIoS项目0服务互联网（IoS）彻底改变了应用程序的思考、实施、部署和使用方式：应用程序不再是由一个组件的编程结果，而是由通过互联网分布的多个组件组成，并根据需求按需灵活使用。然而，只有存在用于确保其安全性的概念、工具和技术，才能充分利用这种架构带来的新机遇。0这个定义是SPaCIoS项目的主要目标。它将为自动验证安全性的新一代分析器奠定技术基础，从而提高IoS的安全性。为了实现这个目标，SPaCIoS工具结合了最新的渗透测试、安全测试、模型检查和自动学习技术和方法。该工具已经在来自自由软件界和工业界的应用程序上进行了实施。这将使项目的结果能够转化为工业界使用的实践。0图1.1显示了SPaCIoS工具的架构表示。0SPaCIoS方法的关键是使用模型来表示系统，并使用多种方法生成安全测试用例（变异测试、属性违规检测、渗透测试模拟）。由于大多数情况下，应用程序没有可用的正式模型，测试人员必须自己编写模型。模型推理的目的正是解决这个问题，为用户提供一种自动生成应用程序模型的方法。虽然这个模型不一定等同于手动编写的模型，但它提供了一个起点模型，用户可以进行补充。01.1. 背景0图1.1 - SPaCIoS工具的架构01.1.2 模型推理0基于属性的测试用例生成方法认为要测试的系统的每个组件都已经用ASLan++（Oheimb2012）[D3.22011]高级规范语言进行了建模，但这要求事先对系统的内部行为、特性有一定的了解，以及对ASLan++语言建模有一定的专业知识。在大多数情况下，测试人员没有足够的知识来进行建模，特别是当应用程序是由多个单独开发的组件组合而成，并且由不同的团队开发时。0模型推理可以自动化这一方法的一部分，通过创建系统的模型，然后将其转换为ASLan++形式的自动机。SPaCIoS工具包括两种推理方法，用于自动构建这些模型：0- 黑盒方法，使用与系统的交互，这是本论文中介绍的工作，与SAP共同开发。
我的内容管理
收起
我的收益 登录查看自己的收益
我的积分
登录查看自己的积分
我的C币
登录后查看C币余额
我的收藏 
我的下载 
下载帮助 
